Module 3 · Lesson 1

Pattern Matching

Pattern matching is the primary control flow mechanism in Lean. It's how you deconstruct data and handle different cases elegantly.

The Match Expression

Use match to inspect values and branch based on their structure:

lean

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

Each branch has a pattern (left of =>) and a result (right of =>). Lean checks patterns from top to bottom.

Function Definition Syntax

For simple functions, you can pattern match directly in the definition:

lean

1-- Using match
2def factorial1 (n : Nat) : Nat :=
3  match n with
4  | 0 => 1
5  | n + 1 => (n + 1) * factorial1 n
6
7-- Direct pattern matching (cleaner)
8def factorial2 : Nat → Nat
9  | 0 => 1
10  | n + 1 => (n + 1) * factorial2 n
11
12#eval factorial2 5  -- 120

Key Takeaway

The direct pattern matching syntax (without match) is often cleaner for simple functions. Use match when you need to match in the middle of a larger expression.

Matching on Inductive Types

Pattern matching shines when working with inductive types:

lean

1inductive Shape where
2  | circle (radius : Float)
3  | rectangle (width : Float) (height : Float)
4  | triangle (base : Float) (height : Float)
5
6def area : Shape → Float
7  | Shape.circle r => 3.14159 * r * r
8  | Shape.rectangle w h => w * h
9  | Shape.triangle b h => 0.5 * b * h
10
11def perimeter : Shape → Float
12  | Shape.circle r => 2.0 * 3.14159 * r
13  | Shape.rectangle w h => 2.0 * (w + h)
14  | Shape.triangle _ _ => 0.0  -- would need side lengths
15
16#eval area (Shape.rectangle 3.0 4.0)  -- 12.000000

Exhaustiveness Checking

Lean refuses to compile if you miss a case:

lean

1inductive Color where
2  | red | green | blue
3
4-- This won't compile!
5-- def toHex : Color → String
6--   | Color.red => "#FF0000"
7--   | Color.green => "#00FF00"
8--   -- Missing blue case!
9
10-- Complete version:
11def toHex : Color → String
12  | Color.red => "#FF0000"
13  | Color.green => "#00FF00"
14  | Color.blue => "#0000FF"

❗

Exhaustiveness checking is one of Lean's most powerful safety features. It catches bugs at compile time that would be runtime errors in other languages.

Order Matters: First Match Wins

Branches are tried top to bottom, and the first one that matches wins. Lean also tells you when a branch can never be reached:

lean

1-- Overlapping patterns: (0, 0) matches the first branch, not the second
2def sumPair : Nat × Nat → Nat
3  | (0, b) => b
4  | (a, 0) => a
5  | (a, b) => a + b
6
7#eval sumPair (0, 0)   -- 0, via the FIRST branch
8
9-- Putting the catch-all first makes later branches dead code,
10-- and Lean says so rather than silently ignoring them:
11-- def f : Nat → String
12--   | _ => "catch-all"
13--   | 0 => "zero"
14-- error: Redundant alternative: Any expression matching 0
15--        will match one of the preceding alternatives

💡

Order your branches most-specific first. If you get the redundant alternative error, you have written them backwards — it is a genuine bug report, not a style warning.

Matching Nat: the n + 1 Pattern

Nat looks like a primitive but is an inductive type with constructors zero and succ. The pattern n + 1 is sugar for Nat.succ n:

lean

1def pred : Nat → Nat
2  | 0     => 0
3  | n + 1 => n
4
5#print pred
6-- fun x => match x with
7--   | 0 => 0
8--   | n.succ => n     ← n + 1 was compiled to Nat.succ n
9
10-- Bigger literal patterns work too, and peel off that many succs
11def describeSmall : Nat → String
12  | 0     => "zero"
13  | 1     => "one"
14  | n + 2 => s!"{n} plus two"
15
16#eval describeSmall 5   -- "3 plus two"

ℹ

The n + 1 spelling is not cosmetic. It is what makes induction and simp line up with your definition later, and it is why the standard library writes xs.length + 1 rather than 1 + xs.length everywhere.

Matching Nothing: nomatch

Some types have no values at all. If you have one in your hands, you are in an impossible situation and can produce anything — nomatchsays exactly that.

lean

1-- Empty has no constructors, so there is no case to write
2def fromEmpty (x : Empty) : Nat := nomatch x
3
4-- The same trick appears in proofs: from a contradiction, anything follows
5example (h : False) : 2 + 2 = 5 := absurd h (by simp)

Destructuring Structures

Pattern matching works on structures too:

lean

1structure Point where
2  x : Float
3  y : Float
4
5-- Destructure in the pattern
6def distanceFromOrigin : Point → Float
7  | ⟨x, y⟩ => Float.sqrt (x * x + y * y)
8
9-- Equivalent using field access
10def distanceFromOrigin' (p : Point) : Float :=
11  Float.sqrt (p.x * p.x + p.y * p.y)
12
13#eval distanceFromOrigin ⟨3.0, 4.0⟩  -- 5.000000

Nested Patterns

Patterns can be nested to match complex structures. This is powerful when you have data types inside other data types, such as a list containing optional values.

lean

1-- Match on nested structures
2def firstElement : List (Option Nat) → Option Nat
3  | [] => none
4  | none :: _ => none
5  | some n :: _ => some n
6
7#eval firstElement [some 1, none]  -- some 1
8#eval firstElement [none, some 2]  -- none
9
10-- Match on pairs
11def addPair : Nat × Nat → Nat
12  | (a, b) => a + b
13
14#eval addPair (3, 4)  -- 7

Matching on Multiple Inputs

