List Proofs

Lists are the proving ground for real proof engineering. This final level is less about new concepts than about workflow— how to find the lemma you need, how to choose between tactics, and what to do when a proof will not close.

Learning Goals

• Prove the standard map, filter, and reverse lemmas.
• Choose deliberately between rw, simp, and omega.
• Split a proof on a Bool condition with by_cases.
• Use simp? and exact? to discover library lemmas.
• Debug a stuck proof systematically instead of guessing.

Map and Append

The pattern from Level 8 carries over unchanged: induct on the list the operation recurses on, then feed the induction hypothesis to simp.

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]

Map fusion is the same shape, and is one of the more useful rewrites in practice — it turns two traversals into one.

1theorem map_map' (f : α → β) (g : β → γ) (xs : List α) :
2    (xs.map f).map g = xs.map (fun x => g (f x)) := by
3  induction xs with
4  | nil => rfl
5  | cons x xs ih => simp [ih]

Filter and Length

Filtering can only ever shrink a list. Proving it introduces a genuinely new move: the recursive case depends on whether the predicate accepted the head, so you must split on that.

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]; omega
8      · simp [h]; omega

by_cases h : p x produces two goals: one with h : p x = true and one with h : ¬p x = true. Passing h to simp lets it reduce the filter in each branch.

Choosing Your Tactic

Three tactics do most of the work in list proofs. Picking the right one is mostly about how much control you want.

1-- rw: surgical, names exactly what happens
2theorem assoc_by_rw (xs ys zs : List α) :
3    (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := by
4  rw [List.append_assoc]
5
6-- simp: hand it the induction hypothesis and let it normalise
7theorem reverse_append' (xs ys : List α) :
8    (xs ++ ys).reverse = ys.reverse ++ xs.reverse := by
9  induction xs with
10  | nil => simp
11  | cons x xs ih => simp [ih]

Finding the Lemma You Need

The hardest part of a real proof is rarely the logic — it is knowing that the fact you want is called List.length_map. Lean will tell you. Both tactics below print a concrete suggestion you can paste back over the call.

1example (xs : List Nat) : (xs.map (· + 1)).length = xs.length := by
2  simp?
3-- Try this: simp only [List.length_map]
4
5example (n : Nat) : n + 0 = n := by
6  exact?
7-- Try this: exact Nat.add_eq_left.mpr rfl

• simp? runs simp and reports the minimal lemma set it actually used.
• exact? searches the library for a single term that closes the goal.
• apply? is the same idea but allows leftover goals.

Naming in the standard library is systematic, which makes guessing viable too. Lemma names describe the statement left to right: length_append is about the length of an append; map_map is about a map of a map. Once you know the convention you can often type the name you need and find it exists.

Proving Things About Your Own Functions

Bringing the whole course together: a recursive definition from Level 7, an induction from Level 8, and omega to finish the arithmetic.

1def sumList : List Nat → Nat
2  | [] => 0
3  | x :: xs => x + sumList xs
4
5theorem sumList_map_succ (xs : List Nat) :
6    sumList (xs.map (· + 1)) = sumList xs + xs.length := by
7  induction xs with
8  | nil => rfl
9  | cons x xs ih =>
10      simp [sumList, ih]
11      omega

The statement says: adding one to every element raises the total by exactly the number of elements. simp unfolds the definitions and applies ih; what remains is a rearrangement of sums that omega settles without you naming a single associativity lemma.

Practice

1theorem length_reverse' (xs : List α) : xs.reverse.length = xs.length := by
2  induction xs with
3  | nil => rfl
4  | cons x xs ih => simp

1theorem reverse_reverse' (xs : List α) : xs.reverse.reverse = xs := by
2  induction xs with
3  | nil => rfl
4  | cons x xs ih => simp [ih]

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

Common Mistakes

• Assuming both by_cases branches need the same tactic. Check each goal separately.
• Adding lemmas to simp until something works. That is how loops appear. Read the goal first.
• Reaching for omega on a nonlinear goal. It cannot handle products of variables; normalise first.
• Ignoring “unused simp argument” warnings. They usually mean the goal was easier than you thought.

Where to Go Next

You have covered the core of Lean as both a programming language and a proof assistant. Three natural directions from here:

• Mathlib. The mathematical library, with tactics such as ring, linarith, and norm_num that make the arithmetic in this level much easier.
• Metaprogramming. Lean is written in Lean; you can define your own tactics and notation.
• Verified programming. Write real software and prove the parts that matter correct.