Module 2 · Lesson 7

cases & induction

cases performs case analysis on inductive types.induction proves properties by mathematical induction. Both are built into Lean 4 core.

cases — Case Analysis

cases splits a goal based on the constructors of an inductive type:

lean

1-- Boolean case analysis
2example (b : Bool) : b = true ∨ b = false := by
3  cases b with
4  | true => left; rfl
5  | false => right; rfl
6
7-- Natural number cases
8example (n : Nat) : n = 0 ∨ n > 0 := by
9  cases n with
10  | zero => left; rfl
11  | succ m => right; omega

Key Takeaway

cases x creates one goal for each constructor of x's type. Use | constructor =>to name each case.

Case Analysis on Propositions

lean

1-- Disjunction has two constructors: Or.inl and Or.inr
2example (P Q R : Prop) (h : P ∨ Q) (hpr : P → R) (hqr : Q → R) : R := by
3  cases h with
4  | inl hp => exact hpr hp
5  | inr hq => exact hqr hq
6
7-- Conjunction has one constructor with two fields
8example (P Q : Prop) (h : P ∧ Q) : Q := by
9  cases h with
10  | intro left right => exact right

induction — Mathematical Induction

induction proves properties by the induction principle of inductive types:

lean

1-- Prove for all natural numbers
2theorem add_zero (n : Nat) : n + 0 = n := by
3  induction n with
4  | zero => 
5    -- Base case: 0 + 0 = 0
6    rfl
7  | succ m ih => 
8    -- Inductive case: assume m + 0 = m, prove (m+1) + 0 = m+1
9    -- ih : m + 0 = m (induction hypothesis)
10    simp [ih]

Induction on Lists

lean

1theorem length_append (xs ys : List α) : 
2    (xs ++ ys).length = xs.length + ys.length := by
3  induction xs with
4  | nil => 
5    -- Base: ([] ++ ys).length = [].length + ys.length
6    simp
7  | cons h t ih =>
8    -- ih : (t ++ ys).length = t.length + ys.length
9    -- Goal: ((h :: t) ++ ys).length = (h :: t).length + ys.length
10    simp [ih]

The Induction Hypothesis

lean

1-- The key: you get to ASSUME the property for smaller values
2theorem add_assoc (a b c : Nat) : (a + b) + c = a + (b + c) := by
3  induction c with
4  | zero => 
5    -- (a + b) + 0 = a + (b + 0)
6    simp
7  | succ n ih =>
8    -- ih : (a + b) + n = a + (b + n)
9    -- Goal: (a + b) + succ n = a + (b + succ n)
10    simp [Nat.add_succ, ih]

ℹ

The induction hypothesis ih is your key tool in the inductive case. It lets you assume the theorem holds for smaller values.

match in Tactic Mode

lean

1-- match works in tactic mode too
2example (n : Nat) : n = 0 ∨ n > 0 := by
3  match n with
4  | 0 => left; rfl
5  | n + 1 => right; omega

Deep Dive: cases vs match

Both cases and matchperform case analysis, but:

cases uses constructor names explicitly
match uses pattern syntax (like n + 1)
cases can do things match cannot (like eliminating equalities)

Examples

Boolean Negation

lean

1example (b : Bool) : !!b = b := by
2  cases b with
3  | true => rfl
4  | false => rfl

List Reverse

lean

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

Option Analysis

lean

1example (o : Option Nat) : o = none ∨ ∃ n, o = some n := by
2  cases o with
3  | none => left; rfl
4  | some val => right; exact ⟨val, rfl⟩

have & let Next: omega