Module 3
Induction: proving things about your programs
- Proofs by induction on Nat and List.
- Combine simp, rw and the induction hypothesis.
- Verify properties of functions you wrote yourself.
The playground runs the latest Lean in your browser. Locally, the file is Exercises/Induction.lean and you check it with lake exe check Induction.
Guide
Read: Theorem Proving in Lean 4, chapters 7 ("Inductive Types") and 8 ("Induction and Recursion").
Key ideas:
induction n with | zero => ... | succ k ih => ...produces two cases. In the second one,ih(the induction hypothesis) says the property holds fork.- The structure of the proof follows the structure of the function: if the
function recurses on
xs, do induction onxs. simp [f]unfolds the definition off.omegaautomatically solves linear equalities and inequalities over natural numbers and integers.
Exercises: ex1 to ex3, plus the final project: define reverse and
prove that it preserves the length of a list.
Hint: for the final project you will probably need a lemma about
length (append xs ys). It is already proved in the file as length_append.
When you finish module 3: lake build should succeed without any
sorry. That marks the end of the introduction.
Exercises
Solve them in the file, not here: the playground or VS Code shows the goal at each step. Tick an exercise once lake exe check marks it ✅ (or it compiles without sorry in the playground).
1ex1
theorem ex1 {α : Type} (xs : List α) : append xs [] = xs := by
sorry2ex2
theorem ex2 {α : Type} (xs ys zs : List α) :
append (append xs ys) zs = append xs (append ys zs) := by
sorry3ex3
theorem ex3 (n m : Nat) : add (m + 1) n = add m n + 1 := by
sorry4reverse
def reverse {α : Type} : List α → List α
| _ => sorry2 tests check your definition when you run lake exe check Induction.
5length_reverse
theorem length_reverse {α : Type} (xs : List α) :
length (reverse xs) = length xs := by
sorry