Lean4
LanguageTactics
Module 4 · Level 10 · Premium

List Proofs

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

❗
This is a premium lesson. It includes full proofs of list lemmas and guided exercises.

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.
Premium Track

Premium exercises include proof refactoring challenges and capstone-style proofs.

View Premium Options
Back: Type ClassesBack to Course Overview