Induction

Induction turns recursive structure into proofs. This advanced lesson shows how to prove properties of natural numbers and lists — and, just as importantly, how to read the errors you get when a proof does not go through.

Learning Goals

• Read the induction ... with tactic and know what each case owes you.
• Tell in advance whether a goal needs induction or is true by computation alone.
• Prove standard facts about Nat and List.
• Diagnose a looping simp and fix it with simp only.

Induction Is Recursion for Proofs

Level 7 ended with a claim worth making concrete: recursion and induction are the same mechanism. Ask Lean for the type of Nat's recursor and you get the induction principle, exactly as it appears in a maths textbook.

1#check @Nat.rec
2-- {motive : Nat → Sort u} →
3--   motive Nat.zero →
4--   ((n : Nat) → motive n → motive n.succ) →
5--   (t : Nat) → motive t

Read it as: to produce a motive t for any t, give me the answer for zero, and a way to turn the answer for n into the answer for n + 1. When motive produces data you have written a recursive function; when it produces a proof you have written an induction. The induction tactic is a friendly front-end to this one primitive.

The Shape of an Induction Proof

1theorem zero_add' (n : Nat) : 0 + n = n := by
2  induction n with
3  | zero => rfl
4  | succ k ih =>
5      rw [Nat.add_succ, ih]

• induction n splits the goal into one case per constructor of Nat.
• The zero case asks you to prove the statement for 0.
• The succ case names the predecessor k and hands you ih, the statement already proved for k.
• Your job in that case is to get from ih to the statement for k + 1.

Does This Goal Even Need Induction?

Here is a distinction that catches out nearly everyone, and it is worth internalising before you write another proof. These two statements look symmetric. They are not.

1theorem add_zero (n : Nat) : n + 0 = n := rfl        -- no induction needed
2theorem zero_add (n : Nat) : 0 + n = n := by         -- induction required
3  induction n with
4  | zero => rfl
5  | succ k ih => rw [Nat.add_succ, ih]

The reason is the definition of addition. Nat.add recurses on its second argument:

1-- Roughly how Nat.add is defined:
2--   n + 0     = n
3--   n + (m+1) = (n + m) + 1

So n + 0 matches the first equation directly, for any n, with no case analysis at all. It reduces to n by computation, and rfl closes it.

0 + n matches neither equation until you know the shape of n. That is precisely what induction supplies.

Building Up the Arithmetic

With zero_addin hand you can climb toward commutativity. Each proof uses the previous ones — this stacking is what real formalisation looks like.

1theorem succ_add' (n m : Nat) : (n + 1) + m = (n + m) + 1 := by
2  induction m with
3  | zero => rfl
4  | succ k ih => simp only [Nat.add_succ, ih]
5
6theorem add_comm' (n m : Nat) : n + m = m + n := by
7  induction m with
8  | zero => rw [Nat.add_zero, Nat.zero_add]
9  | succ k ih => rw [Nat.add_succ, ih, Nat.succ_add]

When simp Goes Wrong

This deserves its own section because it is the single most confusing failure mode in early Lean proofs, and the error message does not obviously point at the cause. Consider this plausible-looking attempt:

1theorem add_zero_bad (n : Nat) : n + 0 = n := by
2  induction n with
3  | zero => rfl
4  | succ n ih =>
5      simp [Nat.add_succ, ih]
6
7-- warning: Possibly looping simp theorem: Nat.add_succ
8-- Note: Possibly caused by: Nat.succ_eq_add_one and Nat.add_zero
9-- error: Tactic simp failed with a nested error:
10--        maximum recursion depth has been reached

The instinct is to assume Nat.add_succ simply does not apply here. In fact the opposite is true, and that is the whole problem. In the succ case the goal displays as n + 1 + 0 = n + 1, and Lean represents 1 as Nat.succ 0 — so n + 1 genuinely matches the pattern ?a + Nat.succ ?b. The lemma fires on the successor that induction just introduced, then fights the default simp set:

1--  n + 1
2--    ==[ Nat.add_succ ]==>        (n + 0).succ
3--    ==[ Nat.succ_eq_add_one ]==>  n + 0 + 1
4--    ==[ Nat.add_zero ]==>         n + 1
5--    ... and around again, forever

