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

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

Evaluate:

```lean
#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.

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

Check:

```lean
#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.

```lean
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.

```lean
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

```lean
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.

```lean
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.

```lean
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.

```lean
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`.

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

Pattern matching version:

```lean
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.

```lean
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.

```lean
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.

```lean
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`.

```lean
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:

```lean
def f : Nat -> Nat
```

List constructors:

```lean
| 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.