Theorem: Algdata.BinaryHeap.heapSort.loop.OpSpec.exists_get (Algdata/Data/BinaryHeap/Basic.lean)

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

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

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

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

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

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

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

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 ?_
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

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

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

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

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

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

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

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

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

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

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

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

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

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