Induction on numbers and lists
Prove properties of your own recursive functions on natural numbers and lists, see what base and step cases look like in Lean, and combine the induction hypothesis with automation.
Progress is kept in this browser until you sign in
- 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