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

State before:
α : Type u_1
motive : Nat → α → Prop
f : Nat → α → α
n : Nat
init : α
hinit : motive n init
hsucc : ∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)
⊢ motive 0 (foldRev f n init)
Tactic:
induction n generalizing f init motive with
| zero => exact hinit
| succ n IH =>
  rewrite [foldRev_succ]
  apply hsucc
  exact @IH (motive ∘ succ) (f ∘ succ) init hinit (fun k => hsucc (k+1))
State after:
no goals

State before:
case zero
α : Type u_1
motive : Nat → α → Prop
f : Nat → α → α
init : α
hinit : motive zero init
hsucc : ∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)
⊢ motive 0 (foldRev f zero init)
Tactic:
exact hinit
State after:
no goals

State before:
case succ
α : Type u_1
n : Nat
IH :
  ∀ {motive : Nat → α → Prop} (f : Nat → α → α) (init : α),
    motive n init → (∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)) → motive 0 (foldRev f n init)
motive : Nat → α → Prop
f : Nat → α → α
init : α
hinit : motive (succ n) init
hsucc : ∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)
⊢ motive 0 (foldRev f (succ n) init)
Tactic:
rewrite [foldRev_succ]
State after:
case succ
α : Type u_1
n : Nat
IH :
  ∀ {motive : Nat → α → Prop} (f : Nat → α → α) (init : α),
    motive n init → (∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)) → motive 0 (foldRev f n init)
motive : Nat → α → Prop
f : Nat → α → α
init : α
hinit : motive (succ n) init
hsucc : ∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)
⊢ motive 0 (f 0 (foldRev (f ∘ succ) n init))

State before:
case succ
α : Type u_1
n : Nat
IH :
  ∀ {motive : Nat → α → Prop} (f : Nat → α → α) (init : α),
    motive n init → (∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)) → motive 0 (foldRev f n init)
motive : Nat → α → Prop
f : Nat → α → α
init : α
hinit : motive (succ n) init
hsucc : ∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)
⊢ motive 0 (f 0 (foldRev (f ∘ succ) n init))
Tactic:
apply hsucc
State after:
case succ.a
α : Type u_1
n : Nat
IH :
  ∀ {motive : Nat → α → Prop} (f : Nat → α → α) (init : α),
    motive n init → (∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)) → motive 0 (foldRev f n init)
motive : Nat → α → Prop
f : Nat → α → α
init : α
hinit : motive (succ n) init
hsucc : ∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)
⊢ motive (0 + 1) (foldRev (f ∘ succ) n init)

State before:
case succ.a
α : Type u_1
n : Nat
IH :
  ∀ {motive : Nat → α → Prop} (f : Nat → α → α) (init : α),
    motive n init → (∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)) → motive 0 (foldRev f n init)
motive : Nat → α → Prop
f : Nat → α → α
init : α
hinit : motive (succ n) init
hsucc : ∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)
⊢ motive (0 + 1) (foldRev (f ∘ succ) n init)
Tactic:
exact @IH (motive ∘ succ) (f ∘ succ) init hinit (fun k => hsucc (k+1))
State after:
no goals