internlm/Lean-Github huggingface dataset:
Theorem: partitionImpl.loop_invariant
Proof state before:
case inv₃
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝¹ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝¹ = result
ij✝ : i.prev < j
ij : ↑i ≤ ↑j
⊢ arr[j] < arr[first]
Tactic:
cases Nat.eq_or_lt_of_le ij with
| inl ij =>
  simp [Fin.eq_of_val_eq ij.symm]
  assumption
| inr ij => exact inv.3 ij
Proof state after:
no goals
Theorem: partitionImpl.loop_invariant
Proof state before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
ij : i.prev < j
⊢ ↑i ≤ ↑j
Tactic:
rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
Proof state after:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
ij : i.prev < j
⊢ ↑i - Nat.succ 0 + Nat.succ 0 ≤ ↑j
Theorem: partitionImpl.loop_invariant
Proof state before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝ : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝ = result
ij : i.prev < j
⊢ ↑i - Nat.succ 0 + Nat.succ 0 ≤ ↑j
Tactic:
exact ij
Proof state after:
no goals
Theorem: partitionImpl.loop_invariant
Proof state before:
case inv₃.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝² = result
ij✝¹ : i.prev < j
ij✝ : ↑i ≤ ↑j
ij : ↑i = ↑j
⊢ arr[j] < arr[first]
Tactic:
simp [Fin.eq_of_val_eq ij.symm]
Proof state after:
case inv₃.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝² = result
ij✝¹ : i.prev < j
ij✝ : ↑i ≤ ↑j
ij : ↑i = ↑j
⊢ arr[i] < arr[first]
Theorem: partitionImpl.loop_invariant
Proof state before:
case inv₃.inl
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝² = result
ij✝¹ : i.prev < j
ij✝ : ↑i ≤ ↑j
ij : ↑i = ↑j
⊢ arr[i] < arr[first]
Tactic:
assumption
Proof state after:
no goals
Theorem: partitionImpl.loop_invariant
Proof state before:
case inv₃.inr
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij✝² : i ≤ j
fi : first < i
x✝¹ : ↑first ≤ ↑i - 1
lt : arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j
ih :
  LoopInvariant arr first i.prev j last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
      partitionImpl arr first i.prev j x✝¹ x✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij✝² = result
ij✝¹ : i.prev < j
ij✝ : ↑i ≤ ↑j
ij : ↑i < ↑j
⊢ arr[j] < arr[first]
Tactic:
exact inv.3 ij
Proof state after:
no goals
Theorem: partitionImpl.loop_invariant
Proof state before:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
Tactic:
let swapped := arr.swap i j
Proof state after:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
Theorem: partitionImpl.loop_invariant
Proof state before:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
Tactic:
have sf : swapped[first] = arr[first] := by
  apply Vec.get_swap_neq
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_lt fi
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_lt (Nat.lt_of_lt_of_le fi ij)
Proof state after:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
Theorem: partitionImpl.loop_invariant
Proof state before:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
Tactic:
let result := partitionImpl swapped first i.prev j.prev (by assumption) (by assumption)
Proof state after:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result✝ : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result✝
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ LoopInvariant result✝.snd first first ⟨↑result✝.fst.val, ⋯⟩ last
Theorem: partitionImpl.loop_invariant
Proof state before:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result✝ : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result✝
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ LoopInvariant result✝.snd first first ⟨↑result✝.fst.val, ⋯⟩ last
Tactic:
subst eq
Proof state after:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ LoopInvariant (partitionImpl arr first i j fi✝ ij).snd first first ⟨↑(partitionImpl arr first i j fi✝ ij).fst.val, ⋯⟩
    last
Theorem: partitionImpl.loop_invariant
Proof state before:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ LoopInvariant (partitionImpl arr first i j fi✝ ij).snd first first ⟨↑(partitionImpl arr first i j fi✝ ij).fst.val, ⋯⟩
    last
Tactic:
simp [*]
Proof state after:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
⊢ LoopInvariant (partitionImpl (arr.swap i j) first i.prev j.prev ⋯ ⋯).snd first first
    (partitionImpl (arr.swap i j) first i.prev j.prev ⋯ ⋯).1.val last
Theorem: partitionImpl.loop_invariant
Proof state before:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv✝ : LoopInvariant arr first i j last
swapped : Vec α n := arr.swap i j
sf : swapped[first] = arr[first]
result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n := partitionImpl swapped first i.prev j.prev x✝² x✝
inv : LoopInvariant swapped first i.prev j.prev last
⊢ LoopInvariant (partitionImpl (arr.swap i j) first i.prev j.prev ⋯ ⋯).snd first first
    (partitionImpl (arr.swap i j) first i.prev j.prev ⋯ ⋯).1.val last
Tactic:
exact ih inv result (by rfl)
Proof state after:
no goals
Theorem: partitionImpl.loop_invariant
Proof state before:
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ swapped[first] = arr[first]
Tactic:
apply Vec.get_swap_neq
Proof state after:
case ki
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ first ≠ i

case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ first ≠ j
Theorem: partitionImpl.loop_invariant
Proof state before:
case ki
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ first ≠ i

case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ first ≠ j
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_lt fi
Proof state after:
case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ first ≠ j
Theorem: partitionImpl.loop_invariant
Proof state before:
case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ first ≠ j
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_lt (Nat.lt_of_lt_of_le fi ij)
Proof state after:
no goals
Theorem: partitionImpl.loop_invariant
Proof state before:
case ki
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ first ≠ i
Tactic:
apply Fin.ne_of_val_ne
Proof state after:
case ki.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ ¬↑first = ↑i
Theorem: partitionImpl.loop_invariant
Proof state before:
case ki.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ ¬↑first = ↑i
Tactic:
exact Nat.ne_of_lt fi
Proof state after:
no goals
Theorem: partitionImpl.loop_invariant
Proof state before:
case kj
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ first ≠ j
Tactic:
apply Fin.ne_of_val_ne
Proof state after:
case kj.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih :
  LoopInvariant (arr.swap i j) first i.prev j.prev last →
    ∀ (result : { mid // first ≤ mid ∧ mid ≤ j.prev } × Vec α n),
      partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result →
        LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi✝ ij = result
swapped : Vec α n := arr.swap i j
⊢ ¬↑first = ↑j