Induction on numbers and lists
Induction is the tool for recursive definitions. You will prove properties of your own recursive functions on natural numbers and lists, learn how base and step cases look in Lean, and combine the induction hypothesis with automation.
Sign in to track your progress
- Your first inductionProve double n = n + n for a recursive double.14 min
- Why 0 + n = n needs inductionn + 0 is rfl, 0 + n is not. See what computation does and does not give you.13 min
- Induction over listsA hand-written length distributes over append.15 min
- map preserves lengthBase cases that compute, step cases that rewrite.12 min
- A growth bound by inductionThe sum 0 + 1 + … + n is at least n.12 min
- Exponential growthProve n < 2ⁿ with an induction hypothesis and omega.12 min