internlm/Lean-Github huggingface dataset:
Theorem: partitionImpl.loop_invariant
Proof state before:
case base
α : 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
h : ¬first < i
inv : LoopInvariant arr first i j last
⊢ ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
    partitionImpl arr first i j fi ij✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
Tactic:
simp [*]
Proof state after:
case base
α : 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
h : ¬first < i
inv : LoopInvariant arr first i j last
⊢ LoopInvariant arr first first j last
Theorem: partitionImpl.loop_invariant
Proof state before:
case base
α : 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
h : ¬first < i
inv : LoopInvariant arr first i j last
⊢ LoopInvariant arr first first j last
Tactic:
have : i = first := Fin.eq_of_val_eq (Nat.le_antisymm (Nat.le_of_not_lt h) fi)
Proof state after:
case base
α : 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
h : ¬first < i
inv : LoopInvariant arr first i j last
this : i = first
⊢ LoopInvariant arr first first j last
Theorem: partitionImpl.loop_invariant
Proof state before:
case base
α : 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
h : ¬first < i
inv : LoopInvariant arr first i j last
this : i = first
⊢ LoopInvariant arr first first j last
Tactic:
exact this ▸ inv
Proof state after:
no goals
Theorem: partitionImpl.loop_invariant
Proof state before:
case step_lt
α : 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
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
Tactic:
have inv : LoopInvariant arr first i.prev j last := by
  apply LoopInvariant.intro
  . intro k ik kj
    have ik : i.val ≤ k.val := by
      rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
      exact ik
    cases Nat.eq_or_lt_of_le ik with
    | inl ik =>
      simp [Fin.eq_of_val_eq ik] at lt
      exact lt
    | inr ik => exact inv.1 k ik kj
  . exact inv.2
  . intro ij
    have ij : i.val ≤ j.val := by
      rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
      exact ij
    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:
case step_lt
α : 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
inv : LoopInvariant arr first i.prev j last
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
Theorem: partitionImpl.loop_invariant
Proof state before:
case step_lt
α : 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
inv : LoopInvariant arr first i.prev j last
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
Tactic:
simp [*] at eq
Proof state after:
case step_lt
α : 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
inv : LoopInvariant arr first i.prev j last
eq : partitionImpl arr first i.prev j ⋯ ⋯ = result
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
Theorem: partitionImpl.loop_invariant
Proof state before:
case step_lt
α : 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
inv : LoopInvariant arr first i.prev j last
eq : partitionImpl arr first i.prev j ⋯ ⋯ = result
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
Tactic:
apply ih inv result eq
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
⊢ LoopInvariant arr first i.prev j last
Tactic:
apply LoopInvariant.intro
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
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
⊢ ∀ (k : Fin n), i.prev < k → k < j → arr[k] < arr[first]

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
⊢ ∀ (k : Fin n), j < k → k ≤ last → ¬arr[k] < arr[first]

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
⊢ i.prev < j → arr[j] < arr[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
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
⊢ ∀ (k : Fin n), j < k → k ≤ last → ¬arr[k] < arr[first]

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
⊢ i.prev < j → arr[j] < arr[first]
Tactic:
. exact inv.2
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
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
⊢ i.prev < j → arr[j] < arr[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
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
⊢ i.prev < j → arr[j] < arr[first]
Tactic:
. intro ij
  have ij : i.val ≤ j.val := by
    rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
    exact ij
  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:
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
⊢ ∀ (k : Fin n), i.prev < k → k < j → arr[k] < arr[first]
Tactic:
intro k ik kj
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
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
k : Fin n
ik : i.prev < k
kj : k < j
⊢ arr[k] < arr[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
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
k : Fin n
ik : i.prev < k
kj : k < j
⊢ arr[k] < arr[first]
Tactic:
have ik : i.val ≤ k.val := by
  rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
  exact ik
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
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
k : Fin n
ik✝ : i.prev < k
kj : k < j
ik : ↑i ≤ ↑k
⊢ arr[k] < arr[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
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
k : Fin n
ik✝ : i.prev < k
kj : k < j
ik : ↑i ≤ ↑k
⊢ arr[k] < arr[first]
Tactic:
cases Nat.eq_or_lt_of_le ik with
| inl ik =>
  simp [Fin.eq_of_val_eq ik] at lt
  exact lt
| inr ik => 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
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
k : Fin n
ik : i.prev < k
kj : k < j
⊢ ↑i ≤ ↑k
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
k : Fin n
ik : i.prev < k
kj : k < j
⊢ ↑i - Nat.succ 0 + Nat.succ 0 ≤ ↑k
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
k : Fin n
ik : i.prev < k
kj : k < j
⊢ ↑i - Nat.succ 0 + Nat.succ 0 ≤ ↑k
Tactic:
exact ik
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
k : Fin n
ik✝¹ : i.prev < k
kj : k < j
ik✝ : ↑i ≤ ↑k
ik : ↑i = ↑k
⊢ arr[k] < arr[first]
Tactic:
simp [Fin.eq_of_val_eq ik] at lt
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
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
k : Fin n
ik✝¹ : i.prev < k
kj : k < j
ik✝ : ↑i ≤ ↑k
ik : ↑i = ↑k
lt : arr[k] < arr[first]
⊢ arr[k] < 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
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
k : Fin n
ik✝¹ : i.prev < k
kj : k < j
ik✝ : ↑i ≤ ↑k
ik : ↑i = ↑k
lt : arr[k] < arr[first]
⊢ arr[k] < arr[first]
Tactic:
exact lt
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
k : Fin n
ik✝¹ : i.prev < k
kj : k < j
ik✝ : ↑i ≤ ↑k
ik : ↑i < ↑k
⊢ arr[k] < arr[first]
Tactic:
exact inv.1 k ik 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
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
⊢ ∀ (k : Fin n), j < k → k ≤ last → ¬arr[k] < arr[first]
Tactic:
exact inv.2
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
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
⊢ i.prev < j → arr[j] < arr[first]
Tactic:
intro ij
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
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
⊢ arr[j] < arr[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
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
⊢ arr[j] < arr[first]
Tactic:
have ij : i.val ≤ j.val := by
  rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
  exact ij
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
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]