Nat.succ_eq_add_one and Nat.add_zero are both default simp lemmas, so adding Nat.add_succ closes the cycle. Three fixes, in order of preference:

1-- 1. Does the goal need simp at all? Here it does not.
2theorem fix1 (n : Nat) : n + 0 = n := by
3  induction n with
4  | zero => rfl
5  | succ n ih => rfl
6
7-- 2. simp only does not pull in the default simp set.
8theorem fix2 (n : Nat) : n + 0 = n := by
9  induction n with
10  | zero => rfl
11  | succ n ih => simp only [Nat.add_succ, ih]
12
13-- 3. Subtract the offending lemma from the default set.
14theorem fix3 (n : Nat) : n + 0 = n := by
15  induction n with
16  | zero => rfl
17  | succ n ih => simp [Nat.add_succ, ih, -Nat.succ_eq_add_one]

Induction on Lists

Lists have two constructors, so list induction has two cases: nil and cons. The cons case gives you the statement for the tail and asks you to extend it to one more element.

1theorem length_append (xs ys : List α) :
2    (xs ++ ys).length = xs.length + ys.length := by
3  induction xs with
4  | nil => simp
5  | cons x xs ih =>
6      simp [ih, Nat.succ_add]
7
8theorem map_append (f : α → β) (xs ys : List α) :
9    (xs ++ ys).map f = xs.map f ++ ys.map f := by
10  induction xs with
11  | nil => rfl
12  | cons x xs ih => simp [ih]
13
14theorem append_assoc (xs ys zs : List α) :
15    (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := by
16  induction xs with
17  | nil => rfl
18  | cons x xs ih => simp [ih]

Proving Things About Your Own Functions

The real payoff is proving properties of functions youwrote. Pass the definition's name to simp and it will unfold the equations.

1def sumList : List Nat → Nat
2  | [] => 0
3  | x :: xs => x + sumList xs
4
5theorem sumList_append (xs ys : List Nat) :
6    sumList (xs ++ ys) = sumList xs + sumList ys := by
7  induction xs with
8  | nil => simp [sumList]
9  | cons x xs ih =>
10      simp [sumList, ih, Nat.add_assoc]

Notice the structure: the induction follows the same [] /x :: xs split that sumListitself was defined by. That is not a coincidence, and it is the most useful heuristic in this level — induct on the same argument your function recurses on.

Practice

1example (n : Nat) : n + 0 = n := ?_
2example (n : Nat) : 0 + n = n := ?_
3example (xs : List Nat) : [] ++ xs = xs := ?_
4example (xs : List Nat) : xs ++ [] = xs := ?_

1theorem append_nil (xs : List α) : xs ++ [] = xs := by
2  induction xs with
3  | nil => rfl
4  | cons x xs ih => simp

1theorem length_map (f : α → β) (xs : List α) :
2    (xs.map f).length = xs.length := by
3  induction xs with
4  | nil => rfl
5  | cons x xs ih => simp [ih]

1def sumTo : Nat → Nat
2  | 0 => 0
3  | n + 1 => (n + 1) + sumTo n
4
5theorem sumTo_formula (n : Nat) : 2 * sumTo n = n * (n + 1) := by
6  induction n with
7  | zero => rfl
8  | succ k ih =>
9      simp only [sumTo, Nat.mul_add, Nat.add_mul, Nat.one_mul, Nat.mul_one, ih]
10      omega
11
12#eval sumTo 10   -- 55

Common Mistakes

• Using induction where rfl suffices. Try the cheap tactic first.
• Inducting on the wrong variable. Match the argument your function or operator recurses on.
• Throwing lemmas at simp until it works. That is how you create loops. Read the goal, pick the lemma that matches it.
• Ignoring the “possibly looping” warning. It names the culprit before the error even appears.

Check Yourself

• Why is n + 0 = n true by rfl but 0 + n = n not?
• What exactly does ih state in the cons x xs ih case?
• What is the difference between simp and simp only?
• Given a function that recurses on its second argument, which variable should you induct on?