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:

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:

example (a b : Nat) : a + b = b + a := by
  rw [Nat.add_comm]

If inference is insufficient, supply arguments explicitly:

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:

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:

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:

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:

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:

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:

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:

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:

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.