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:

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

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

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]

Collections & Arrays Next: Recursion