1.15 Pattern Matching Basics

Pattern matching defines functions by cases on the shape of their inputs. For inductive types such as Nat, List, and user-defined data, pattern matching is the canonical way to specify behavior and to expose structure for proofs.

Problem

You want to write definitions that branch on constructors, understand how patterns bind variables, and see how these definitions compile to recursors used in proofs.

Solution

Use pattern matching equations after the function signature.

def pred : Nat -> Nat
| 0     => 0
| n + 1 => n

Evaluate:

#eval pred 0
#eval pred 5

Expected:

0
4

Each equation handles one constructor case of Nat.

Matching on Multiple Arguments

You can match on several arguments at once.

def add' : Nat -> Nat -> Nat
| 0,     m => m
| n + 1, m => (add' n m) + 1

Check:

#eval add' 3 4

Expected:

7

Patterns are matched left to right. Each equation is tried in order.

Variables in Patterns

Variables in patterns bind components of the input.

def swap : Nat × Nat -> Nat × Nat
| (x, y) => (y, x)

#eval swap (3, 5)

Expected:

(5, 3)

Here (x, y) matches a pair and binds x and y.

Wildcards

Use _ to ignore parts of the input.

def isZero : Nat -> Bool
| 0     => true
| _     => false

#eval isZero 0
#eval isZero 7

Expected:

true
false

Wildcards avoid naming values you do not use.

Matching on Lists

def length : List α -> Nat
| []      => 0
| _ :: xs => length xs + 1

#eval length [1, 2, 3, 4]

Expected:

4

The pattern x :: xs splits a list into head and tail.

Nested Patterns

Patterns can be nested to match deeper structure.

def firstOfPairList : List (Nat × Nat) -> Nat
| []            => 0
| (x, _) :: _   => x

#eval firstOfPairList [(3, 4), (5, 6)]

Expected:

3

The pattern (x, _) :: _ matches a nonempty list whose head is a pair.

Order Matters

Patterns are checked in order. Earlier matches take priority.

def testOrder : Nat -> String
| 0     => "zero"
| _     => "nonzero"

Reversing the order would make the second case unreachable.

Overlapping Patterns

Lean allows overlapping patterns but uses the first match.

def overlap : Nat -> String
| _     => "any"
| 0     => "zero"

Here the second case is never used. Lean may warn about unreachable patterns.

Pattern Matching vs if

Pattern matching often replaces if.

def isZeroIf (n : Nat) : Bool :=
  if n = 0 then true else false

Pattern matching version:

def isZeroPM : Nat -> Bool
| 0 => true
| _ => false

The pattern matching version exposes structure directly and is usually preferred for inductive types.

Match Expressions

You can match inside an expression.

def pred' (n : Nat) : Nat :=
  match n with
  | 0     => 0
  | n + 1 => n

This is equivalent to the earlier definition using equations.

Use match when pattern matching is part of a larger expression.

Dependent Pattern Matching

Patterns can influence the result type.

def headOrZero : List Nat -> Nat
| []      => 0
| x :: _  => x

The result depends on the structure of the list. For dependent types, Lean tracks how patterns refine types. More advanced cases appear in later chapters.

Compilation to Recursors

Pattern matching is compiled into eliminators. For Nat, the recursor corresponds to induction.

def double : Nat -> Nat
| 0     => 0
| n + 1 => double n + 2

This is equivalent to a recursive definition using the induction principle for natural numbers.

Understanding this connection explains why pattern matching aligns with proofs by induction.

Pattern Matching in Proofs

Pattern matching appears in proofs through cases.

theorem zero_or_succ (n : Nat) : n = 0 ∨ ∃ m, n = m + 1 := by
  cases n with
  | zero =>
      left
      rfl
  | succ m =>
      right
      exact ⟨m, rfl⟩

Each case corresponds to a constructor of Nat.

Common Pitfalls

If a pattern does not match, check whether all constructors are covered.

If Lean reports missing cases, add a wildcard or explicit case.

If recursion fails, ensure recursive calls use structurally smaller arguments.

If patterns overlap, check their order.

If matching becomes complex, refactor into smaller functions.

Recipe: Build by Cases

Start with the type:

def f : Nat -> Nat

List constructors:

| 0     => ...
| n + 1 => ...

Fill each case independently.

This mirrors structural recursion and ensures coverage.

Takeaway

Pattern matching defines functions by decomposing data into constructors. Each pattern introduces variables that represent parts of the input. The structure of the definition follows the structure of the type, which aligns with recursion and induction. This makes pattern matching the primary tool for working with inductive data in Lean.