Theorem: Algdata.BinaryHeap.heapSort.Intermed.of_spec (Algdata/Data/BinaryHeap/Lemmas.lean)

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
State after:
no goals

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
State after:
no goals

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)
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

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
this : x.start < x.stop
⊢ lt y✝[j] y✝[i] = false
Tactic:
refine @IH h.popMax ?_ ?_
State after:
case succ.refine_1
α : 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
⊢ n ≤ Subarray.size (BinaryHeap.popMax lt x)

case succ.refine_2
α : 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
⊢ (BinaryHeap.popMax lt x).stop - n ≤ i

State before:
case succ.refine_1
α : 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
⊢ n ≤ Subarray.size (BinaryHeap.popMax lt x)

case succ.refine_2
α : 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
⊢ (BinaryHeap.popMax lt x).stop - n ≤ i
Tactic:
. exact size_popMax lt x ▸ Nat.le_sub_of_add_le hn
State after:
case succ.refine_2
α : 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
⊢ (BinaryHeap.popMax lt x).stop - n ≤ i

State before:
case succ.refine_2
α : 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
⊢ (BinaryHeap.popMax lt x).stop - n ≤ i
Tactic:
. rewrite [stop_popMax lt x this, Nat.sub_sub, Nat.add_comm]
  exact hi
State after:
no goals

State before:
case succ.refine_1
α : 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
⊢ n ≤ Subarray.size (BinaryHeap.popMax lt x)
Tactic:
exact size_popMax lt x ▸ Nat.le_sub_of_add_le hn
State after:
no goals

State before:
case succ.refine_2
α : 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
⊢ (BinaryHeap.popMax lt x).stop - n ≤ i
Tactic:
rewrite [stop_popMax lt x this, Nat.sub_sub, Nat.add_comm]
State after:
case succ.refine_2
α : 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
⊢ x.stop - (n + 1) ≤ i

State before:
case succ.refine_2
α : 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
⊢ x.stop - (n + 1) ≤ i
Tactic:
exact hi
State after:
no goals