Theorem: Nat.foldM_succ (Algdata/Init/Nat.lean)

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
⊢ foldM f init (n + 1) = do
    let x ← f 0 init
    foldM (f ∘ succ) x n
Tactic:
unfold foldM
State after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
⊢ foldM.loop f (n + 1) (n + 1) init = do
    let x ← f 0 init
    foldM.loop (f ∘ succ) n n x

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
⊢ foldM.loop f (n + 1) (n + 1) init = do
    let x ← f 0 init
    foldM.loop (f ∘ succ) n n x
Tactic:
conv =>
  lhs; unfold foldM.loop
  simp only [Nat.add_eq, Nat.add_zero, Nat.add_sub_cancel_left, Nat.sub_self]
State after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
⊢ f 0 init >>= foldM.loop f (n + 1) n = do
    let x ← f 0 init
    foldM.loop (f ∘ succ) n n x

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
⊢ f 0 init >>= foldM.loop f (n + 1) n = do
    let x ← f 0 init
    foldM.loop (f ∘ succ) n n x
Tactic:
suffices ∀ k, k ≤ n → foldM.loop f (n+1) k = foldM.loop (f ∘ succ) n k
  by rw [this n .refl]
State after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
⊢ ∀ (k : Nat), k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
⊢ ∀ (k : Nat), k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
Tactic:
intro k hk
State after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
hk : k ≤ n
⊢ foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
hk : k ≤ n
⊢ foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
Tactic:
induction k
State after:
case zero
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
hk : zero ≤ n
⊢ foldM.loop f (n + 1) zero = foldM.loop (f ∘ succ) n zero

case succ
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n n✝ : Nat
n_ih✝ : n✝ ≤ n → foldM.loop f (n + 1) n✝ = foldM.loop (f ∘ succ) n n✝
hk : succ n✝ ≤ n
⊢ foldM.loop f (n + 1) (succ n✝) = foldM.loop (f ∘ succ) n (succ n✝)

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
hk : zero ≤ n
⊢ foldM.loop f (n + 1) zero = foldM.loop (f ∘ succ) n zero
Tactic:
case zero => rfl
State after:
no goals

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
⊢ foldM.loop f (n + 1) (succ k) = foldM.loop (f ∘ succ) n (succ k)
Tactic:
case succ k h_ind =>
  dsimp [foldM.loop]
  have := calc
    n+1-k-1 = n.succ - k.succ := by simp only [Nat.sub_sub]
    _       = n-k := Nat.succ_sub_succ ..
  have := calc
    succ (n-k-1) = n-k-1+1 := rfl
    _            = n-k := Nat.sub_add_cancel (Nat.lt_sub_of_add_lt (Nat.zero_add .. ▸ hk))
  rw [‹n+1-k-1=n-k›, ‹succ (n-k-1)=n-k›]
  rw [h_ind (Nat.le_of_succ_le hk)]
State after:
no goals

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
this : ∀ (k : Nat), k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
⊢ f 0 init >>= foldM.loop f (n + 1) n = do
    let x ← f 0 init
    foldM.loop (f ∘ succ) n n x
Tactic:
rw [this n .refl]
State after:
no goals

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
hk : zero ≤ n
⊢ foldM.loop f (n + 1) zero = foldM.loop (f ∘ succ) n zero
Tactic:
rfl
State after:
no goals

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
⊢ foldM.loop f (n + 1) (succ k) = foldM.loop (f ∘ succ) n (succ k)
Tactic:
dsimp [foldM.loop]
State after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
⊢ (fun x => f (n + 1 - k - 1) x >>= foldM.loop f (n + 1) k) = fun x =>
    f (succ (n - k - 1)) x >>= foldM.loop (f ∘ succ) n k

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
⊢ (fun x => f (n + 1 - k - 1) x >>= foldM.loop f (n + 1) k) = fun x =>
    f (succ (n - k - 1)) x >>= foldM.loop (f ∘ succ) n k
Tactic:
have := calc
  n+1-k-1 = n.succ - k.succ := by simp only [Nat.sub_sub]
  _       = n-k := Nat.succ_sub_succ ..
State after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
this : n + 1 - k - 1 = n - k
⊢ (fun x => f (n + 1 - k - 1) x >>= foldM.loop f (n + 1) k) = fun x =>
    f (succ (n - k - 1)) x >>= foldM.loop (f ∘ succ) n k

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
this : n + 1 - k - 1 = n - k
⊢ (fun x => f (n + 1 - k - 1) x >>= foldM.loop f (n + 1) k) = fun x =>
    f (succ (n - k - 1)) x >>= foldM.loop (f ∘ succ) n k
Tactic:
have := calc
  succ (n-k-1) = n-k-1+1 := rfl
  _            = n-k := Nat.sub_add_cancel (Nat.lt_sub_of_add_lt (Nat.zero_add .. ▸ hk))
State after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
this✝ : n + 1 - k - 1 = n - k
this : succ (n - k - 1) = n - k
⊢ (fun x => f (n + 1 - k - 1) x >>= foldM.loop f (n + 1) k) = fun x =>
    f (succ (n - k - 1)) x >>= foldM.loop (f ∘ succ) n k

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
this✝ : n + 1 - k - 1 = n - k
this : succ (n - k - 1) = n - k
⊢ (fun x => f (n + 1 - k - 1) x >>= foldM.loop f (n + 1) k) = fun x =>
    f (succ (n - k - 1)) x >>= foldM.loop (f ∘ succ) n k
Tactic:
rw [‹n+1-k-1=n-k›, ‹succ (n-k-1)=n-k›]
State after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
this✝ : n + 1 - k - 1 = n - k
this : succ (n - k - 1) = n - k
⊢ (fun x => f (n - k) x >>= foldM.loop f (n + 1) k) = fun x => f (n - k) x >>= foldM.loop (f ∘ succ) n k

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
this✝ : n + 1 - k - 1 = n - k
this : succ (n - k - 1) = n - k
⊢ (fun x => f (n - k) x >>= foldM.loop f (n + 1) k) = fun x => f (n - k) x >>= foldM.loop (f ∘ succ) n k
Tactic:
rw [h_ind (Nat.le_of_succ_le hk)]
State after:
no goals

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
⊢ n + 1 - k - 1 = succ n - succ k
Tactic:
simp only [Nat.sub_sub]
State after:
no goals