Induction
Induction turns recursive structure into proofs. This premium lesson shows how to prove properties of natural numbers and lists.
❗
This is a premium lesson. It includes extended explanations, proof walkthroughs, and deeper exercises for mastery.
Induction on Natural Numbers
lean
1theorem add_zero (n : Nat) : n + 0 = n := by2 induction n with3 | zero => rfl4 | 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 := by3 induction xs with4 | nil => simp5 | cons x xs ih =>6 simp [ih]Key Takeaway
Induction is the proof counterpart of recursion. Once you master it, most proofs become systematic.
Premium Track
Unlock the premium module to access walkthrough videos, extended exercises, and project-grade proofs.
View Premium Options