# Two steps induction in Lean4: how to obtain 2nd inductive hypothesis?

When trying to solve this example from "The Mechanics of Proof":

def a : ℕ → ℤ
| 0 => 2
| 1 => 1
| n + 2 => a (n + 1) + 2 * a n

example (n : ℕ) : a n = 2 ^ n + (-1) ^ n := by
two_step_induction n with k IH1 IH2
. calc a 0 = 2 := by rw [a]
_ = 2 ^ 0 + (-1) ^ 0 := by numbers
. calc a 1 = 1 := by rw [a]
_ = 2 ^ 1 + (-1) ^ 1 := by numbers
calc
a (k + 2)
= a (k + 1) + 2 * a k := by rw [a]
_ = (2 ^ (k + 1) + (-1) ^ (k + 1)) + 2 * (2 ^ k + (-1) ^ k) := by rw [IH1, IH2]
_ = (2 : ℤ) ^ (k + 2) + (-1) ^ (k + 2) := by ring


using only Mathlib, I am struggling to obtain the inductive hypothesis for the 2nd induction step. For now I have

example (n : ℕ) : a n = 2 ^ n + (-1) ^ n := by
induction n with
| zero => simp [a]; rfl
| succ k ik => cases k with
| zero => simp [a]; rfl
| succ k => calc
a (k + 2) = a (k + 1) + 2 * a k := rfl
_ = (2 ^ (k + 1) + (-1) ^ (k + 1)) + 2 * (2 ^ k + (-1) ^ k) := by rw [ik]; sorry
_ = 2 ^ (k + 2) + (-1) ^ (k + 2) := by ring


But here I only have one inductive hypothesis. Where would I get the other hypothesis (in the example above, we have ih1 and ih2) from?

You can put induction principle Nat.twoStepInduction into the induction' tactic. (The norm_num tactic is a good replacement for the numbers tactic in Mechanics of Proof, although as you noticed, rfl also works in this case.)

import Mathlib

def a : ℕ → ℤ
| 0 => 2
| 1 => 1
| n + 2 => a (n + 1) + 2 * a n

example (n : ℕ) : a n = 2 ^ n + (-1) ^ n := by
induction' n using Nat.twoStepInduction with k IH1 IH2
. calc a 0 = 2 := by rw [a]
_ = 2 ^ 0 + (-1) ^ 0 := by rfl  -- or norm_num
. calc a 1 = 1 := by rw [a]
_ = 2 ^ 1 + (-1) ^ 1 := by rfl  -- or norm_num
. calc
a (k + 2)
= a (k + 1) + 2 * a k := by rw [a]
_ = (2 ^ (k + 1) + (-1) ^ (k + 1)) + 2 * (2 ^ k + (-1) ^ k) := by rw [IH1, IH2]
_ = (2 : ℤ) ^ (k + 2) + (-1) ^ (k + 2) := by ring


You can also use Nat.twoStepInduction with the built in induction tactic as follows:

example (n : ℕ) : a n = 2 ^ n + (-1) ^ n := by
induction n using Nat.twoStepInduction
. rfl
. rfl
. case _ k ik1 ik2 => calc
a (k + 2) = a (k + 1) + 2 * a k := rfl
_ = (2 ^ (k + 1) + (-1) ^ (k + 1)) + 2 * (2 ^ k + (-1) ^ k) := by rw [ik1, ik2]
_ = 2 ^ (k + 2) + (-1) ^ (k + 2) := by ring


I found the induction principle Nat.twoStepInduction via moogle.ai.

To see why you need Nat.twoStepInduction, this is how you would prove it with normal induction. Notice we are not proving the original statement by induction, but instead the conjunction of both the n and n+1 cases at the same time! That gives us the necessary induction hypotheses to do the induction, and it is what the induction principle Nat.twoStepInduction automates.

example (n : Nat) : a n = 2 ^ n + (-1) ^ n := by
-- prove the n and n+1 cases simultaneously by induction
have aux_lemma :
a n = 2 ^ n + (-1) ^ n /\
a (n + 1) = 2 ^ (n + 1) + (-1) ^ (n + 1) := by
induction n with
| zero =>
constructor
. rfl
. rfl
| succ k ik =>
constructor
. exact ik.2
. calc
a (k + 2) = a (k + 1) + 2 * (a k) := rfl
_ = 2 ^ (k + 1) + (-1) ^ (k + 1) + 2 * (2 ^ k + (-1) ^ k) := by rw [ik.1, ik.2]
_ = 2 ^ (k + 2) + (-1) ^ (k + 2) := by ring

-- we just need the n case in the end
exact aux_lemma.1