Theorem: Array.size_shrink_loop (Fifteen/Data/Array/Basic.lean)

State before:
α : Type u
as : Array α
k : Nat
h : k ≤ size as
⊢ size (shrink.loop k as) = size as - k
Tactic:
induction k generalizing as with
| zero => rfl
| succ k IH =>
  dsimp [shrink.loop]
  have : as.size = as.pop.size + 1 := by
    rw [as.size_pop, Nat.sub_add_cancel (trans (r:=LE.le (α:=Nat)) (s:=LT.lt (α:=Nat)) k.zero_le h)]
  rewrite [this] at h ⊢
  rewrite [IH as.pop (Nat.le_of_succ_le_succ h)]
  simp only [Nat.succ_sub_succ_eq_sub]
State after:
no goals

State before:
case zero
α : Type u
as : Array α
h : Nat.zero ≤ size as
⊢ size (shrink.loop Nat.zero as) = size as - Nat.zero
Tactic:
rfl
State after:
no goals

State before:
case succ
α : Type u
k : Nat
IH : ∀ (as : Array α), k ≤ size as → size (shrink.loop k as) = size as - k
as : Array α
h : Nat.succ k ≤ size as
⊢ size (shrink.loop (Nat.succ k) as) = size as - Nat.succ k
Tactic:
dsimp [shrink.loop]
State after:
case succ
α : Type u
k : Nat
IH : ∀ (as : Array α), k ≤ size as → size (shrink.loop k as) = size as - k
as : Array α
h : Nat.succ k ≤ size as
⊢ size (shrink.loop k (pop as)) = size as - Nat.succ k

State before:
case succ
α : Type u
k : Nat
IH : ∀ (as : Array α), k ≤ size as → size (shrink.loop k as) = size as - k
as : Array α
h : Nat.succ k ≤ size as
⊢ size (shrink.loop k (pop as)) = size as - Nat.succ k
Tactic:
have : as.size = as.pop.size + 1 := by
  rw [as.size_pop, Nat.sub_add_cancel (trans (r:=LE.le (α:=Nat)) (s:=LT.lt (α:=Nat)) k.zero_le h)]
State after:
case succ
α : Type u
k : Nat
IH : ∀ (as : Array α), k ≤ size as → size (shrink.loop k as) = size as - k
as : Array α
h : Nat.succ k ≤ size as
this : size as = size (pop as) + 1
⊢ size (shrink.loop k (pop as)) = size as - Nat.succ k

State before:
case succ
α : Type u
k : Nat
IH : ∀ (as : Array α), k ≤ size as → size (shrink.loop k as) = size as - k
as : Array α
h : Nat.succ k ≤ size as
this : size as = size (pop as) + 1
⊢ size (shrink.loop k (pop as)) = size as - Nat.succ k
Tactic:
rewrite [this] at h ⊢
State after:
case succ
α : Type u
k : Nat
IH : ∀ (as : Array α), k ≤ size as → size (shrink.loop k as) = size as - k
as : Array α
h : Nat.succ k ≤ size (pop as) + 1
this : size as = size (pop as) + 1
⊢ size (shrink.loop k (pop as)) = size (pop as) + 1 - Nat.succ k

State before:
case succ
α : Type u
k : Nat
IH : ∀ (as : Array α), k ≤ size as → size (shrink.loop k as) = size as - k
as : Array α
h : Nat.succ k ≤ size (pop as) + 1
this : size as = size (pop as) + 1
⊢ size (shrink.loop k (pop as)) = size (pop as) + 1 - Nat.succ k
Tactic:
rewrite [IH as.pop (Nat.le_of_succ_le_succ h)]
State after:
case succ
α : Type u
k : Nat
IH : ∀ (as : Array α), k ≤ size as → size (shrink.loop k as) = size as - k
as : Array α
h : Nat.succ k ≤ size (pop as) + 1
this : size as = size (pop as) + 1
⊢ size (pop as) - k = size (pop as) + 1 - Nat.succ k

State before:
case succ
α : Type u
k : Nat
IH : ∀ (as : Array α), k ≤ size as → size (shrink.loop k as) = size as - k
as : Array α
h : Nat.succ k ≤ size (pop as) + 1
this : size as = size (pop as) + 1
⊢ size (pop as) - k = size (pop as) + 1 - Nat.succ k
Tactic:
simp only [Nat.succ_sub_succ_eq_sub]
State after:
no goals

State before:
α : Type u
k : Nat
IH : ∀ (as : Array α), k ≤ size as → size (shrink.loop k as) = size as - k
as : Array α
h : Nat.succ k ≤ size as
⊢ size as = size (pop as) + 1
Tactic:
rw [as.size_pop, Nat.sub_add_cancel (trans (r:=LE.le (α:=Nat)) (s:=LT.lt (α:=Nat)) k.zero_le h)]
State after:
no goals