4.8 Case Analysis and Rewriting

Case analysis splits a goal according to the structure of a value. In Lean, it is performed with cases or pattern matching. Rewriting then proceeds independently in each branch. The combination is common: expose structure first, then normalize each case.

The basic pattern:

example (n : Nat) : n = 0 ∨ n ≠ 0 := by
  cases n with
  | zero =>
      left
      rfl
  | succ k =>
      right
      intro h
      cases h

The cases tactic replaces n by its constructors. Each branch gets a refined goal and context. After the split, equalities often become simpler or definitional, so rfl or simp can close subgoals.

Rewriting frequently follows case analysis. When a hypothesis depends on the shape of a value, splitting exposes concrete forms that match rewrite rules.

example (n : Nat) : n + 0 = n := by
  cases n with
  | zero =>
      rfl
  | succ k =>
      -- goal reduces to (k.succ + 0) = k.succ
      simp

In the successor branch, the goal simplifies using standard lemmas. The split made the recursive structure visible so that simplification can proceed.

Case analysis on equalities is also useful. When you have h : a = b, the tactic cases h replaces all occurrences of b with a (or the reverse, depending on orientation) and reduces the equality to reflexivity. This is a form of substitution.

example (a b : Nat) (h : a = b) :
  a + 1 = b + 1 := by
  cases h
  rfl

After cases h, the goal becomes a + 1 = a + 1, which closes by reflexivity.

This substitution effect generalizes to dependent contexts. If types depend on a value, cases h transports data across the equality. It is often simpler than managing explicit rewrites.

Pattern matching provides a term-level alternative to cases. It can be more compact and integrates naturally with definitions.

def isZero (n : Nat) : Bool :=
  match n with
  | 0     => true
  | _ + 1 => false

In proofs, pattern matching can be used with match expressions, though tactic-style cases is more common for stepwise reasoning.

Rewriting inside cases should respect the refined context. Lemmas that did not match before the split may become applicable. It is often effective to run simp in each branch after cases:

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

The notation <;> applies simp to all branches.

A practical guideline is to perform case analysis when rewriting stalls. If a term hides its structure, splitting exposes it and enables both definitional reduction and lemma-based rewriting.

Avoid unnecessary splits. Each cases multiplies the number of goals. Prefer rewriting when a direct equality is available. Use case analysis when the structure of the data is essential to the argument.

In summary, case analysis refines the context by exposing constructors. Rewriting then becomes simpler and often reduces to reflexivity or straightforward simplification. The two techniques work together: split to reveal structure, rewrite to normalize each branch.