internlm/Lean-Github huggingface dataset:
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h✝ : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i k : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i ∧ i < stop
hk : k < Subarray.size (BinaryHeap.popMax lt x)
k' : Nat
hk' : k' < Subarray.size x
left✝ : 0 < k'
h : (BinaryHeap.popMax lt x)[k] = x[k']
⊢ lt (BinaryHeap.popMax lt x).as[i] x[k'] = false
Tactic:
clear h
Proof state after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i k : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i ∧ i < stop
hk : k < Subarray.size (BinaryHeap.popMax lt x)
k' : Nat
hk' : k' < Subarray.size x
left✝ : 0 < k'
⊢ lt (BinaryHeap.popMax lt x).as[i] x[k'] = false
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i k : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i ∧ i < stop
hk : k < Subarray.size (BinaryHeap.popMax lt x)
k' : Nat
hk' : k' < Subarray.size x
left✝ : 0 < k'
⊢ lt (BinaryHeap.popMax lt x).as[i] x[k'] = false
Tactic:
have hrng : x.start < x.stop :=
  trans (x.start.le_add_left k') (Nat.add_lt_of_lt_sub hk')
Proof state after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i k : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i ∧ i < stop
hk : k < Subarray.size (BinaryHeap.popMax lt x)
k' : Nat
hk' : k' < Subarray.size x
left✝ : 0 < k'
hrng : x.start < x.stop
⊢ lt (BinaryHeap.popMax lt x).as[i] x[k'] = false
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i k : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i ∧ i < stop
hk : k < Subarray.size (BinaryHeap.popMax lt x)
k' : Nat
hk' : k' < Subarray.size x
left✝ : 0 < k'
hrng : x.start < x.stop
⊢ lt (BinaryHeap.popMax lt x).as[i] x[k'] = false
Tactic:
have hi' : x.stop - 1 ≤ i :=
  stop_popMax lt x hrng ▸ hi.1
Proof state after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i k : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i ∧ i < stop
hk : k < Subarray.size (BinaryHeap.popMax lt x)
k' : Nat
hk' : k' < Subarray.size x
left✝ : 0 < k'
hrng : x.start < x.stop
hi' : x.stop - 1 ≤ i
⊢ lt (BinaryHeap.popMax lt x).as[i] x[k'] = false
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i k : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i ∧ i < stop
hk : k < Subarray.size (BinaryHeap.popMax lt x)
k' : Nat
hk' : k' < Subarray.size x
left✝ : 0 < k'
hrng : x.start < x.stop
hi' : x.stop - 1 ≤ i
⊢ lt (BinaryHeap.popMax lt x).as[i] x[k'] = false
Tactic:
cases Nat.lt_or_eq_of_le hi' with
| inl hlt =>
  have hi' : x.stop ≤ i :=
    Nat.sub_add_cancel (trans x.start.zero_le hrng :) ▸ hlt
  rewrite [get_as_popMax_of_ge_stop lt x i hi']
  exact h.bound_above i k' ⟨hi',hi.2⟩ hk'
| inr heq =>
  cases heq
  rewrite [get_as_popMax_stop_sub_one lt x hrng]
  exact h.is_heap.not_lt_of_descendant k' (.root k')
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
case inl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i k : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i ∧ i < stop
hk : k < Subarray.size (BinaryHeap.popMax lt x)
k' : Nat
hk' : k' < Subarray.size x
left✝ : 0 < k'
hrng : x.start < x.stop
hi' : x.stop - 1 ≤ i
hlt : x.stop - 1 < i
⊢ lt (BinaryHeap.popMax lt x).as[i] x[k'] = false
Tactic:
have hi' : x.stop ≤ i :=
  Nat.sub_add_cancel (trans x.start.zero_le hrng :) ▸ hlt
Proof state after:
case inl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i k : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i ∧ i < stop
hk : k < Subarray.size (BinaryHeap.popMax lt x)
k' : Nat
hk' : k' < Subarray.size x
left✝ : 0 < k'
hrng : x.start < x.stop
hi'✝ : x.stop - 1 ≤ i
hlt : x.stop - 1 < i
hi' : x.stop ≤ i
⊢ lt (BinaryHeap.popMax lt x).as[i] x[k'] = false
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
case inl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i k : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i ∧ i < stop
hk : k < Subarray.size (BinaryHeap.popMax lt x)
k' : Nat
hk' : k' < Subarray.size x
left✝ : 0 < k'
hrng : x.start < x.stop
hi'✝ : x.stop - 1 ≤ i
hlt : x.stop - 1 < i
hi' : x.stop ≤ i
⊢ lt (BinaryHeap.popMax lt x).as[i] x[k'] = false
Tactic:
rewrite [get_as_popMax_of_ge_stop lt x i hi']
Proof state after:
case inl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i k : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i ∧ i < stop
hk : k < Subarray.size (BinaryHeap.popMax lt x)
k' : Nat
hk' : k' < Subarray.size x
left✝ : 0 < k'
hrng : x.start < x.stop
hi'✝ : x.stop - 1 ≤ i
hlt : x.stop - 1 < i
hi' : x.stop ≤ i
⊢ lt x.as[i] x[k'] = false
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
case inl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i k : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i ∧ i < stop
hk : k < Subarray.size (BinaryHeap.popMax lt x)
k' : Nat
hk' : k' < Subarray.size x
left✝ : 0 < k'
hrng : x.start < x.stop
hi'✝ : x.stop - 1 ≤ i
hlt : x.stop - 1 < i
hi' : x.stop ≤ i
⊢ lt x.as[i] x[k'] = false
Tactic:
exact h.bound_above i k' ⟨hi',hi.2⟩ hk'
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
case inr
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i k : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i ∧ i < stop
hk : k < Subarray.size (BinaryHeap.popMax lt x)
k' : Nat
hk' : k' < Subarray.size x
left✝ : 0 < k'
hrng : x.start < x.stop
hi' : x.stop - 1 ≤ i
heq : x.stop - 1 = i
⊢ lt (BinaryHeap.popMax lt x).as[i] x[k'] = false
Tactic:
cases heq
Proof state after:
case inr.refl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
k : Nat
hk : k < Subarray.size (BinaryHeap.popMax lt x)
k' : Nat
hk' : k' < Subarray.size x
left✝ : 0 < k'
hrng : x.start < x.stop
hi : (BinaryHeap.popMax lt x).stop ≤ x.stop - 1 ∧ x.stop - 1 < stop
hi' : x.stop - 1 ≤ x.stop - 1
⊢ lt (BinaryHeap.popMax lt x).as[x.stop - 1] x[k'] = false
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
case inr.refl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
k : Nat
hk : k < Subarray.size (BinaryHeap.popMax lt x)
k' : Nat
hk' : k' < Subarray.size x
left✝ : 0 < k'
hrng : x.start < x.stop
hi : (BinaryHeap.popMax lt x).stop ≤ x.stop - 1 ∧ x.stop - 1 < stop
hi' : x.stop - 1 ≤ x.stop - 1
⊢ lt (BinaryHeap.popMax lt x).as[x.stop - 1] x[k'] = false
Tactic:
rewrite [get_as_popMax_stop_sub_one lt x hrng]
Proof state after:
case inr.refl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
k : Nat
hk : k < Subarray.size (BinaryHeap.popMax lt x)
k' : Nat
hk' : k' < Subarray.size x
left✝ : 0 < k'
hrng : x.start < x.stop
hi : (BinaryHeap.popMax lt x).stop ≤ x.stop - 1 ∧ x.stop - 1 < stop
hi' : x.stop - 1 ≤ x.stop - 1
⊢ lt x[0] x[k'] = false
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
case inr.refl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
k : Nat
hk : k < Subarray.size (BinaryHeap.popMax lt x)
k' : Nat
hk' : k' < Subarray.size x
left✝ : 0 < k'
hrng : x.start < x.stop
hi : (BinaryHeap.popMax lt x).stop ≤ x.stop - 1 ∧ x.stop - 1 < stop
hi' : x.stop - 1 ≤ x.stop - 1
⊢ lt x[0] x[k'] = false
Tactic:
exact h.is_heap.not_lt_of_descendant k' (.root k')
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i
hij : i < j
hj : j < stop
⊢ lt (BinaryHeap.popMax lt x).as[j] (BinaryHeap.popMax lt x).as[i] = false
Tactic:
cases Nat.lt_or_eq_of_le x.h₁ with
| inl hrng =>
  simp only [stop_popMax lt x hrng] at hi
  have stop_pos : 0 < x.stop :=
    Nat.lt_of_le_of_lt x.start.zero_le hrng
  have : x.stop-1+1 = x.stop :=
    Nat.sub_add_cancel stop_pos
  have hj' : x.stop ≤ j :=
    trans this.symm (trans hi hij :)
  rewrite [get_as_popMax_of_ge_stop lt x j hj']
  cases Nat.lt_or_eq_of_le hi with
  | inl hlti =>
    have : x.stop ≤ i :=
      ‹x.stop-1+1=x.stop› ▸ (hlti : x.stop-1+1 ≤ i)
    rewrite [get_as_popMax_of_ge_stop lt x i this]
    exact h.sorted i j this hij hj
  | inr heqi =>
    cases heqi
    rewrite [get_as_popMax_stop_sub_one lt x hrng]
    exact h.bound_above j 0 ⟨hj',hj⟩ _
| inr hz =>
  simp only [popMax_empty lt x hz] at hi ⊢
  exact h.sorted i j hi hij hj
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
case inl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i
hij : i < j
hj : j < stop
hrng : x.start < x.stop
⊢ lt (BinaryHeap.popMax lt x).as[j] (BinaryHeap.popMax lt x).as[i] = false
Tactic:
simp only [stop_popMax lt x hrng] at hi
Proof state after:
case inl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hij : i < j
hj : j < stop
hrng : x.start < x.stop
hi : x.stop - 1 ≤ i
⊢ lt (BinaryHeap.popMax lt x).as[j] (BinaryHeap.popMax lt x).as[i] = false
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
case inl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hij : i < j
hj : j < stop
hrng : x.start < x.stop
hi : x.stop - 1 ≤ i
⊢ lt (BinaryHeap.popMax lt x).as[j] (BinaryHeap.popMax lt x).as[i] = false
Tactic:
have stop_pos : 0 < x.stop :=
  Nat.lt_of_le_of_lt x.start.zero_le hrng
Proof state after:
case inl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hij : i < j
hj : j < stop
hrng : x.start < x.stop
hi : x.stop - 1 ≤ i
stop_pos : 0 < x.stop
⊢ lt (BinaryHeap.popMax lt x).as[j] (BinaryHeap.popMax lt x).as[i] = false
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
case inl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hij : i < j
hj : j < stop
hrng : x.start < x.stop
hi : x.stop - 1 ≤ i
stop_pos : 0 < x.stop
⊢ lt (BinaryHeap.popMax lt x).as[j] (BinaryHeap.popMax lt x).as[i] = false
Tactic:
have : x.stop-1+1 = x.stop :=
  Nat.sub_add_cancel stop_pos
Proof state after:
case inl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hij : i < j
hj : j < stop
hrng : x.start < x.stop
hi : x.stop - 1 ≤ i
stop_pos : 0 < x.stop
this : x.stop - 1 + 1 = x.stop
⊢ lt (BinaryHeap.popMax lt x).as[j] (BinaryHeap.popMax lt x).as[i] = false
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
case inl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hij : i < j
hj : j < stop
hrng : x.start < x.stop
hi : x.stop - 1 ≤ i
stop_pos : 0 < x.stop
this : x.stop - 1 + 1 = x.stop
⊢ lt (BinaryHeap.popMax lt x).as[j] (BinaryHeap.popMax lt x).as[i] = false
Tactic:
have hj' : x.stop ≤ j :=
  trans this.symm (trans hi hij :)
Proof state after:
case inl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hij : i < j
hj : j < stop
hrng : x.start < x.stop
hi : x.stop - 1 ≤ i
stop_pos : 0 < x.stop
this : x.stop - 1 + 1 = x.stop
hj' : x.stop ≤ j
⊢ lt (BinaryHeap.popMax lt x).as[j] (BinaryHeap.popMax lt x).as[i] = false
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
case inl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hij : i < j
hj : j < stop
hrng : x.start < x.stop
hi : x.stop - 1 ≤ i
stop_pos : 0 < x.stop
this : x.stop - 1 + 1 = x.stop
hj' : x.stop ≤ j
⊢ lt (BinaryHeap.popMax lt x).as[j] (BinaryHeap.popMax lt x).as[i] = false
Tactic:
rewrite [get_as_popMax_of_ge_stop lt x j hj']
Proof state after:
case inl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hij : i < j
hj : j < stop
hrng : x.start < x.stop
hi : x.stop - 1 ≤ i
stop_pos : 0 < x.stop
this : x.stop - 1 + 1 = x.stop
hj' : x.stop ≤ j
⊢ lt x.as[j] (BinaryHeap.popMax lt x).as[i] = false
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
case inl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hij : i < j
hj : j < stop
hrng : x.start < x.stop
hi : x.stop - 1 ≤ i
stop_pos : 0 < x.stop
this : x.stop - 1 + 1 = x.stop
hj' : x.stop ≤ j
⊢ lt x.as[j] (BinaryHeap.popMax lt x).as[i] = false
Tactic:
cases Nat.lt_or_eq_of_le hi with
| inl hlti =>
  have : x.stop ≤ i :=
    ‹x.stop-1+1=x.stop› ▸ (hlti : x.stop-1+1 ≤ i)
  rewrite [get_as_popMax_of_ge_stop lt x i this]
  exact h.sorted i j this hij hj
| inr heqi =>
  cases heqi
  rewrite [get_as_popMax_stop_sub_one lt x hrng]
  exact h.bound_above j 0 ⟨hj',hj⟩ _
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
case inl.inl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hij : i < j
hj : j < stop
hrng : x.start < x.stop
hi : x.stop - 1 ≤ i
stop_pos : 0 < x.stop
this : x.stop - 1 + 1 = x.stop
hj' : x.stop ≤ j
hlti : x.stop - 1 < i
⊢ lt x.as[j] (BinaryHeap.popMax lt x).as[i] = false
Tactic:
have : x.stop ≤ i :=
  ‹x.stop-1+1=x.stop› ▸ (hlti : x.stop-1+1 ≤ i)
Proof state after:
case inl.inl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hij : i < j
hj : j < stop
hrng : x.start < x.stop
hi : x.stop - 1 ≤ i
stop_pos : 0 < x.stop
this✝ : x.stop - 1 + 1 = x.stop
hj' : x.stop ≤ j
hlti : x.stop - 1 < i
this : x.stop ≤ i
⊢ lt x.as[j] (BinaryHeap.popMax lt x).as[i] = false
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
case inl.inl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hij : i < j
hj : j < stop
hrng : x.start < x.stop
hi : x.stop - 1 ≤ i
stop_pos : 0 < x.stop
this✝ : x.stop - 1 + 1 = x.stop
hj' : x.stop ≤ j
hlti : x.stop - 1 < i
this : x.stop ≤ i
⊢ lt x.as[j] (BinaryHeap.popMax lt x).as[i] = false
Tactic:
rewrite [get_as_popMax_of_ge_stop lt x i this]
Proof state after:
case inl.inl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hij : i < j
hj : j < stop
hrng : x.start < x.stop
hi : x.stop - 1 ≤ i
stop_pos : 0 < x.stop
this✝ : x.stop - 1 + 1 = x.stop
hj' : x.stop ≤ j
hlti : x.stop - 1 < i
this : x.stop ≤ i
⊢ lt x.as[j] x.as[i] = false
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
case inl.inl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hij : i < j
hj : j < stop
hrng : x.start < x.stop
hi : x.stop - 1 ≤ i
stop_pos : 0 < x.stop
this✝ : x.stop - 1 + 1 = x.stop
hj' : x.stop ≤ j
hlti : x.stop - 1 < i
this : x.stop ≤ i
⊢ lt x.as[j] x.as[i] = false
Tactic:
exact h.sorted i j this hij hj
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
case inl.inr
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hij : i < j
hj : j < stop
hrng : x.start < x.stop
hi : x.stop - 1 ≤ i
stop_pos : 0 < x.stop
this : x.stop - 1 + 1 = x.stop
hj' : x.stop ≤ j
heqi : x.stop - 1 = i
⊢ lt x.as[j] (BinaryHeap.popMax lt x).as[i] = false
Tactic:
cases heqi
Proof state after:
case inl.inr.refl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
j : Nat
hj : j < stop
hrng : x.start < x.stop
stop_pos : 0 < x.stop
this : x.stop - 1 + 1 = x.stop
hj' : x.stop ≤ j
hij : x.stop - 1 < j
hi : x.stop - 1 ≤ x.stop - 1
⊢ lt x.as[j] (BinaryHeap.popMax lt x).as[x.stop - 1] = false
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
case inl.inr.refl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
j : Nat
hj : j < stop
hrng : x.start < x.stop
stop_pos : 0 < x.stop
this : x.stop - 1 + 1 = x.stop
hj' : x.stop ≤ j
hij : x.stop - 1 < j
hi : x.stop - 1 ≤ x.stop - 1
⊢ lt x.as[j] (BinaryHeap.popMax lt x).as[x.stop - 1] = false
Tactic:
rewrite [get_as_popMax_stop_sub_one lt x hrng]
Proof state after:
case inl.inr.refl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
j : Nat
hj : j < stop
hrng : x.start < x.stop
stop_pos : 0 < x.stop
this : x.stop - 1 + 1 = x.stop
hj' : x.stop ≤ j
hij : x.stop - 1 < j
hi : x.stop - 1 ≤ x.stop - 1
⊢ lt x.as[j] x[0] = false
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
case inl.inr.refl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
j : Nat
hj : j < stop
hrng : x.start < x.stop
stop_pos : 0 < x.stop
this : x.stop - 1 + 1 = x.stop
hj' : x.stop ≤ j
hij : x.stop - 1 < j
hi : x.stop - 1 ≤ x.stop - 1
⊢ lt x.as[j] x[0] = false
Tactic:
exact h.bound_above j 0 ⟨hj',hj⟩ _
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
case inr
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i
hij : i < j
hj : j < stop
hz : x.start = x.stop
⊢ lt (BinaryHeap.popMax lt x).as[j] (BinaryHeap.popMax lt x).as[i] = false
Tactic:
simp only [popMax_empty lt x hz] at hi ⊢
Proof state after:
case inr
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hij : i < j
hj : j < stop
hz : x.start = x.stop
hi : x.stop ≤ i
⊢ lt x.as[j] x.as[i] = false
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
case inr
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hij : i < j
hj : j < stop
hz : x.start = x.stop
hi : x.stop ≤ i
⊢ lt x.as[j] x.as[i] = false
Tactic:
exact h.sorted i j hi hij hj
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.Intermed.of_spec
Proof state before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop n : Nat
y : Array α
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
h' : loop.OpSpec lt x n y
hn : n ≤ Subarray.size x
i j : Nat
hi : x.stop - n ≤ i
hij : i < j
hj : j < stop
⊢ lt y[j] y[i] = false
Tactic:
induction h' with
| zero => exact h.sorted i j hi hij hj
| @succ x n _ _ IH =>
  have : x.start < x.stop :=
    trans (x.start.le_add_left n) (Nat.add_lt_of_lt_sub hn)
  refine @IH h.popMax ?_ ?_
  . exact size_popMax lt x ▸ Nat.le_sub_of_add_le hn
  . rewrite [stop_popMax lt x this, Nat.sub_sub, Nat.add_comm]
    exact hi
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.Intermed.of_spec
Proof state before:
case zero
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop n : Nat
y : Array α
i j : Nat
hij : i < j
hj : j < stop
x✝ : Subarray α
h : Algdata.BinaryHeap.heapSort.Intermed lt x✝ stop
hn : 0 ≤ Subarray.size x✝
hi : x✝.stop - 0 ≤ i
⊢ lt x✝.as[j] x✝.as[i] = false
Tactic:
exact h.sorted i j hi hij hj
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.Intermed.of_spec
Proof state before:
case succ
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
stop n✝ : Nat
y : Array α
i j : Nat
hij : i < j
hj : j < stop
x : Subarray α
n : Nat
y✝ : Array α
a✝ : loop.OpSpec lt (BinaryHeap.popMax lt x) n y✝
IH :
  ∀ (h : Algdata.BinaryHeap.heapSort.Intermed lt (BinaryHeap.popMax lt x) stop),
    n ≤ Subarray.size (BinaryHeap.popMax lt x) → (BinaryHeap.popMax lt x).stop - n ≤ i → lt y✝[j] y✝[i] = false
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
hn : n + 1 ≤ Subarray.size x
hi : x.stop - (n + 1) ≤ i
⊢ lt y✝[j] y✝[i] = false
Tactic:
have : x.start < x.stop :=
  trans (x.start.le_add_left n) (Nat.add_lt_of_lt_sub hn)
Proof state after:
case succ
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
stop n✝ : Nat
y : Array α
i j : Nat
hij : i < j
hj : j < stop
x : Subarray α
n : Nat
y✝ : Array α
a✝ : loop.OpSpec lt (BinaryHeap.popMax lt x) n y✝
IH :
  ∀ (h : Algdata.BinaryHeap.heapSort.Intermed lt (BinaryHeap.popMax lt x) stop),
    n ≤ Subarray.size (BinaryHeap.popMax lt x) → (BinaryHeap.popMax lt x).stop - n ≤ i → lt y✝[j] y✝[i] = false
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
hn : n + 1 ≤ Subarray.size x
hi : x.stop - (n + 1) ≤ i
this : x.start < x.stop
⊢ lt y✝[j] y✝[i] = false