4.21 Rewriting in Pattern Matching

Pattern matching performs case analysis by selecting a branch based on the shape of a value. Rewriting interacts with pattern matching in two ways: it can simplify the scrutinee so that a branch is selected, and it can normalize expressions inside branches after the match is exposed. In Lean, effective use of rewriting around matches reduces many goals to definitional equality.

Simplifying the scrutinee

When the scrutinee of a match reduces, the entire expression often collapses to a single branch. Rewriting can enable this reduction.

def f (n : Nat) :=
  match n with
  | 0     => 0
  | k + 1 => k + 1

example (a b : Nat) (h : a = b) :
  f a = f b := by
  rw [h]

After rw [h], both sides are syntactically identical, so the goal closes by reflexivity. If additional computation is needed, simp will reduce the match once the scrutinee is known.

Rewriting to expose a branch

If you know the scrutinee equals a constructor, rewrite first, then simplify:

example (n : Nat) (h : n = 0) :
  (match n with | 0 => 1 | _ + 1 => 2) = 1 := by
  rw [h]
  rfl

The rewrite turns the scrutinee into 0, and the match reduces definitionally.

Rewriting inside branches

After a cases split, each branch exposes concrete structure. Rewriting then applies locally:

example (n : Nat) :
  (match n with | 0 => 0 | k + 1 => k + 1) = n := by
  cases n with
  | zero =>
      rfl
  | succ k =>
      simp

The successor branch reduces to k + 1 = k + 1. The combination of case analysis and simplification eliminates the match.

Rewriting hypotheses with matches

If a hypothesis contains a match, normalize it before use:

example (n : Nat)
  (H : (match n with | 0 => 0 | k + 1 => k + 1) = n) :
  n = n := by
  cases n <;> simp at H
  exact H

Each branch simplifies H to a reflexive equality.

Pattern matching in terms

Term-level match behaves the same way. Rewriting applies after the match is evaluated or after the scrutinee is normalized:

example (a b : Nat) (h : a = b) :
  (match a with | 0 => 0 | k + 1 => k + 1)
  =
  (match b with | 0 => 0 | k + 1 => k + 1) := by
  rw [h]

The rewrite aligns both sides, so the goal is trivial.

Avoiding hidden matches

Sometimes the match is hidden inside a definition. Unfold it to enable rewriting:

def g (n : Nat) :=
  match n with
  | 0     => 0
  | k + 1 => k + 1

example (n : Nat) :
  g n = n := by
  cases n <;> simp [g]

Unfolding exposes the match so that simplification can reduce it.

Practical guidance

• Rewrite the scrutinee to a constructor form when possible.
• Use cases to expose branches when rewriting stalls.
• Apply simp after rewriting to collapse matches.
• Unfold definitions to reveal hidden pattern matches.
• Keep matches simple so that definitional reduction applies.

Summary

Rewriting around pattern matching focuses on exposing structure. Once the scrutinee is known, matches reduce automatically. By combining rewriting, case analysis, and simplification, you can eliminate matches and reduce goals to canonical forms.