# 4.10 Rewriting with Lemmas

# 4.10 Rewriting with Lemmas

Lemmas provide reusable equalities that drive most rewriting. In Lean, a well-shaped lemma doubles as a rewrite rule. The focus here is on selecting, orienting, and instantiating lemmas so that `rw` and `simp` behave deterministically.

A lemma has a type that ends in an equality, possibly with parameters:

```lean
Nat.add_comm : ∀ a b : Nat, a + b = b + a
```

Using such a lemma with `rw` requires that its left-hand side matches a subterm of the goal after instantiation. Lean infers arguments when possible:

```lean id="w0p9s2"
example (a b : Nat) : a + b = b + a := by
  rw [Nat.add_comm]
```

If inference is insufficient, supply arguments explicitly:

```lean id="2p3z1m"
rw [Nat.add_comm a b]
```

Explicit instantiation is often necessary when multiple matches exist or when the intended occurrence is ambiguous.

Orientation is critical. Many library lemmas are symmetric or have a preferred direction for normalization. Choose the direction that reduces complexity:

```lean id="9s6k8q"
rw [Nat.add_comm]     -- a + b → b + a
rw [← Nat.add_comm]   -- b + a → a + b
```

Consistent orientation across a development avoids oscillation and simplifies `simp` usage.

Lemmas with conditions require those conditions to be available in the context:

```lean id="q3m5td"
example (a b : Nat) (h : a = b) :
  a + 1 = b + 1 := by
  rw [h]
```

Here the lemma is the hypothesis `h`. For library lemmas that require premises, ensure those premises are present or derive them locally before rewriting.

Rewriting often benefits from partial application. When a lemma targets a subterm, wrap it to match the context:

```lean id="c8x4r1"
example (f : Nat -> Nat -> Nat) (a b c : Nat)
  (h : a = b) :
  f a c = f b c := by
  rw [show a = b from h]
```

More directly, use a lambda to isolate the position:

```lean id="k1v7yn"
rw [congrArg (fun x => f x c) h]
```

For multi-argument functions, combine congruence and rewriting, or use specialized lemmas such as `congrArg₂` when available.

Chaining lemma-based rewrites is common. Keep the sequence explicit:

```lean id="r6u2ha"
example (a b c : Nat)
  (h₁ : a = b) (h₂ : b = c) :
  a + 2 = c + 2 := by
  rw [h₁, h₂]
```

When chains become long, prefer a structured form:

```lean id="t4n9be"
example (a b c : Nat)
  (h₁ : a = b) (h₂ : b = c) :
  a + 2 = c + 2 := by
  calc
    a + 2 = b + 2 := by rw [h₁]
    _     = c + 2 := by rw [h₂]
```

This localizes each step and improves maintainability.

Rewriting under binders or in function positions often requires exposing the body:

```lean id="m9x0ap"
example (a b : Nat) (h : a = b) :
  (fun x => x + a) = (fun x => x + b) := by
  funext x
  rw [h]
```

Use extensionality to reduce function equality to pointwise equality before applying lemmas.

`simp` integrates lemma-based rewriting at scale. Provide the exact lemmas needed:

```lean id="v2h8gc"
example (a b : Nat) (h : a = b) :
  a + 0 = b := by
  simp [h]
```

Prefer `simp` when the goal is normalization. Prefer `rw` when a specific transformation is intended.

A practical discipline for lemma design:

* State lemmas with the most general parameters needed for reuse.
* Orient equalities toward canonical forms.
* Avoid symmetric lemmas in the global simp set; keep one direction canonical.
* Keep premises minimal and easy to satisfy.

When a rewrite fails, inspect the lemma type and the goal. Typical issues include mismatched structure, missing arguments, or the need to rewrite an intermediate subterm first.

In summary, lemmas are the primary source of rewrite rules. Effective use depends on correct instantiation, consistent orientation, and careful sequencing.