Pattern Matching

Pattern matching is the cleanest way to deconstruct data and express branching logic in Lean. It is also the tool that lets the compiler prove you handled every case — which is why it underpins both recursion and proofs.

Learning Goals

• Match on numbers, options, lists, tuples, and your own types.
• Use the n + 1 pattern to name a predecessor.
• Match on several values at once and nest patterns inside each other.
• Read and fix a “Missing cases” error.
• Define your own multi-constructor types with inductive.

Matching on Nat

1def describe (n : Nat) : String :=
2  match n with
3  | 0 => "zero"
4  | 1 => "one"
5  | _ => "many"
6
7#eval describe 0   -- "zero"
8#eval describe 1   -- "one"
9#eval describe 5   -- "many"

Patterns are tried top to bottom, first match wins. The underscore is a wildcard that matches anything and binds nothing. Because it matches everything, a wildcard placed first would shadow every branch below it — put it last.

The n + 1 pattern

Every natural number is either 0 or one more than another natural number. The pattern k + 1 matches the second case and binds kto the predecessor — giving you a smaller number to work with.

1def pred (n : Nat) : Nat :=
2  match n with
3  | 0 => 0
4  | k + 1 => k
5
6#eval pred 0   -- 0
7#eval pred 7   -- 6

You can step by more than one. Here the recursive call shrinks the input by two each time, which is enough for Lean to see the function terminates.

1def parity : Nat → String
2  | 0 => "even"
3  | 1 => "odd"
4  | n + 2 => parity n
5
6#eval parity 10   -- "even"
7#eval parity 7    -- "odd"

Matching on Option and List

1def showOption (value : Option String) : String :=
2  match value with
3  | some name => s!"Hello {name}"
4  | none => "No name"
5
6#eval showOption (some "Lean")   -- "Hello Lean"
7#eval showOption none            -- "No name"

Lists follow the same two-case shape you met in Level 2: empty, or one element on top of a smaller list.

1def headOption (xs : List Nat) : Option Nat :=
2  match xs with
3  | [] => none
4  | x :: _ => some x
5
6#eval headOption [1, 2, 3]   -- some 1
7#eval headOption []          -- none
8
9-- Patterns can look further than one element ahead
10def secondOption : List Nat → Option Nat
11  | _ :: y :: _ => some y
12  | _ => none
13
14#eval secondOption [1, 2, 3]   -- some 2
15#eval secondOption [1]         -- none

Matching on Several Values at Once

Separate the scrutinees with commas, and separate each branch's patterns the same way.

1def bothZero (a b : Nat) : Bool :=
2  match a, b with
3  | 0, 0 => true
4  | _, _ => false
5
6#eval bothZero 0 0   -- true
7#eval bothZero 0 1   -- false
8
9-- Reimplementing boolean and, for illustration
10def andB : Bool → Bool → Bool
11  | true, true => true
12  | _, _ => false

Nested Patterns

Patterns compose. You can look inside a structure that is itself inside another one, in a single branch.

1def firstIsSome : List (Option Nat) → String
2  | some x :: _ => s!"starts with {x}"
3  | none :: _   => "starts with none"
4  | []          => "empty"
5
6#eval firstIsSome [some 3, none]   -- "starts with 3"
7#eval firstIsSome [none]           -- "starts with none"
8#eval firstIsSome []               -- "empty"

Destructuring Tuples

A pattern works anywhere you bind a value — not just in match, but in let and in lambda arguments too.

1def swap (p : Nat × String) : String × Nat :=
2  match p with
3  | (n, s) => (s, n)
4
5#eval swap (1, "one")   -- ("one", 1)
6
7-- Directly in let
8def sumPair (p : Nat × Nat) : Nat :=
9  let (a, b) := p
10  a + b
11
12#eval sumPair (5, 6)    -- 11
13
14-- Directly in a lambda
15#eval [(1, 2), (3, 4)].map (fun (a, b) => a + b)   -- [3, 7]

Your Own Types with inductive

Level 4 gave you structure for data with a fixed set of fields. inductive is the more general tool: it lets a type have several different shapes, each carrying its own data. This is where pattern matching becomes essential rather than merely convenient.

1inductive Shape where
2  | circle (r : Nat)
3  | rect (w h : Nat)
4  | triangle (b h : Nat)
5deriving Repr
6
7def area : Shape → Nat
8  | .circle r     => 3 * r * r      -- π ≈ 3, this is Nat after all
9  | .rect w h     => w * h
10  | .triangle b h => b * h / 2
11
12#eval area (.circle 2)       -- 12
13#eval area (.rect 3 4)       -- 12
14#eval area (.triangle 6 4)   -- 12

Option and Listare not built into the language — they are ordinary inductive types defined exactly like this one, which is why matching on them feels identical.

Exhaustiveness: The Compiler Has Your Back

Lean requires every match to cover every possible input. Leave a case out and it will not compile — and the error tells you precisely which case you forgot.

1def bad (xs : List Nat) : Nat :=
2  match xs with
3  | x :: _ => x
4
5-- error: Missing cases:
6-- []

This is the same totality requirement from Level 2 that made 3 - 5 equal 0. Every function must produce a result for every input, so “I only handled the non-empty case” is not an option. In exchange, a whole category of runtime crash simply cannot happen in your Lean programs.

1-- if is the right tool: a condition, no data to extract
2def sign (n : Int) : String :=
3  if n > 0 then "positive"
4  else if n < 0 then "negative"
5  else "zero"
6
7-- match is the right tool: you need the x out of the some
8def double? (o : Option Nat) : Option Nat :=
9  match o with
10  | some x => some (x * 2)
11  | none => none

Practice

1def lastOption : List Nat → Option Nat
2  | [] => none
3  | [x] => some x
4  | _ :: rest => lastOption rest
5
6#eval lastOption [1, 2, 3]   -- some 3
7#eval lastOption []          -- none

1def classify (n : Nat) : String :=
2  match n with
3  | 0 => "zero"
4  | 1 => "one"
5  | 2 => "two"
6  | _ => "lots"
7
8#eval classify 2   -- "two"
9#eval classify 9   -- "lots"

1def zip : List Nat → List String → List (Nat × String)
2  | [], _ => []
3  | _, [] => []
4  | x :: xs, y :: ys => (x, y) :: zip xs ys
5
6#eval zip [1, 2, 3] ["a", "b"]   -- [(1, "a"), (2, "b")]

1def name : Shape → String
2  | .circle _     => "circle"
3  | .rect _ _     => "rectangle"
4  | .triangle _ _ => "triangle"
5
6#eval name (.rect 1 1)   -- "rectangle"

Common Mistakes

• Putting the wildcard first. It matches everything, so every later branch becomes unreachable.
• Putting the general case before the specific one._ :: rest before [x] means [x] never fires.
• Forgetting a case.Read the “Missing cases” list — it is the exact answer, not a hint.
• Using if when you need the contained value.if o.isSome does not give you the x.

Check Yourself

• What does k bind to in the pattern k + 1 when the input is 7?
• Why must [x] come before _ :: rest?
• What is .circle shorthand for, and how does Lean know?
• When would you choose match over if?