You can pattern match on multiple arguments at once, which is perfect for combining two values or two lists.

lean

1def addOptions : Option Nat → Option Nat → Option Nat
2  | some a, some b => some (a + b)
3  | _, _ => none
4
5#eval addOptions (some 2) (some 3)  -- some 5
6#eval addOptions none (some 3)      -- none

Conditions in Branches

Lean does not have Haskell-style pattern guards — there is no | n if n > 0 => …. Instead, match on structure and use if inside the branch:

lean

1def classifyNumber (n : Int) : String :=
2  match n with
3  | 0 => "zero"
4  | n => if n > 0 then "positive" else "negative"
5
6#eval classifyNumber (-3)   -- "negative"
7
8-- When every case is a condition rather than a shape, skip match entirely
9def grade (score : Nat) : String :=
10  if score >= 90 then "A"
11  else if score >= 80 then "B"
12  else if score >= 70 then "C"
13  else if score >= 60 then "D"
14  else "F"
15
16#eval grade 85  -- "B"

💡

Reach for matchwhen you are asking "what shape is this value?" and for ifwhen you are asking "is this condition true?". A match with a single catch-all pattern and a chain of ifs inside it is always the ifchain written the long way.

Remembering What You Matched: match h : e with

A plain match forgets the connection between the scrutinee and the branch you took. Naming the equation with match h : e with keeps it, which is essential once you start proving things about the function.

lean

1def lookupAt (xs : List Nat) (i : Nat) : String :=
2  match h : xs[i]? with
3  | none   => "out of range"
4  -- inside this branch, h : xs[i]? = some v
5  | some v => s!"found {v}"
6
7#eval lookupAt [1, 2, 3] 1   -- "found 2"

ℹ

Without the h :, once you are inside the some v branch Lean knows v exists but has thrown away the fact that it came from xs[i]?. That fact is exactly what a later proof needs. The cost of writing h : is nothing; the cost of omitting it is sometimes restructuring the whole function.

Or-Patterns

Match multiple patterns with the same result:

lean

1inductive Weekday where
2  | monday | tuesday | wednesday | thursday | friday | saturday | sunday
3
4def isWeekend : Weekday → Bool
5  | .saturday | .sunday => true
6  | _ => false
7
8-- Without or-patterns (more verbose)
9def isWeekend' : Weekday → Bool
10  | .saturday => true
11  | .sunday => true
12  | _ => false
13
14#eval isWeekend .saturday   -- true

⚠

Every alternative in an or-pattern must bind the same variables with the same types. | .circle r | .rectangle w h => … is rejected, because the two sides disagree about what is in scope. Or-patterns are for cases you treat identically and whose contents you do not need.

As-Patterns

Use @ to bind a name while also destructuring:

lean

1-- Bind the whole list while also matching head and tail
2def processFirst : List Nat → (Nat × List Nat)
3  | xs@(x :: _) => (x, xs)  -- xs is the whole list, x is the first element
4  | [] => (0, [])
5
6#eval processFirst [1, 2, 3]  -- (1, [1, 2, 3])
7#eval processFirst []         -- (0, [])
8
9-- Useful when you need both the structure and its parts
10def describeOpt : Option Nat → String
11  | opt@(some n) => s!"Value {n}, original: {repr opt}"
12  | none => "None"
13
14#eval describeOpt (some 1)   -- "Value 1, original: some 1"

⚠

Parenthesise the pattern after @ whenever it starts with a bracket. xs@[] does not parse: Lean reads @[as the start of an attribute and reports a confusing "unexpected token". Write xs@([]), or just match [] directly — there is nothing to name in an empty list.

If-Let and Let-Else

For simple pattern matching with an alternative, use if let:

lean

1-- if let: match a pattern or take else branch
2def getFirst (xs : List Nat) : Nat :=
3  if let x :: _ := xs then x else 0
4
5#eval getFirst [1, 2, 3]  -- 1
6#eval getFirst []         -- 0
7
8-- Works with any pattern
9def extractValue (opt : Option String) : String :=
10  if let some s := opt then s else "default"
11
12-- let-else: match or diverge early
13def processOption (opt : Option Nat) : IO Nat := do
14  let some n := opt | return 0  -- Early return if none
15  IO.println s!"Processing {n}"
16  return n * 2

💡

Use if let when you have one pattern and a simple fallback. Use match when you have multiple cases or complex logic.

Deep Dive: Pattern Matching Compiles to Efficient Code

Lean's pattern matching compiles to efficient decision trees. The compiler analyzes patterns and generates optimal branching code—often better than hand-written if-else chains.

This means you can write clear, declarative patterns without worrying about performance.

Matching on Lists

Lists are commonly pattern-matched to process elements:

lean

1def sum : List Nat → Nat
2  | [] => 0
3  | x :: xs => x + sum xs
4
5def head? : List α → Option α
6  | [] => none
7  | x :: _ => some x
8
9def tail? : List α → Option (List α)
10  | [] => none
11  | _ :: xs => some xs
12
13def take : Nat → List α → List α
14  | 0, _ => []
15  | _, [] => []
16  | n + 1, x :: xs => x :: take n xs
17
18#eval sum [1, 2, 3, 4, 5]     -- 15
19#eval take 2 [1, 2, 3, 4, 5]  -- [1, 2]

Exercise: Safe Head and Tail

Write a function that returns both the head and tail of a list if it exists.

lean

1def headTail? : List α → Option (α × List α)
2  | [] => none
3  | x :: xs => some (x, xs)
4
5#eval headTail? [1, 2, 3]  -- some (1, [2, 3])
6#eval headTail? ([] : List Nat)  -- none

Collections & Arrays Next: Recursion