internlm/Lean-Github huggingface dataset:
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
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✝
k : Fin n
ik✝¹ : i.prev < k
kj : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i = ↑k
⊢ swapped[i] = arr[j]
Tactic:
apply Vec.get_swap_left
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
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✝
k : Fin n
ik✝¹ : i.prev < k
kj : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
⊢ swapped[k] < swapped[first]
Tactic:
have kj : k < j := (Nat.lt_of_lt_of_le kj (Nat.sub_le ..))
Proof state after:
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
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✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ swapped[k] < swapped[first]
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
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✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ swapped[k] < swapped[first]
Tactic:
have : swapped[k] = arr[k] := by
  apply Vec.get_swap_neq
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_gt ik
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_lt kj
Proof state after:
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
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✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
this : swapped[k] = arr[k]
⊢ swapped[k] < swapped[first]
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
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✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
this : swapped[k] = arr[k]
⊢ swapped[k] < swapped[first]
Tactic:
rw [this, sf]
Proof state after:
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
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✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
this : swapped[k] = arr[k]
⊢ arr[k] < arr[first]
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
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✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
this : swapped[k] = arr[k]
⊢ arr[k] < arr[first]
Tactic:
exact inv.1 k ik kj
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
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✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ swapped[k] = arr[k]
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
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✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ k ≠ 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
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✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ k ≠ 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
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✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ k ≠ 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
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✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ k ≠ j
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_gt ik
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
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✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ k ≠ 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
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✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ k ≠ j
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_lt kj
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
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✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ k ≠ 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
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✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ ¬↑k = ↑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
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✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ ¬↑k = ↑i
Tactic:
exact Nat.ne_of_gt ik
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
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✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ k ≠ 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
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✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ ¬↑k = ↑j
Theorem: partitionImpl.loop_invariant
Proof state before:
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
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✝
k : Fin n
ik✝¹ : i.prev < k
kj✝ : k < j.prev
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
kj : k < j
⊢ ¬↑k = ↑j
Tactic:
exact Nat.ne_of_lt kj
Proof state after:
no goals
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
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✝
⊢ ∀ (k : Fin n), j.prev < k → k ≤ last → ¬swapped[k] < swapped[first]
Tactic:
intro k jk kl
Proof state after:
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
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✝
k : Fin n
jk : j.prev < k
kl : k ≤ last
⊢ ¬swapped[k] < swapped[first]
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
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✝
k : Fin n
jk : j.prev < k
kl : k ≤ last
⊢ ¬swapped[k] < swapped[first]
Tactic:
have jk : j.val ≤ k.val := by
  rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt (Nat.zero_lt_of_lt (Nat.lt_of_lt_of_le fi ij)))]
  exact jk
Proof state after:
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
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✝
k : Fin n
jk✝ : j.prev < k
kl : k ≤ last
jk : ↑j ≤ ↑k
⊢ ¬swapped[k] < swapped[first]
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
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✝
k : Fin n
jk✝ : j.prev < k
kl : k ≤ last
jk : ↑j ≤ ↑k
⊢ ¬swapped[k] < swapped[first]
Tactic:
cases Nat.eq_or_lt_of_le jk with
| inl jk =>
  have : swapped[k] = arr[i] := by
    simp [Fin.eq_of_val_eq jk.symm]
    apply Vec.get_swap_right
  rw [this, sf]
  assumption
| inr jk =>
  have : swapped[k] = arr[k] := by
    apply Vec.get_swap_neq
    . apply Fin.ne_of_val_ne
      exact Nat.ne_of_gt (Nat.lt_of_le_of_lt ij jk)
    . apply Fin.ne_of_val_ne
      exact Nat.ne_of_gt jk
  rw [this, sf]
  exact inv.2 k jk kl
Proof state after:
no goals