# 4.8 Case Analysis and Rewriting

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

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

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

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

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

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