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.0

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.

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.0

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

Guards (Conditional Patterns)

Add conditions to patterns with if:

lean

1def classifyNumber (n : Int) : String :=
2  match n with
3  | 0 => "zero"
4  | n => if n > 0 then "positive" else "negative"
5
6-- Or using pattern guards
7def grade (score : Nat) : String :=
8  match score with
9  | s => if s >= 90 then "A"
10         else if s >= 80 then "B"
11         else if s >= 70 then "C"
12         else if s >= 60 then "D"
13         else "F"
14
15#eval grade 85  -- "B"

Or-Patterns

Match multiple patterns with the same result:

lean

1def isWeekend : Weekday → Bool
2  | Weekday.saturday | Weekday.sunday => true
3  | _ => false
4
5-- Without or-patterns (more verbose)
6def isWeekend' : Weekday → Bool
7  | Weekday.saturday => true
8  | Weekday.sunday => true
9  | _ => false

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 first element
4  | xs@[] => (0, xs)
5
6#eval processFirst [1, 2, 3]  -- (1, [1, 2, 3])
7
8-- Useful when you need both the structure and its parts
9def describe : Option Nat → String
10  | opt@(some n) => s!"Value {n}, original: {repr opt}"
11  | opt@none => s!"None, original: {repr opt}"

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