internlm/Lean-Github huggingface dataset:
Theorem: Algdata.BinaryHeap.exists_get_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
hzk : ¬0 = k
⊢ ∃ k_1 hk, 0 < k_1 ∧ x[k] = x[k_1]
Tactic:
exists k, (Nat.lt_of_lt_of_le hk x.size.pred_le)
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
hzk : ¬0 = k
⊢ 0 < k ∧ x[k] = x[k]
Theorem: Algdata.BinaryHeap.exists_get_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
hzk : ¬0 = k
⊢ 0 < k ∧ x[k] = x[k]
Tactic:
exact ⟨Nat.pos_of_ne_zero (Ne.symm hzk), rfl⟩
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.mk
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
⊢ loop.OpSpec lt x n (loop lt x n)
Tactic:
induction n generalizing x with
| zero => exact .zero x
| succ n IH => exact .succ <| IH (popMax lt x)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.mk
Proof state before:
case zero
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ loop.OpSpec lt x Nat.zero (loop lt x Nat.zero)
Tactic:
exact .zero x
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.mk
Proof state before:
case succ
α : Type u
lt : α → α → Bool
n : Nat
IH : ∀ (x : Subarray α), loop.OpSpec lt x n (loop lt x n)
x : Subarray α
⊢ loop.OpSpec lt x (Nat.succ n) (loop lt x (Nat.succ n))
Tactic:
exact .succ <| IH (popMax lt x)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.to_eq
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt x n y
⊢ y = loop lt x n
Tactic:
induction h with
| zero => rfl
| succ h IH => rw [IH]; rfl
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.to_eq
Proof state before:
case zero
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
x✝ : Subarray α
⊢ x✝.as = loop lt x✝ 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.to_eq
Proof state before:
case succ
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
h : loop.OpSpec lt (popMax lt x✝) n✝ y✝
IH : y✝ = loop lt (popMax lt x✝) n✝
⊢ y✝ = loop lt x✝ (n✝ + 1)
Tactic:
rw [IH]
Proof state after:
case succ
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
h : loop.OpSpec lt (popMax lt x✝) n✝ y✝
IH : y✝ = loop lt (popMax lt x✝) n✝
⊢ loop lt (popMax lt x✝) n✝ = loop lt x✝ (n✝ + 1)
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.to_eq
Proof state before:
case succ
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
h : loop.OpSpec lt (popMax lt x✝) n✝ y✝
IH : y✝ = loop lt (popMax lt x✝) n✝
⊢ loop lt (popMax lt x✝) n✝ = loop lt x✝ (n✝ + 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.size_eq
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt x n y
⊢ Array.size y = Array.size x.as
Tactic:
induction h with
| zero => rfl
| succ h IH => rw [IH, size_as_popMax]
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.size_eq
Proof state before:
case zero
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
x✝ : Subarray α
⊢ Array.size x✝.as = Array.size x✝.as
Tactic:
rfl
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.size_eq
Proof state before:
case succ
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
h : loop.OpSpec lt (popMax lt x✝) n✝ y✝
IH : Array.size y✝ = Array.size (popMax lt x✝).as
⊢ Array.size y✝ = Array.size x✝.as
Tactic:
rw [IH, size_as_popMax]
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.get_eq_of_lt_start
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt x n y
i : Nat
hi : i < Array.size y
hlt : i < x.start
⊢ y[i] = x.as[i]
Tactic:
induction h with
| zero => rfl
| @succ x n y h IH =>
  specialize @IH hi <| start_popMax lt x ▸ hlt
  exact Eq.trans IH <| get_as_popMax_of_lt_start lt x i hlt
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.get_eq_of_lt_start
Proof state before:
case zero
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
i : Nat
x✝ : Subarray α
hi : i < Array.size x✝.as
hlt : i < x✝.start
⊢ x✝.as[i] = x✝.as[i]
Tactic:
rfl
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.get_eq_of_lt_start
Proof state before:
case succ
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
IH : ∀ {hi : i < Array.size y}, i < (popMax lt x).start → y[i] = (popMax lt x).as[i]
hi : i < Array.size y
hlt : i < x.start
⊢ y[i] = x.as[i]
Tactic:
specialize @IH hi <| start_popMax lt x ▸ hlt
Proof state after:
case succ
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
hi : i < Array.size y
hlt : i < x.start
IH : y[i] = (popMax lt x).as[i]
⊢ y[i] = x.as[i]
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.get_eq_of_lt_start
Proof state before:
case succ
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
hi : i < Array.size y
hlt : i < x.start
IH : y[i] = (popMax lt x).as[i]
⊢ y[i] = x.as[i]
Tactic:
exact Eq.trans IH <| get_as_popMax_of_lt_start lt x i hlt
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.get_eq_of_ge_stop
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt x n y
i : Nat
hi : i < Array.size y
hge : i ≥ x.stop
⊢ y[i] = x.as[i]
Tactic:
induction h with
| zero => rfl
| @succ x n y h IH =>
  specialize @IH hi <| Nat.le_trans (stop_popMax_le_stop lt x) hge
  exact Eq.trans IH <| get_as_popMax_of_ge_stop lt x i hge
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.get_eq_of_ge_stop
Proof state before:
case zero
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
i : Nat
x✝ : Subarray α
hi : i < Array.size x✝.as
hge : i ≥ x✝.stop
⊢ x✝.as[i] = x✝.as[i]
Tactic:
rfl
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.get_eq_of_ge_stop
Proof state before:
case succ
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
IH : ∀ {hi : i < Array.size y}, i ≥ (popMax lt x).stop → y[i] = (popMax lt x).as[i]
hi : i < Array.size y
hge : i ≥ x.stop
⊢ y[i] = x.as[i]
Tactic:
specialize @IH hi <| Nat.le_trans (stop_popMax_le_stop lt x) hge
Proof state after:
case succ
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
hi : i < Array.size y
hge : i ≥ x.stop
IH : y[i] = (popMax lt x).as[i]
⊢ y[i] = x.as[i]
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.get_eq_of_ge_stop
Proof state before:
case succ
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
hi : i < Array.size y
hge : i ≥ x.stop
IH : y[i] = (popMax lt x).as[i]
⊢ y[i] = x.as[i]
Tactic:
exact Eq.trans IH <| get_as_popMax_of_ge_stop lt x i hge
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.exists_get
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt x n y
i : Nat
ge_start : x.start ≤ i
lt_stop : i < x.stop
⊢ ∃ k hk, y[i] = x[k]
Tactic:
induction h with
| @zero x =>
  let k := i - x.start
  have hki : i = x.start + k := by
    rw [Nat.add_comm, Nat.sub_add_cancel ge_start]
  have hk : k < x.size := by
    refine Nat.lt_sub_of_add_lt ?_
    simp only [Nat.sub_add_cancel ge_start]
    exact lt_stop
  exists k, hk
  exact getElem_eq (x:=x.as) (y:=x.as) rfl hki
| @succ x n y h IH =>
  specialize IH (start_popMax lt x ▸ ge_start)
  have hrng : x.start < x.stop := trans ge_start lt_stop
  cases Nat.lt_or_eq_of_le (Nat.le_pred_of_lt lt_stop) with
  | inl hlt =>
    have ⟨k,hk,hy⟩ := IH (stop_popMax lt x hrng ▸ hlt)
    have ⟨l,hl,_,hx⟩ := exists_get_popMax lt x k (size_popMax lt x ▸ hk)
    simp only [hy, hx]
    exact ⟨l, hl, rfl⟩
  | inr heq =>
    cases heq
    rewrite [h.get_eq_of_ge_stop (x.stop-1) (stop_popMax lt x hrng ▸ .refl)]
    rewrite [get_as_popMax_stop_sub_one lt x hrng]
    exact ⟨0, Nat.zero_lt_sub_of_lt hrng, rfl⟩
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.exists_get
Proof state before:
case zero
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n : Nat
y : Array α
i : Nat
x : Subarray α
ge_start : x.start ≤ i
lt_stop : i < x.stop
⊢ ∃ k hk, x.as[i] = x[k]
Tactic:
let k := i - x.start
Proof state after:
case zero
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n : Nat
y : Array α
i : Nat
x : Subarray α
ge_start : x.start ≤ i
lt_stop : i < x.stop
k : Nat := i - x.start
⊢ ∃ k hk, x.as[i] = x[k]
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.exists_get
Proof state before:
case zero
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n : Nat
y : Array α
i : Nat
x : Subarray α
ge_start : x.start ≤ i
lt_stop : i < x.stop
k : Nat := i - x.start
⊢ ∃ k hk, x.as[i] = x[k]
Tactic:
have hki : i = x.start + k := by
  rw [Nat.add_comm, Nat.sub_add_cancel ge_start]
Proof state after:
case zero
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n : Nat
y : Array α
i : Nat
x : Subarray α
ge_start : x.start ≤ i
lt_stop : i < x.stop
k : Nat := i - x.start
hki : i = x.start + k
⊢ ∃ k hk, x.as[i] = x[k]
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.exists_get
Proof state before:
case zero
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n : Nat
y : Array α
i : Nat
x : Subarray α
ge_start : x.start ≤ i
lt_stop : i < x.stop
k : Nat := i - x.start
hki : i = x.start + k
⊢ ∃ k hk, x.as[i] = x[k]
Tactic:
have hk : k < x.size := by
  refine Nat.lt_sub_of_add_lt ?_
  simp only [Nat.sub_add_cancel ge_start]
  exact lt_stop
Proof state after:
case zero
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n : Nat
y : Array α
i : Nat
x : Subarray α
ge_start : x.start ≤ i
lt_stop : i < x.stop
k : Nat := i - x.start
hki : i = x.start + k
hk : k < Subarray.size x
⊢ ∃ k hk, x.as[i] = x[k]
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.exists_get
Proof state before:
case zero
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n : Nat
y : Array α
i : Nat
x : Subarray α
ge_start : x.start ≤ i
lt_stop : i < x.stop
k : Nat := i - x.start
hki : i = x.start + k
hk : k < Subarray.size x
⊢ ∃ k hk, x.as[i] = x[k]
Tactic:
exists k, hk
Proof state after:
case zero
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n : Nat
y : Array α
i : Nat
x : Subarray α
ge_start : x.start ≤ i
lt_stop : i < x.stop
k : Nat := i - x.start
hki : i = x.start + k
hk : k < Subarray.size x
⊢ x.as[i] = x[k]
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.exists_get
Proof state before:
case zero
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n : Nat
y : Array α
i : Nat
x : Subarray α
ge_start : x.start ≤ i
lt_stop : i < x.stop
k : Nat := i - x.start
hki : i = x.start + k
hk : k < Subarray.size x
⊢ x.as[i] = x[k]
Tactic:
exact getElem_eq (x:=x.as) (y:=x.as) rfl hki
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.exists_get
Proof state before:
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n : Nat
y : Array α
i : Nat
x : Subarray α
ge_start : x.start ≤ i
lt_stop : i < x.stop
k : Nat := i - x.start
⊢ i = x.start + k
Tactic:
rw [Nat.add_comm, Nat.sub_add_cancel ge_start]
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.exists_get
Proof state before:
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n : Nat
y : Array α
i : Nat
x : Subarray α
ge_start : x.start ≤ i
lt_stop : i < x.stop
k : Nat := i - x.start
hki : i = x.start + k
⊢ k < Subarray.size x
Tactic:
refine Nat.lt_sub_of_add_lt ?_
Proof state after:
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n : Nat
y : Array α
i : Nat
x : Subarray α
ge_start : x.start ≤ i
lt_stop : i < x.stop
k : Nat := i - x.start
hki : i = x.start + k
⊢ k + x.start < x.stop
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.exists_get
Proof state before:
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n : Nat
y : Array α
i : Nat
x : Subarray α
ge_start : x.start ≤ i
lt_stop : i < x.stop
k : Nat := i - x.start
hki : i = x.start + k
⊢ k + x.start < x.stop
Tactic:
simp only [Nat.sub_add_cancel ge_start]
Proof state after:
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n : Nat
y : Array α
i : Nat
x : Subarray α
ge_start : x.start ≤ i
lt_stop : i < x.stop
k : Nat := i - x.start
hki : i = x.start + k
⊢ i < x.stop
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.exists_get
Proof state before:
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n : Nat
y : Array α
i : Nat
x : Subarray α
ge_start : x.start ≤ i
lt_stop : i < x.stop
k : Nat := i - x.start
hki : i = x.start + k
⊢ i < x.stop
Tactic:
exact lt_stop
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.exists_get
Proof state before:
case succ
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
IH : (popMax lt x).start ≤ i → ∀ (lt_stop : i < (popMax lt x).stop), ∃ k hk, y[i] = (popMax lt x)[k]
ge_start : x.start ≤ i
lt_stop : i < x.stop
⊢ ∃ k hk, y[i] = x[k]
Tactic:
specialize IH (start_popMax lt x ▸ ge_start)
Proof state after:
case succ
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
ge_start : x.start ≤ i
lt_stop : i < x.stop
IH : ∀ (lt_stop : i < (popMax lt x).stop), ∃ k hk, y[i] = (popMax lt x)[k]
⊢ ∃ k hk, y[i] = x[k]
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.exists_get
Proof state before:
case succ
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
ge_start : x.start ≤ i
lt_stop : i < x.stop
IH : ∀ (lt_stop : i < (popMax lt x).stop), ∃ k hk, y[i] = (popMax lt x)[k]
⊢ ∃ k hk, y[i] = x[k]
Tactic:
have hrng : x.start < x.stop := trans ge_start lt_stop
Proof state after:
case succ
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
ge_start : x.start ≤ i
lt_stop : i < x.stop
IH : ∀ (lt_stop : i < (popMax lt x).stop), ∃ k hk, y[i] = (popMax lt x)[k]
hrng : x.start < x.stop
⊢ ∃ k hk, y[i] = x[k]
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.exists_get
Proof state before:
case succ
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
ge_start : x.start ≤ i
lt_stop : i < x.stop
IH : ∀ (lt_stop : i < (popMax lt x).stop), ∃ k hk, y[i] = (popMax lt x)[k]
hrng : x.start < x.stop
⊢ ∃ k hk, y[i] = x[k]
Tactic:
cases Nat.lt_or_eq_of_le (Nat.le_pred_of_lt lt_stop) with
| inl hlt =>
  have ⟨k,hk,hy⟩ := IH (stop_popMax lt x hrng ▸ hlt)
  have ⟨l,hl,_,hx⟩ := exists_get_popMax lt x k (size_popMax lt x ▸ hk)
  simp only [hy, hx]
  exact ⟨l, hl, rfl⟩
| inr heq =>
  cases heq
  rewrite [h.get_eq_of_ge_stop (x.stop-1) (stop_popMax lt x hrng ▸ .refl)]
  rewrite [get_as_popMax_stop_sub_one lt x hrng]
  exact ⟨0, Nat.zero_lt_sub_of_lt hrng, rfl⟩
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.exists_get
Proof state before:
case succ.inl
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
ge_start : x.start ≤ i
lt_stop : i < x.stop
IH : ∀ (lt_stop : i < (popMax lt x).stop), ∃ k hk, y[i] = (popMax lt x)[k]
hrng : x.start < x.stop
hlt : i < x.stop - 1
⊢ ∃ k hk, y[i] = x[k]
Tactic:
have ⟨k,hk,hy⟩ := IH (stop_popMax lt x hrng ▸ hlt)
Proof state after:
case succ.inl
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
ge_start : x.start ≤ i
lt_stop : i < x.stop
IH : ∀ (lt_stop : i < (popMax lt x).stop), ∃ k hk, y[i] = (popMax lt x)[k]
hrng : x.start < x.stop
hlt : i < x.stop - 1
k : Nat
hk : k < Subarray.size (popMax lt x)
hy : y[i] = (popMax lt x)[k]
⊢ ∃ k hk, y[i] = x[k]
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.exists_get
Proof state before:
case succ.inl
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
ge_start : x.start ≤ i
lt_stop : i < x.stop
IH : ∀ (lt_stop : i < (popMax lt x).stop), ∃ k hk, y[i] = (popMax lt x)[k]
hrng : x.start < x.stop
hlt : i < x.stop - 1
k : Nat
hk : k < Subarray.size (popMax lt x)
hy : y[i] = (popMax lt x)[k]
⊢ ∃ k hk, y[i] = x[k]
Tactic:
have ⟨l,hl,_,hx⟩ := exists_get_popMax lt x k (size_popMax lt x ▸ hk)
Proof state after:
case succ.inl
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
ge_start : x.start ≤ i
lt_stop : i < x.stop
IH : ∀ (lt_stop : i < (popMax lt x).stop), ∃ k hk, y[i] = (popMax lt x)[k]
hrng : x.start < x.stop
hlt : i < x.stop - 1
k : Nat
hk : k < Subarray.size (popMax lt x)
hy : y[i] = (popMax lt x)[k]
l : Nat
hl : l < Subarray.size x
left✝ : 0 < l
hx : (popMax lt x)[k] = x[l]
⊢ ∃ k hk, y[i] = x[k]
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.exists_get
Proof state before:
case succ.inl
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
ge_start : x.start ≤ i
lt_stop : i < x.stop
IH : ∀ (lt_stop : i < (popMax lt x).stop), ∃ k hk, y[i] = (popMax lt x)[k]
hrng : x.start < x.stop
hlt : i < x.stop - 1
k : Nat
hk : k < Subarray.size (popMax lt x)
hy : y[i] = (popMax lt x)[k]
l : Nat
hl : l < Subarray.size x
left✝ : 0 < l
hx : (popMax lt x)[k] = x[l]
⊢ ∃ k hk, y[i] = x[k]
Tactic:
simp only [hy, hx]
Proof state after:
case succ.inl
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
ge_start : x.start ≤ i
lt_stop : i < x.stop
IH : ∀ (lt_stop : i < (popMax lt x).stop), ∃ k hk, y[i] = (popMax lt x)[k]
hrng : x.start < x.stop
hlt : i < x.stop - 1
k : Nat
hk : k < Subarray.size (popMax lt x)
hy : y[i] = (popMax lt x)[k]
l : Nat
hl : l < Subarray.size x
left✝ : 0 < l
hx : (popMax lt x)[k] = x[l]
⊢ ∃ k hk, x[l] = x[k]
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.exists_get
Proof state before:
case succ.inl
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
ge_start : x.start ≤ i
lt_stop : i < x.stop
IH : ∀ (lt_stop : i < (popMax lt x).stop), ∃ k hk, y[i] = (popMax lt x)[k]
hrng : x.start < x.stop
hlt : i < x.stop - 1
k : Nat
hk : k < Subarray.size (popMax lt x)
hy : y[i] = (popMax lt x)[k]
l : Nat
hl : l < Subarray.size x
left✝ : 0 < l
hx : (popMax lt x)[k] = x[l]
⊢ ∃ k hk, x[l] = x[k]
Tactic:
exact ⟨l, hl, rfl⟩
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.exists_get
Proof state before:
case succ.inr
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
ge_start : x.start ≤ i
lt_stop : i < x.stop
IH : ∀ (lt_stop : i < (popMax lt x).stop), ∃ k hk, y[i] = (popMax lt x)[k]
hrng : x.start < x.stop
heq : i = x.stop - 1
⊢ ∃ k hk, y[i] = x[k]
Tactic:
cases heq
Proof state after:
case succ.inr.refl
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
hrng : x.start < x.stop
ge_start : x.start ≤ x.stop - 1
lt_stop : x.stop - 1 < x.stop
IH : ∀ (lt_stop : x.stop - 1 < (popMax lt x).stop), ∃ k hk, y[x.stop - 1] = (popMax lt x)[k]
⊢ ∃ k hk, y[x.stop - 1] = x[k]
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.exists_get
Proof state before:
case succ.inr.refl
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
hrng : x.start < x.stop
ge_start : x.start ≤ x.stop - 1
lt_stop : x.stop - 1 < x.stop
IH : ∀ (lt_stop : x.stop - 1 < (popMax lt x).stop), ∃ k hk, y[x.stop - 1] = (popMax lt x)[k]
⊢ ∃ k hk, y[x.stop - 1] = x[k]
Tactic:
rewrite [h.get_eq_of_ge_stop (x.stop-1) (stop_popMax lt x hrng ▸ .refl)]
Proof state after:
case succ.inr.refl
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
hrng : x.start < x.stop
ge_start : x.start ≤ x.stop - 1
lt_stop : x.stop - 1 < x.stop
IH : ∀ (lt_stop : x.stop - 1 < (popMax lt x).stop), ∃ k hk, y[x.stop - 1] = (popMax lt x)[k]
⊢ ∃ k hk, (popMax lt x).as[x.stop - 1] = x[k]
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.exists_get
Proof state before:
case succ.inr.refl
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
hrng : x.start < x.stop
ge_start : x.start ≤ x.stop - 1
lt_stop : x.stop - 1 < x.stop
IH : ∀ (lt_stop : x.stop - 1 < (popMax lt x).stop), ∃ k hk, y[x.stop - 1] = (popMax lt x)[k]
⊢ ∃ k hk, (popMax lt x).as[x.stop - 1] = x[k]
Tactic:
rewrite [get_as_popMax_stop_sub_one lt x hrng]
Proof state after:
case succ.inr.refl
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
hrng : x.start < x.stop
ge_start : x.start ≤ x.stop - 1
lt_stop : x.stop - 1 < x.stop
IH : ∀ (lt_stop : x.stop - 1 < (popMax lt x).stop), ∃ k hk, y[x.stop - 1] = (popMax lt x)[k]
⊢ ∃ k hk, x[0] = x[k]
Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.exists_get
Proof state before:
case succ.inr.refl
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
hrng : x.start < x.stop
ge_start : x.start ≤ x.stop - 1
lt_stop : x.stop - 1 < x.stop
IH : ∀ (lt_stop : x.stop - 1 < (popMax lt x).stop), ∃ k hk, y[x.stop - 1] = (popMax lt x)[k]
⊢ ∃ k hk, x[0] = x[k]
Tactic:
exact ⟨0, Nat.zero_lt_sub_of_lt hrng, rfl⟩
Proof state after:
no goals
Theorem: List.Ascending.head
Proof state before:
α : Type u
r : α → α → Prop
a : α
as : List α
⊢ Ascending r (a :: as) → predHead (r a) as
Tactic:
intro hchain
Proof state after:
α : Type u
r : α → α → Prop
a : α
as : List α
hchain : Ascending r (a :: as)
⊢ predHead (r a) as
Theorem: List.Ascending.head
Proof state before:
α : Type u
r : α → α → Prop
a : α
as : List α
hchain : Ascending r (a :: as)
⊢ predHead (r a) as
Tactic:
cases hchain
Proof state after:
case singleton
α : Type u
r : α → α → Prop
a : α
⊢ predHead (r a) []

case cons
α : Type u
r : α → α → Prop
a b✝ : α
bs✝ : List α
a✝¹ : Ascending r (b✝ :: bs✝)
a✝ : r a b✝
⊢ predHead (r a) (b✝ :: bs✝)
Theorem: List.Ascending.head
Proof state before:
α : Type u
r : α → α → Prop
a : α
⊢ predHead (r a) []
Tactic:
case singleton => exact True.intro
Proof state after:
no goals