internlm/Lean-Github huggingface dataset:
Theorem: partition.partition
Proof state before:
case kj
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
⊢ k ≠ ⟨↑mid.val, this✝¹⟩
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_gt mk
Proof state after:
no goals
Theorem: partition.partition
Proof state before:
case ki
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
⊢ k ≠ first
Tactic:
apply Fin.ne_of_val_ne
Proof state after:
case ki.h
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
⊢ ¬↑k = ↑first
Theorem: partition.partition
Proof state before:
case ki.h
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
⊢ ¬↑k = ↑first
Tactic:
exact Nat.ne_of_gt (Nat.lt_of_le_of_lt mid.property.1 mk)
Proof state after:
no goals
Theorem: partition.partition
Proof state before:
case kj
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
⊢ k ≠ ⟨↑mid.val, this✝¹⟩
Tactic:
apply Fin.ne_of_val_ne
Proof state after:
case kj.h
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
⊢ ¬↑k = ↑⟨↑mid.val, this✝¹⟩
Theorem: partition.partition
Proof state before:
case kj.h
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
k : Fin n
mk : ↑mid.val < ↑k
kl : k ≤ last
⊢ ¬↑k = ↑⟨↑mid.val, this✝¹⟩
Tactic:
exact Nat.ne_of_gt mk
Proof state after:
no goals
Theorem: partition.partition
Proof state before:
case left
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ ∀ (k : Fin n), first ≤ k → ↑k < ↑result.fst.val → result.snd[k] < arr[first]
Tactic:
simp [*]
Proof state after:
case left
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
Theorem: partition.partition
Proof state before:
case left
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
Tactic:
apply p₁
Proof state after:
no goals
Theorem: partition.partition
Proof state before:
case right.right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]
Tactic:
. simp [*]
  apply p₃
Proof state after:
no goals
Theorem: partition.partition
Proof state before:
case right.left
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ result.snd[result.fst.val] = arr[first]
Tactic:
simp [*]
Proof state after:
no goals
Theorem: partition.partition
Proof state before:
case right.right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ ∀ (k : Fin n), ↑result.fst.val < ↑k → k ≤ last → ¬result.snd[k] < arr[first]
Tactic:
simp [*]
Proof state after:
case right.right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
Theorem: partition.partition
Proof state before:
case right.right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first last : Fin n
fl : first ≤ last
result : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n
eq : _root_.partition arr first last fl = result
afterLoop : { mid // first ≤ mid ∧ mid ≤ last } × Vec α n := partitionImpl arr first last last fl ⋯
mid : { mid // first ≤ mid ∧ mid ≤ last } := afterLoop.fst
arr' : Vec α n := afterLoop.snd
this✝¹ : ↑mid.val < n
swapped : Vec α n := arr'.swap first ⟨↑mid.val, this✝¹⟩
this✝ : result.fst = mid
this : result.snd = swapped
first_eq : arr'[first] = arr[first]
inv₀ : partitionImpl.LoopInvariant arr first last last last :=
  { inv₁ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_trans kl lk)),
    inv₂ := fun k lk kl => False.elim (Nat.lt_irrefl (↑k) (Nat.lt_of_le_of_lt kl lk)),
    inv₃ := fun ll => False.elim (Nat.lt_irrefl (↑last) ll) }
inv : partitionImpl.LoopInvariant afterLoop.snd first first ⟨↑afterLoop.fst.val, ⋯⟩ last :=
  partitionImpl.loop_invariant arr first last last last fl (Nat.le_refl ↑last) inv₀ afterLoop
    (Eq.refl (partitionImpl arr first last last fl (Nat.le_refl ↑last)))
p₁ : ∀ (k : Fin n), first ≤ k → ↑k < ↑mid.val → swapped[k] < arr[first]
p₂ : swapped[mid.val] = arr[first]
p₃ : ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
⊢ ∀ (k : Fin n), ↑mid.val < ↑k → k ≤ last → ¬swapped[k] < arr[first]
Tactic:
apply p₃
Proof state after:
no goals
Theorem: quickSortImpl.get_lt
Proof state before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first : Nat
last k : Fin n
lt : ↑k < first
⊢ (quickSortImpl arr first last)[k] = arr[k]
Tactic:
let p := quickSortImpl_permuted arr first last
Proof state after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first : Nat
last k : Fin n
lt : ↑k < first
p : permuted n first (↑last) arr (quickSortImpl arr first last) := quickSortImpl_permuted arr first last
⊢ (quickSortImpl arr first last)[k] = arr[k]
Theorem: quickSortImpl.get_lt
Proof state before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first : Nat
last k : Fin n
lt : ↑k < first
p : permuted n first (↑last) arr (quickSortImpl arr first last) := quickSortImpl_permuted arr first last
⊢ (quickSortImpl arr first last)[k] = arr[k]
Tactic:
exact p.get_lt lt
Proof state after:
no goals
Theorem: quickSortImpl.get_gt
Proof state before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first : Nat
last k : Fin n
gt : k > last
⊢ (quickSortImpl arr first last)[k] = arr[k]
Tactic:
let p := quickSortImpl_permuted arr first last
Proof state after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first : Nat
last k : Fin n
gt : k > last
p : permuted n first (↑last) arr (quickSortImpl arr first last) := quickSortImpl_permuted arr first last
⊢ (quickSortImpl arr first last)[k] = arr[k]
Theorem: quickSortImpl.get_gt
Proof state before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first : Nat
last k : Fin n
gt : k > last
p : permuted n first (↑last) arr (quickSortImpl arr first last) := quickSortImpl_permuted arr first last
⊢ (quickSortImpl arr first last)[k] = arr[k]
Tactic:
exact p.get_gt gt
Proof state after:
no goals
Theorem: quickSortImpl_sortedRange
Proof state before:
case base
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
h : ¬first < ↑last
⊢ sortedRange (quickSortImpl arr first last) first ↑last
Tactic:
simp [*]
Proof state after:
case base
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
h : ¬first < ↑last
⊢ sortedRange arr first ↑last
Theorem: quickSortImpl_sortedRange
Proof state before:
case base
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
h : ¬first < ↑last
⊢ sortedRange arr first ↑last
Tactic:
intro i j fi ij jl
Proof state after:
case base
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
h : ¬first < ↑last
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ ↑last
⊢ (compare arr[i] arr[j]).isLE = true
Theorem: quickSortImpl_sortedRange
Proof state before:
case base
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
h : ¬first < ↑last
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ ↑last
⊢ (compare arr[i] arr[j]).isLE = true
Tactic:
have : first = last := Nat.le_antisymm (Nat.le_trans (Nat.le_trans fi ij) jl) (Nat.le_of_not_gt h)
Proof state after:
case base
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
h : ¬first < ↑last
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ ↑last
this : first = ↑last
⊢ (compare arr[i] arr[j]).isLE = true