Module 4 · Level 8 · Advanced

Induction

Induction turns recursive structure into proofs. This advanced lesson shows how to prove properties of natural numbers and lists.

❗

This lesson builds on recursion and rewriting. Read Level 7 first if structural recursion still feels unfamiliar.

Induction on Natural Numbers

lean

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

Induction on Lists

lean

1theorem length_append (xs ys : List Nat) :
2    (xs ++ ys).length = xs.length + ys.length := by
3  induction xs with
4  | nil => simp
5  | cons x xs ih =>
6      simp [ih]

Key Takeaway

Induction is the proof counterpart of recursion. Once you master it, most proofs become systematic.

Advanced Track

Continue through the advanced modules to connect induction, type classes, and reusable list proof workflows.

View Advanced Track

Back: Recursion Next: Level 9 · Type Classes