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✝
ij✝¹ : i.prev < j.prev
this✝ : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i = ↑j - 1
this : swapped[j.prev] = arr[j]
⊢ ↑i ≤ ↑j - 1
Tactic:
assumption
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✝
ij✝¹ : i.prev < j.prev
this✝ : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i = ↑j - 1
this : swapped[j.prev] = arr[j]
⊢ ↑j - 1 < ↑j
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
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✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ swapped[j.prev] < swapped[first]
Tactic:
have : swapped[j.prev] = arr[j.prev] := by
  apply Vec.get_swap_neq
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_gt ij
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_lt (by assumption)
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✝
ij✝¹ : i.prev < j.prev
this✝ : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
this : swapped[j.prev] = arr[j.prev]
⊢ swapped[j.prev] < 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✝
ij✝¹ : i.prev < j.prev
this✝ : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
this : swapped[j.prev] = arr[j.prev]
⊢ swapped[j.prev] < 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✝
ij✝¹ : i.prev < j.prev
this✝ : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
this : swapped[j.prev] = arr[j.prev]
⊢ arr[j.prev] < 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✝
ij✝¹ : i.prev < j.prev
this✝ : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
this : swapped[j.prev] = arr[j.prev]
⊢ arr[j.prev] < arr[first]
Tactic:
apply inv.1 j.prev ij (by assumption)
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✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ swapped[j.prev] = arr[j.prev]
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✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ j.prev ≠ 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✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ j.prev ≠ 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✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ j.prev ≠ 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✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ j.prev ≠ j
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_gt ij
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✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ j.prev ≠ 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✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ j.prev ≠ j
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_lt (by assumption)
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✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ j.prev ≠ 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✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ ¬↑j.prev = ↑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✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ ¬↑j.prev = ↑i
Tactic:
exact Nat.ne_of_gt ij
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✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ j.prev ≠ 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✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ ¬↑j.prev = ↑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✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ ¬↑j.prev = ↑j
Tactic:
exact Nat.ne_of_lt (by assumption)
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✝
ij✝¹ : i.prev < j.prev
this : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
⊢ ↑j.prev < ↑j
Tactic:
assumption
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✝
ij✝¹ : i.prev < j.prev
this✝ : ↑j - 1 < ↑j
ij✝ : ↑i ≤ ↑j - 1
ij : ↑i < ↑j - 1
this : swapped[j.prev] = arr[j.prev]
⊢ j.prev < j
Tactic:
assumption
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✝
inv : LoopInvariant swapped first i.prev j.prev last
⊢ partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝ = result
Tactic:
rfl
Proof state after:
no goals
Theorem: partitionImpl.first_eq
Proof state before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
⊢ (partitionImpl arr first i j fi ij).snd[first] = arr[first]
Tactic:
induction arr, first, i, j, fi, ij using partitionImpl.induct' with
| base => simp [*]
| step_lt => simp [*]
| step_ge arr first i j _ ij fi =>
  simp [*]
  have fj : first < j := Nat.lt_of_lt_of_le fi ij
  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 fj
Proof state after:
no goals
Theorem: partitionImpl.first_eq
Proof state before:
case base
α : Type
inst✝ : Ord α
n : Nat
first i j : Fin n
arr✝ : Vec α n
first✝ i✝ j✝ : Fin n
fi✝ : first✝ ≤ i✝
ij✝ : i✝ ≤ j✝
x✝ : ¬first✝ < i✝
⊢ (partitionImpl arr✝ first✝ i✝ j✝ fi✝ ij✝).snd[first✝] = arr✝[first✝]
Tactic:
simp [*]
Proof state after:
no goals
Theorem: partitionImpl.first_eq
Proof state before:
case step_lt
α : Type
inst✝ : Ord α
n : Nat
first i j : Fin n
arr✝ : Vec α n
first✝ i✝ j✝ : Fin n
fi✝ : first✝ ≤ i✝
ij✝ : i✝ ≤ j✝
x✝³ : first✝ < i✝
x✝² : ↑first✝ ≤ ↑i✝ - 1
x✝¹ : arr✝[i✝] < arr✝[first✝]
x✝ : ↑i✝ - 1 ≤ ↑j✝
ih✝ : (partitionImpl arr✝ first✝ i✝.prev j✝ x✝² x✝).snd[first✝] = arr✝[first✝]
⊢ (partitionImpl arr✝ first✝ i✝ j✝ fi✝ ij✝).snd[first✝] = arr✝[first✝]
Tactic:
simp [*]
Proof state after:
no goals
Theorem: partitionImpl.first_eq
Proof state before:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : 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✝ : (partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝).snd[first] = (arr.swap i j)[first]
⊢ (partitionImpl arr first i j fi✝ ij).snd[first] = arr[first]
Tactic:
simp [*]
Proof state after:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : 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✝ : (partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝).snd[first] = (arr.swap i j)[first]
⊢ (arr.swap i j)[first] = arr[first]
Theorem: partitionImpl.first_eq
Proof state before:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : 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✝ : (partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝).snd[first] = (arr.swap i j)[first]
⊢ (arr.swap i j)[first] = arr[first]
Tactic:
have fj : first < j := Nat.lt_of_lt_of_le fi ij
Proof state after:
case step_ge
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : 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✝ : (partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝).snd[first] = (arr.swap i j)[first]
fj : first < j
⊢ (arr.swap i j)[first] = arr[first]