internlm/Lean-Github huggingface dataset:
Theorem: quickSortImpl_sortedRange
Proof state before:
case step.lt
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
lt : first < ↑last
parted : { mid // first ≤ ↑mid ∧ mid ≤ last } × Vec α n
eq : partition arr ⟨first, ⋯⟩ last ⋯ = parted
ih₁ : sortedRange (quickSortImpl parted.snd first parted.fst.val.prev) first ↑parted.fst.val.prev
ih₂ :
  sortedRange (quickSortImpl (quickSortImpl parted.snd first parted.fst.val.prev) (↑parted.fst.val + 1) last)
    (↑parted.fst.val + 1) ↑last
this : first < n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ ↑last
mid : { mid // first ≤ ↑mid ∧ mid ≤ last } := parted.fst
mn : ↑mid.val < n
sorted : Vec α n := quickSortImpl (quickSortImpl parted.snd first mid.val.prev) (↑mid.val + 1) last
l : ∀ (k : Fin n), ⟨first, this⟩ ≤ k → ↑k < ↑parted.fst.val → parted.snd[k] < arr[⟨first, this⟩]
m : parted.snd[parted.fst.val] = arr[⟨first, this⟩]
r : ∀ (k : Fin n), ↑parted.fst.val < ↑k → k ≤ last → ¬parted.snd[k] < arr[⟨first, this⟩]
getL : ∀ (k : Fin n), first ≤ ↑k → k < mid.val → sorted[k] < arr[first]
getM : ∀ (k : Fin n), ↑mid.val = ↑k → sorted[k] = arr[first]
getR : ∀ (k : Fin n), mid.val < k → k ≤ last → ¬sorted[k] < arr[first]
getLM : ∀ (k : Fin n), first ≤ ↑k → k ≤ mid.val → sorted[k] ≤ arr[first]
getMR : ∀ (k : Fin n), mid.val ≤ k → k ≤ last → ¬sorted[k] < arr[first]
im : ↑i < ↑mid.val
jm : ↑j < ↑mid.val
⊢ (compare (quickSortImpl parted.snd first parted.fst.val.prev)[i]
        (quickSortImpl (quickSortImpl parted.snd first parted.fst.val.prev) (↑parted.fst.val + 1) last)[j]).isLE =
    true
Tactic:
rw [quickSortImpl.get_lt (lt := Nat.lt_trans jm (Nat.lt_succ_self ..))]
Proof state after:
case step.lt
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
lt : first < ↑last
parted : { mid // first ≤ ↑mid ∧ mid ≤ last } × Vec α n
eq : partition arr ⟨first, ⋯⟩ last ⋯ = parted
ih₁ : sortedRange (quickSortImpl parted.snd first parted.fst.val.prev) first ↑parted.fst.val.prev
ih₂ :
  sortedRange (quickSortImpl (quickSortImpl parted.snd first parted.fst.val.prev) (↑parted.fst.val + 1) last)
    (↑parted.fst.val + 1) ↑last
this : first < n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ ↑last
mid : { mid // first ≤ ↑mid ∧ mid ≤ last } := parted.fst
mn : ↑mid.val < n
sorted : Vec α n := quickSortImpl (quickSortImpl parted.snd first mid.val.prev) (↑mid.val + 1) last
l : ∀ (k : Fin n), ⟨first, this⟩ ≤ k → ↑k < ↑parted.fst.val → parted.snd[k] < arr[⟨first, this⟩]
m : parted.snd[parted.fst.val] = arr[⟨first, this⟩]
r : ∀ (k : Fin n), ↑parted.fst.val < ↑k → k ≤ last → ¬parted.snd[k] < arr[⟨first, this⟩]
getL : ∀ (k : Fin n), first ≤ ↑k → k < mid.val → sorted[k] < arr[first]
getM : ∀ (k : Fin n), ↑mid.val = ↑k → sorted[k] = arr[first]
getR : ∀ (k : Fin n), mid.val < k → k ≤ last → ¬sorted[k] < arr[first]
getLM : ∀ (k : Fin n), first ≤ ↑k → k ≤ mid.val → sorted[k] ≤ arr[first]
getMR : ∀ (k : Fin n), mid.val ≤ k → k ≤ last → ¬sorted[k] < arr[first]
im : ↑i < ↑mid.val
jm : ↑j < ↑mid.val
⊢ (compare (quickSortImpl parted.snd first parted.fst.val.prev)[i]
        (quickSortImpl parted.snd first parted.fst.val.prev)[j]).isLE =
    true
Theorem: quickSortImpl_sortedRange
Proof state before:
case step.lt
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
lt : first < ↑last
parted : { mid // first ≤ ↑mid ∧ mid ≤ last } × Vec α n
eq : partition arr ⟨first, ⋯⟩ last ⋯ = parted
ih₁ : sortedRange (quickSortImpl parted.snd first parted.fst.val.prev) first ↑parted.fst.val.prev
ih₂ :
  sortedRange (quickSortImpl (quickSortImpl parted.snd first parted.fst.val.prev) (↑parted.fst.val + 1) last)
    (↑parted.fst.val + 1) ↑last
this : first < n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ ↑last
mid : { mid // first ≤ ↑mid ∧ mid ≤ last } := parted.fst
mn : ↑mid.val < n
sorted : Vec α n := quickSortImpl (quickSortImpl parted.snd first mid.val.prev) (↑mid.val + 1) last
l : ∀ (k : Fin n), ⟨first, this⟩ ≤ k → ↑k < ↑parted.fst.val → parted.snd[k] < arr[⟨first, this⟩]
m : parted.snd[parted.fst.val] = arr[⟨first, this⟩]
r : ∀ (k : Fin n), ↑parted.fst.val < ↑k → k ≤ last → ¬parted.snd[k] < arr[⟨first, this⟩]
getL : ∀ (k : Fin n), first ≤ ↑k → k < mid.val → sorted[k] < arr[first]
getM : ∀ (k : Fin n), ↑mid.val = ↑k → sorted[k] = arr[first]
getR : ∀ (k : Fin n), mid.val < k → k ≤ last → ¬sorted[k] < arr[first]
getLM : ∀ (k : Fin n), first ≤ ↑k → k ≤ mid.val → sorted[k] ≤ arr[first]
getMR : ∀ (k : Fin n), mid.val ≤ k → k ≤ last → ¬sorted[k] < arr[first]
im : ↑i < ↑mid.val
jm : ↑j < ↑mid.val
⊢ (compare (quickSortImpl parted.snd first parted.fst.val.prev)[i]
        (quickSortImpl parted.snd first parted.fst.val.prev)[j]).isLE =
    true
Tactic:
exact ih₁ i j fi ij (Nat.le_sub_of_add_le jm)
Proof state after:
no goals
Theorem: quickSortImpl_sortedRange
Proof state before:
case step.ge
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
lt : first < ↑last
parted : { mid // first ≤ ↑mid ∧ mid ≤ last } × Vec α n
eq : partition arr ⟨first, ⋯⟩ last ⋯ = parted
ih₁ : sortedRange (quickSortImpl parted.snd first parted.fst.val.prev) first ↑parted.fst.val.prev
ih₂ :
  sortedRange (quickSortImpl (quickSortImpl parted.snd first parted.fst.val.prev) (↑parted.fst.val + 1) last)
    (↑parted.fst.val + 1) ↑last
this : first < n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ ↑last
mid : { mid // first ≤ ↑mid ∧ mid ≤ last } := parted.fst
mn : ↑mid.val < n
sorted : Vec α n := quickSortImpl (quickSortImpl parted.snd first mid.val.prev) (↑mid.val + 1) last
l : ∀ (k : Fin n), ⟨first, this⟩ ≤ k → ↑k < ↑parted.fst.val → parted.snd[k] < arr[⟨first, this⟩]
m : parted.snd[parted.fst.val] = arr[⟨first, this⟩]
r : ∀ (k : Fin n), ↑parted.fst.val < ↑k → k ≤ last → ¬parted.snd[k] < arr[⟨first, this⟩]
getL : ∀ (k : Fin n), first ≤ ↑k → k < mid.val → sorted[k] < arr[first]
getM : ∀ (k : Fin n), ↑mid.val = ↑k → sorted[k] = arr[first]
getR : ∀ (k : Fin n), mid.val < k → k ≤ last → ¬sorted[k] < arr[first]
getLM : ∀ (k : Fin n), first ≤ ↑k → k ≤ mid.val → sorted[k] ≤ arr[first]
getMR : ∀ (k : Fin n), mid.val ≤ k → k ≤ last → ¬sorted[k] < arr[first]
mi : ↑mid.val < ↑i
mj : ↑mid.val < ↑j
⊢ (compare (quickSortImpl (quickSortImpl parted.snd first parted.fst.val.prev) (↑parted.fst.val + 1) last)[i]
        (quickSortImpl (quickSortImpl parted.snd first parted.fst.val.prev) (↑parted.fst.val + 1) last)[j]).isLE =
    true
Tactic:
exact ih₂ i j mi ij jl
Proof state after:
no goals
Theorem: quickSortImpl_sortedRange
Proof state before:
case step.split
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
lt : first < ↑last
parted : { mid // first ≤ ↑mid ∧ mid ≤ last } × Vec α n
eq : partition arr ⟨first, ⋯⟩ last ⋯ = parted
ih₁ : sortedRange (quickSortImpl parted.snd first parted.fst.val.prev) first ↑parted.fst.val.prev
ih₂ :
  sortedRange (quickSortImpl (quickSortImpl parted.snd first parted.fst.val.prev) (↑parted.fst.val + 1) last)
    (↑parted.fst.val + 1) ↑last
this : first < n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ ↑last
mid : { mid // first ≤ ↑mid ∧ mid ≤ last } := parted.fst
mn : ↑mid.val < n
sorted : Vec α n := quickSortImpl (quickSortImpl parted.snd first mid.val.prev) (↑mid.val + 1) last
l : ∀ (k : Fin n), ⟨first, this⟩ ≤ k → ↑k < ↑parted.fst.val → parted.snd[k] < arr[⟨first, this⟩]
m : parted.snd[parted.fst.val] = arr[⟨first, this⟩]
r : ∀ (k : Fin n), ↑parted.fst.val < ↑k → k ≤ last → ¬parted.snd[k] < arr[⟨first, this⟩]
getL : ∀ (k : Fin n), first ≤ ↑k → k < mid.val → sorted[k] < arr[first]
getM : ∀ (k : Fin n), ↑mid.val = ↑k → sorted[k] = arr[first]
getR : ∀ (k : Fin n), mid.val < k → k ≤ last → ¬sorted[k] < arr[first]
getLM : ∀ (k : Fin n), first ≤ ↑k → k ≤ mid.val → sorted[k] ≤ arr[first]
getMR : ∀ (k : Fin n), mid.val ≤ k → k ≤ last → ¬sorted[k] < arr[first]
im : ↑i ≤ ↑mid.val
mj : ↑mid.val ≤ ↑j
h₁ : sorted[i] ≤ arr[first]
h₂ : arr[first] ≤ sorted[j]
⊢ (compare (quickSortImpl (quickSortImpl parted.snd first parted.fst.val.prev) (↑parted.fst.val + 1) last)[i]
        (quickSortImpl (quickSortImpl parted.snd first parted.fst.val.prev) (↑parted.fst.val + 1) last)[j]).isLE =
    true
Tactic:
apply Order.trans h₁ h₂
Proof state after:
no goals
Theorem: quickSort'_sortedRange
Proof state before:
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
⊢ sortedRange (quickSort' arr) 0 (n - 1)
Tactic:
if h : n > 0 then
  simp [quickSort', h]
  apply quickSortImpl_sortedRange
else
  intro i
  have : n = 0 := Nat.eq_zero_of_not_pos h
  subst n
  exact (Nat.not_lt_zero i.val i.isLt).elim
Proof state after:
no goals
Theorem: quickSort'_sortedRange
Proof state before:
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
h : n > 0
⊢ sortedRange (quickSort' arr) 0 (n - 1)
Tactic:
simp [quickSort', h]
Proof state after:
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
h : n > 0
⊢ sortedRange (quickSortImpl arr 0 ⟨n - 1, ⋯⟩) 0 (n - 1)
Theorem: quickSort'_sortedRange
Proof state before:
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
h : n > 0
⊢ sortedRange (quickSortImpl arr 0 ⟨n - 1, ⋯⟩) 0 (n - 1)
Tactic:
apply quickSortImpl_sortedRange
Proof state after:
no goals
Theorem: quickSort'_sortedRange
Proof state before:
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
h : ¬n > 0
⊢ sortedRange (quickSort' arr) 0 (n - 1)
Tactic:
intro i
Proof state after:
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
h : ¬n > 0
i : Fin n
⊢ ∀ (j : Fin n), 0 ≤ ↑i → i ≤ j → ↑j ≤ n - 1 → (compare (quickSort' arr)[i] (quickSort' arr)[j]).isLE = true
Theorem: quickSort'_sortedRange
Proof state before:
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
h : ¬n > 0
i : Fin n
⊢ ∀ (j : Fin n), 0 ≤ ↑i → i ≤ j → ↑j ≤ n - 1 → (compare (quickSort' arr)[i] (quickSort' arr)[j]).isLE = true
Tactic:
have : n = 0 := Nat.eq_zero_of_not_pos h
Proof state after:
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
h : ¬n > 0
i : Fin n
this : n = 0
⊢ ∀ (j : Fin n), 0 ≤ ↑i → i ≤ j → ↑j ≤ n - 1 → (compare (quickSort' arr)[i] (quickSort' arr)[j]).isLE = true
Theorem: quickSort'_sortedRange
Proof state before:
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
h : ¬n > 0
i : Fin n
this : n = 0
⊢ ∀ (j : Fin n), 0 ≤ ↑i → i ≤ j → ↑j ≤ n - 1 → (compare (quickSort' arr)[i] (quickSort' arr)[j]).isLE = true
Tactic:
subst n
Proof state after:
α : Type
inst✝ : Order α
arr : Vec α 0
h : ¬0 > 0
i : Fin 0
⊢ ∀ (j : Fin 0), 0 ≤ ↑i → i ≤ j → ↑j ≤ 0 - 1 → (compare (quickSort' arr)[i] (quickSort' arr)[j]).isLE = true
Theorem: quickSort'_sortedRange
Proof state before:
α : Type
inst✝ : Order α
arr : Vec α 0
h : ¬0 > 0
i : Fin 0
⊢ ∀ (j : Fin 0), 0 ≤ ↑i → i ≤ j → ↑j ≤ 0 - 1 → (compare (quickSort' arr)[i] (quickSort' arr)[j]).isLE = true
Tactic:
exact (Nat.not_lt_zero i.val i.isLt).elim
Proof state after:
no goals
Theorem: quickSort_size
Proof state before:
α : Type
inst✝ : Order α
arr : Array α
⊢ (quickSort arr).size = arr.size
Tactic:
let sorted := quickSort' ⟨arr, rfl⟩
Proof state after:
α : Type
inst✝ : Order α
arr : Array α
sorted : Vec α arr.size := quickSort' ⟨arr, ⋯⟩
⊢ (quickSort arr).size = arr.size
Theorem: quickSort_size
Proof state before:
α : Type
inst✝ : Order α
arr : Array α
sorted : Vec α arr.size := quickSort' ⟨arr, ⋯⟩
⊢ (quickSort arr).size = arr.size
Tactic:
show sorted.val.size = arr.size
Proof state after:
α : Type
inst✝ : Order α
arr : Array α
sorted : Vec α arr.size := quickSort' ⟨arr, ⋯⟩
⊢ sorted.val.size = arr.size
Theorem: quickSort_size
Proof state before:
α : Type
inst✝ : Order α
arr : Array α
sorted : Vec α arr.size := quickSort' ⟨arr, ⋯⟩
⊢ sorted.val.size = arr.size
Tactic:
simp [sorted.property]
Proof state after:
no goals
Theorem: quickSort_sorted
Proof state before:
α : Type
inst✝ : Order α
arr : Array α
⊢ sorted (quickSort arr)
Tactic:
let sr := quickSort'_sortedRange (arr : Vec α arr.size)
Proof state after:
α : Type
inst✝ : Order α
arr : Array α
sr : sortedRange (quickSort' ⟨arr, ⋯⟩) 0 (arr.size - 1) := quickSort'_sortedRange ⟨arr, instCoeDepArrayVecSize.proof_1⟩
⊢ sorted (quickSort arr)
Theorem: quickSort_sorted
Proof state before:
α : Type
inst✝ : Order α
arr : Array α
sr : sortedRange (quickSort' ⟨arr, ⋯⟩) 0 (arr.size - 1) := quickSort'_sortedRange ⟨arr, instCoeDepArrayVecSize.proof_1⟩
⊢ sorted (quickSort arr)
Tactic:
intro i j ij
Proof state after:
α : Type
inst✝ : Order α
arr : Array α
sr : sortedRange (quickSort' ⟨arr, ⋯⟩) 0 (arr.size - 1) := quickSort'_sortedRange ⟨arr, instCoeDepArrayVecSize.proof_1⟩
i j : Fin (quickSort arr).size
ij : i ≤ j
⊢ (compare (quickSort arr)[i] (quickSort arr)[j]).isLE = true
Theorem: quickSort_sorted
Proof state before:
α : Type
inst✝ : Order α
arr : Array α
sr : sortedRange (quickSort' ⟨arr, ⋯⟩) 0 (arr.size - 1) := quickSort'_sortedRange ⟨arr, instCoeDepArrayVecSize.proof_1⟩
i j : Fin (quickSort arr).size
ij : i ≤ j
⊢ (compare (quickSort arr)[i] (quickSort arr)[j]).isLE = true
Tactic:
have hi : 0 ≤ i.val := Nat.zero_le i.val
Proof state after:
α : Type
inst✝ : Order α
arr : Array α
sr : sortedRange (quickSort' ⟨arr, ⋯⟩) 0 (arr.size - 1) := quickSort'_sortedRange ⟨arr, instCoeDepArrayVecSize.proof_1⟩
i j : Fin (quickSort arr).size
ij : i ≤ j
hi : 0 ≤ ↑i
⊢ (compare (quickSort arr)[i] (quickSort arr)[j]).isLE = true
Theorem: quickSort_sorted
Proof state before:
α : Type
inst✝ : Order α
arr : Array α
sr : sortedRange (quickSort' ⟨arr, ⋯⟩) 0 (arr.size - 1) := quickSort'_sortedRange ⟨arr, instCoeDepArrayVecSize.proof_1⟩
i j : Fin (quickSort arr).size
ij : i ≤ j
hi : 0 ≤ ↑i
⊢ (compare (quickSort arr)[i] (quickSort arr)[j]).isLE = true
Tactic:
have s : (quickSort arr).size = arr.size := quickSort_size arr
Proof state after:
α : Type
inst✝ : Order α
arr : Array α
sr : sortedRange (quickSort' ⟨arr, ⋯⟩) 0 (arr.size - 1) := quickSort'_sortedRange ⟨arr, instCoeDepArrayVecSize.proof_1⟩
i j : Fin (quickSort arr).size
ij : i ≤ j
hi : 0 ≤ ↑i
s : (quickSort arr).size = arr.size
⊢ (compare (quickSort arr)[i] (quickSort arr)[j]).isLE = true
Theorem: quickSort_sorted
Proof state before:
α : Type
inst✝ : Order α
arr : Array α
sr : sortedRange (quickSort' ⟨arr, ⋯⟩) 0 (arr.size - 1) := quickSort'_sortedRange ⟨arr, instCoeDepArrayVecSize.proof_1⟩
i j : Fin (quickSort arr).size
ij : i ≤ j
hi : 0 ≤ ↑i
s : (quickSort arr).size = arr.size
⊢ (compare (quickSort arr)[i] (quickSort arr)[j]).isLE = true
Tactic:
have hj : j.val ≤ arr.size - 1 := Nat.le_sub_one_of_lt (s ▸ j.isLt)
Proof state after:
α : Type
inst✝ : Order α
arr : Array α
sr : sortedRange (quickSort' ⟨arr, ⋯⟩) 0 (arr.size - 1) := quickSort'_sortedRange ⟨arr, instCoeDepArrayVecSize.proof_1⟩
i j : Fin (quickSort arr).size
ij : i ≤ j
hi : 0 ≤ ↑i
s : (quickSort arr).size = arr.size
hj : ↑j ≤ arr.size - 1
⊢ (compare (quickSort arr)[i] (quickSort arr)[j]).isLE = true
Theorem: quickSort_sorted
Proof state before:
α : Type
inst✝ : Order α
arr : Array α
sr : sortedRange (quickSort' ⟨arr, ⋯⟩) 0 (arr.size - 1) := quickSort'_sortedRange ⟨arr, instCoeDepArrayVecSize.proof_1⟩
i j : Fin (quickSort arr).size
ij : i ≤ j
hi : 0 ≤ ↑i
s : (quickSort arr).size = arr.size
hj : ↑j ≤ arr.size - 1
⊢ (compare (quickSort arr)[i] (quickSort arr)[j]).isLE = true
Tactic:
exact sr (i.cast s) (j.cast s) hi ij hj
Proof state after:
no goals
Theorem: Nat.sub_add_eq_add_sub
Proof state before:
m n k : Nat
km : k ≤ m
⊢ m - k + n = m + n - k
Tactic:
induction km with
| refl => simp [Nat.add_sub_cancel_left]
| @step m km ih =>
  have : k ≤ m + n := Nat.le_trans km (Nat.le_add_right ..)
  simp [Nat.succ_sub km, Nat.succ_add, ih, Nat.succ_sub this]
Proof state after:
no goals
Theorem: Nat.sub_add_eq_add_sub
Proof state before:
case refl
m n k : Nat
⊢ k - k + n = k + n - k
Tactic:
simp [Nat.add_sub_cancel_left]
Proof state after:
no goals
Theorem: Nat.sub_add_eq_add_sub
Proof state before:
case step
m✝ n k m : Nat
km : k.le m
ih : m - k + n = m + n - k
⊢ m.succ - k + n = m.succ + n - k
Tactic:
have : k ≤ m + n := Nat.le_trans km (Nat.le_add_right ..)
Proof state after:
case step
m✝ n k m : Nat
km : k.le m
ih : m - k + n = m + n - k
this : k ≤ m + n
⊢ m.succ - k + n = m.succ + n - k
Theorem: Nat.sub_add_eq_add_sub
Proof state before:
case step
m✝ n k m : Nat
km : k.le m
ih : m - k + n = m + n - k
this : k ≤ m + n
⊢ m.succ - k + n = m.succ + n - k
Tactic:
simp [Nat.succ_sub km, Nat.succ_add, ih, Nat.succ_sub this]
Proof state after:
no goals
Theorem: Nat.lt_sub_right
Proof state before:
m n k : Nat
mk : k ≤ m
mn : m < n
⊢ m - k < n - k
Tactic:
show m - k + 1 ≤ n - k
Proof state after:
m n k : Nat
mk : k ≤ m
mn : m < n
⊢ m - k + 1 ≤ n - k
Theorem: Nat.lt_sub_right
Proof state before:
m n k : Nat
mk : k ≤ m
mn : m < n
⊢ m - k + 1 ≤ n - k
Tactic:
have : m - k + 1 = m + 1 - k := Nat.sub_add_eq_add_sub mk
Proof state after:
m n k : Nat
mk : k ≤ m
mn : m < n
this : m - k + 1 = m + 1 - k
⊢ m - k + 1 ≤ n - k
Theorem: Nat.lt_sub_right
Proof state before:
m n k : Nat
mk : k ≤ m
mn : m < n
this : m - k + 1 = m + 1 - k
⊢ m - k + 1 ≤ n - k
Tactic:
rw [this]
Proof state after:
m n k : Nat
mk : k ≤ m
mn : m < n
this : m - k + 1 = m + 1 - k
⊢ m + 1 - k ≤ n - k
Theorem: Nat.lt_sub_right
Proof state before:
m n k : Nat
mk : k ≤ m
mn : m < n
this : m - k + 1 = m + 1 - k
⊢ m + 1 - k ≤ n - k
Tactic:
apply Nat.sub_le_sub_right mn
Proof state after:
no goals
Theorem: partitionImpl.simp_base
Proof state before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
h : ¬first < i
⊢ ↑first ≤ ↑i
Tactic:
assumption
Proof state after:
no goals
Theorem: partitionImpl.simp_base
Proof state before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
h : ¬first < i
⊢ partitionImpl arr first i j fi ij = (⟨j, ⋯⟩, arr)
Tactic:
unfold partitionImpl
Proof state after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
h : ¬first < i
⊢ (if h : first < i then
      let_fun this := ⋯;
      if arr[i] < arr[first] then
        let_fun this_1 := ⋯;
        partitionImpl arr first i.prev j this this_1
      else
        let arr := (dbgTraceIfShared "swap1" arr).swap i j;
        match partitionImpl arr first i.prev j.prev this ⋯ with
        | (⟨mid, hm⟩, arr) => (⟨mid, ⋯⟩, arr)
    else (⟨j, ⋯⟩, arr)) =
    (⟨j, ⋯⟩, arr)
Theorem: partitionImpl.simp_base
Proof state before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
h : ¬first < i
⊢ (if h : first < i then
      let_fun this := ⋯;
      if arr[i] < arr[first] then
        let_fun this_1 := ⋯;
        partitionImpl arr first i.prev j this this_1
      else
        let arr := (dbgTraceIfShared "swap1" arr).swap i j;
        match partitionImpl arr first i.prev j.prev this ⋯ with
        | (⟨mid, hm⟩, arr) => (⟨mid, ⋯⟩, arr)
    else (⟨j, ⋯⟩, arr)) =
    (⟨j, ⋯⟩, arr)
Tactic:
simp [*, dbgTraceIfShared]
Proof state after:
no goals
Theorem: partitionImpl.simp_step_lt
Proof state before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
h : first < i
x✝ : arr[i] < arr[first]
⊢ partitionImpl arr first i j fi ij = partitionImpl arr first i.prev j ⋯ ⋯
Tactic:
rw [partitionImpl]
Proof state after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
h : first < i
x✝ : arr[i] < arr[first]
⊢ (if h : first < i then
      let_fun this := ⋯;
      if arr[i] < arr[first] then
        let_fun this_1 := ⋯;
        partitionImpl arr first i.prev j this this_1
      else
        let arr := (dbgTraceIfShared "swap1" arr).swap i j;
        match partitionImpl arr first i.prev j.prev this ⋯ with
        | (⟨mid, hm⟩, arr) => (⟨mid, ⋯⟩, arr)
    else (⟨j, ⋯⟩, arr)) =
    partitionImpl arr first i.prev j ⋯ ⋯
Theorem: partitionImpl.simp_step_lt
Proof state before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
h : first < i
x✝ : arr[i] < arr[first]
⊢ (if h : first < i then
      let_fun this := ⋯;
      if arr[i] < arr[first] then
        let_fun this_1 := ⋯;
        partitionImpl arr first i.prev j this this_1
      else
        let arr := (dbgTraceIfShared "swap1" arr).swap i j;
        match partitionImpl arr first i.prev j.prev this ⋯ with
        | (⟨mid, hm⟩, arr) => (⟨mid, ⋯⟩, arr)
    else (⟨j, ⋯⟩, arr)) =
    partitionImpl arr first i.prev j ⋯ ⋯
Tactic:
simp [*]
Proof state after:
no goals
Theorem: partitionImpl.simp_step_ge
Proof state before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
h : first < i
x✝ : ¬arr[i] < arr[first]
⊢ partitionImpl arr first i j fi ij =
    match partitionImpl (arr.swap i j) first i.prev j.prev ⋯ ⋯ with
    | (⟨mid, hm⟩, arr) => (⟨mid, ⋯⟩, arr)
Tactic:
rw [partitionImpl]
Proof state after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
h : first < i
x✝ : ¬arr[i] < arr[first]
⊢ (if h : first < i then
      let_fun this := ⋯;
      if arr[i] < arr[first] then
        let_fun this_1 := ⋯;
        partitionImpl arr first i.prev j this this_1
      else
        let arr := (dbgTraceIfShared "swap1" arr).swap i j;
        match partitionImpl arr first i.prev j.prev this ⋯ with
        | (⟨mid, hm⟩, arr) => (⟨mid, ⋯⟩, arr)
    else (⟨j, ⋯⟩, arr)) =
    match partitionImpl (arr.swap i j) first i.prev j.prev ⋯ ⋯ with
    | (⟨mid, hm⟩, arr) => (⟨mid, ⋯⟩, arr)
Theorem: partitionImpl.simp_step_ge
Proof state before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
h : first < i
x✝ : ¬arr[i] < arr[first]
⊢ (if h : first < i then
      let_fun this := ⋯;
      if arr[i] < arr[first] then
        let_fun this_1 := ⋯;
        partitionImpl arr first i.prev j this this_1
      else
        let arr := (dbgTraceIfShared "swap1" arr).swap i j;
        match partitionImpl arr first i.prev j.prev this ⋯ with
        | (⟨mid, hm⟩, arr) => (⟨mid, ⋯⟩, arr)
    else (⟨j, ⋯⟩, arr)) =
    match partitionImpl (arr.swap i j) first i.prev j.prev ⋯ ⋯ with
    | (⟨mid, hm⟩, arr) => (⟨mid, ⋯⟩, arr)
Tactic:
simp [*, dbgTraceIfShared]
Proof state after:
no goals
Theorem: quickSortImpl.simp_base
Proof state before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
h : ¬first < ↑last
⊢ quickSortImpl arr first last = arr
Tactic:
unfold quickSortImpl
Proof state after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
h : ¬first < ↑last
⊢ (if lt : first < ↑last then
      let parted := partition arr ⟨first, ⋯⟩ last ⋯;
      let mid := parted.fst.val;
      let hm := ⋯;
      let arr_1 := parted.snd;
      let_fun this := ⋯;
      let_fun this_1 := ⋯;
      let arr_2 := quickSortImpl arr_1 first mid.prev;
      quickSortImpl arr_2 (↑mid + 1) last
    else arr) =
    arr
Theorem: quickSortImpl.simp_base
Proof state before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
h : ¬first < ↑last
⊢ (if lt : first < ↑last then
      let parted := partition arr ⟨first, ⋯⟩ last ⋯;
      let mid := parted.fst.val;
      let hm := ⋯;
      let arr_1 := parted.snd;
      let_fun this := ⋯;
      let_fun this_1 := ⋯;
      let arr_2 := quickSortImpl arr_1 first mid.prev;
      quickSortImpl arr_2 (↑mid + 1) last
    else arr) =
    arr
Tactic:
simp [*]
Proof state after:
no goals
Theorem: quickSortImpl.simp_step
Proof state before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
lt : first < ↑last
⊢ let parted := partition arr ⟨first, ⋯⟩ last ⋯;
  let mid := parted.fst.val;
  quickSortImpl arr first last = quickSortImpl (quickSortImpl parted.snd first mid.prev) (↑mid + 1) last
Tactic:
rw [quickSortImpl]
Proof state after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
lt : first < ↑last
⊢ let parted := partition arr ⟨first, ⋯⟩ last ⋯;
  let mid := parted.fst.val;
  (if lt : first < ↑last then
      let parted := partition arr ⟨first, ⋯⟩ last ⋯;
      let mid := parted.fst.val;
      let hm := ⋯;
      let arr_1 := parted.snd;
      let_fun this := ⋯;
      let_fun this_1 := ⋯;
      let arr_2 := quickSortImpl arr_1 first mid.prev;
      quickSortImpl arr_2 (↑mid + 1) last
    else arr) =
    quickSortImpl (quickSortImpl parted.snd first mid.prev) (↑mid + 1) last