Module 4 · Level 10 · Advanced

List Proofs

Lists are the proving ground for real proof engineering. This advanced lesson focuses on map/filter proofs and rewriting workflows.

❗

This lesson pulls together induction, rewriting, simplification, and case splits.

Map and Append

lean

1theorem map_append (f : α → β) (xs ys : List α) :
2    List.map f (xs ++ ys) = List.map f xs ++ List.map f ys := by
3  induction xs with
4  | nil => simp
5  | cons x xs ih =>
6      simp [ih]

Filter and Length

lean

1theorem length_filter_le (p : α → Bool) (xs : List α) :
2    (xs.filter p).length ≤ xs.length := by
3  induction xs with
4  | nil => simp
5  | cons x xs ih =>
6      by_cases h : p x
7      · simp [h, ih]
8      · simp [h, ih]

Key Takeaway

List proofs build on induction and rewriting. Master these and you can scale to advanced mathlib proof engineering.

Advanced Track

Use these examples as templates for small proof refactoring challenges and capstone-style list proofs.

View Advanced Track

Back: Type Classes Back to Course Overview