Skip to content

2.23 Rewriting Strategies

Rewriting with equality is one of the most frequent operations in Lean.

lean proof-assistant type-theory logic proof-theory rewriting

Rewriting with equality is one of the most frequent operations in Lean. At scale, the challenge is not knowing that rw exists, but deciding what to rewrite, where, and in which direction so the proof remains stable and readable.

Problem

You have equalities available, but naive rewriting:

  • fails because the shape does not match
  • succeeds but makes the goal harder
  • applies too broadly and breaks later steps

You need a disciplined approach.

Core Strategy

Before rewriting, answer three questions:

  1. Where is the mismatch between goal and context?
  2. Which equality aligns them?
  3. In which direction should it be applied?

Aligning Goal and Hypotheses

A common pattern is aligning a hypothesis to match the goal.

theorem rewrite_align_goal
    (a b : Nat)
    (hAB : a = b)
    (ha : a + 1 = 5) :
    b + 1 = 5 := by
  rw [hAB] at ha
  exact ha

Instead of rewriting the goal, rewrite the hypothesis so it directly solves the goal.

Rewriting the Goal

When the goal differs by a known equality, rewrite the goal.

theorem rewrite_goal
    (a b : Nat)
    (hAB : a = b) :
    a + 1 = b + 1 := by
  rw [hAB]

After rewriting, the goal becomes reflexive.

Choosing Direction

Direction is often the main decision.

hAB : a = b
  • rw [hAB] replaces a with b
  • rw [← hAB] replaces b with a

Example:

theorem rewrite_direction
    (a b : Nat)
    (hAB : a = b)
    (hb : b + 1 = 5) :
    a + 1 = 5 := by
  rw [← hAB]
  exact hb

If rewriting fails, try reversing direction first.

Rewriting to Simplify

Often rewriting is used to reduce expressions to canonical forms.

theorem rewrite_simplify (n : Nat) :
    n + 0 = n := by
  rw [Nat.add_zero]

Or:

theorem rewrite_simplify_chain (n : Nat) :
    (n + 0) + 0 = n := by
  rw [Nat.add_zero, Nat.add_zero]

Rewrite until the expression reaches a normal form.

Combining with simp

simp applies many rewrite rules automatically.

theorem rewrite_vs_simp (n : Nat) :
    n + 0 = n := by
  simp

Guideline:

  • use rw when you want control
  • use simp when the transformation is standard

You can combine them:

theorem rewrite_then_simp (a b : Nat)
    (hAB : a = b) :
    a + 0 = b := by
  rw [hAB]
  simp

Rewriting Multiple Equalities

Apply rewrites in sequence.

theorem rewrite_chain
    (a b c : Nat)
    (hAB : a = b)
    (hBC : b = c) :
    a + 1 = c + 1 := by
  rw [hAB, hBC]

Order matters. Each rewrite transforms the goal for the next step.

Rewriting Inside Hypotheses

Sometimes the goal is already correct, but a hypothesis needs adjustment.

theorem rewrite_inside_hyp
    (a b : Nat)
    (hAB : a = b)
    (ha : a + 2 = 7) :
    b + 2 = 7 := by
  rw [hAB] at ha
  exact ha

This avoids modifying the goal unnecessarily.

Rewriting Everywhere 

rw [h] at *

This rewrites both the goal and all hypotheses.

Use with care. It may introduce unwanted changes.

Controlling Occurrences

By default, all matching occurrences are rewritten.

theorem rewrite_all_occurrences
    (a b : Nat)
    (hAB : a = b) :
    a + a = b + b := by
  rw [hAB]

To rewrite a single occurrence:

theorem rewrite_one_occurrence
    (a b : Nat)
    (hAB : a = b) :
    a + a = b + a := by
  nth_rewrite 1 [hAB]

This is useful when full rewriting overshoots the target.

Rewriting Under Functions

Rewriting works inside expressions.

theorem rewrite_under_function
    (a b : Nat)
    (hAB : a = b)
    (f : Nat -> Nat) :
    f a = f b := by
  rw [hAB]

Lean propagates the equality through function application.

Rewriting Predicates

Rewriting also works for propositions.

theorem rewrite_predicate
    (a b : Nat)
    (P : Nat -> Prop)
    (hAB : a = b)
    (ha : P a) :
    P b := by
  rw [hAB] at ha
  exact ha

This is transport of proofs along equality.

Rewriting to Match a Lemma

A common use is rewriting so a lemma applies.

theorem rewrite_for_lemma
    (a b : Nat)
    (hAB : a = b) :
    a + 0 = b := by
  rw [hAB]
  apply Nat.add_zero

The rewrite aligns the goal with the lemma.

Rewriting with Definitions

Definitions may need unfolding.

def double (n : Nat) := n + n

theorem rewrite_definition (n : Nat) :
    double n = n + n := by
  rfl

If not automatic:

theorem rewrite_definition_unfold (n : Nat) :
    double n = n + n := by
  unfold double
  rfl

Rewriting vs calc

For longer chains, use calc.

theorem rewrite_calc
    (a b c : Nat)
    (hAB : a = b)
    (hBC : b = c) :
    a = c := by
  calc
    a = b := hAB
    _ = c := hBC

This is clearer than a long rw sequence.

Debugging Failed Rewrites

If rw fails:

  • check if the term actually appears
  • check direction
  • check if the expression is hidden behind a definition
  • try simp or unfold

Example failure:

-- no occurrence of a
-- rw [hAB]

Lean cannot rewrite what is not present.

Common Patterns

Rewrite goal:

rw [h]

Rewrite backward:

rw [← h]

Rewrite hypothesis:

rw [h] at ha

Rewrite many:

rw [h1, h2, h3]

Rewrite everywhere:

rw [h] at *

Rewrite one occurrence:

nth_rewrite 1 [h]

Common Pitfalls

Do not rewrite blindly. Each rewrite should move the goal toward a simpler or more canonical form.

Do not use rw when simp expresses the intent better.

Do not rewrite in the wrong direction and make the goal more complex.

Do not apply rw ... at * in large contexts without checking side effects.

Do not rely on fragile expression shapes. Minor definition changes can break such proofs.

Takeaway

Rewriting is controlled substitution guided by equality. Effective use depends on choosing the right direction, location, and sequence. The goal is not to rewrite as much as possible, but to rewrite just enough to align the goal with known facts or canonical forms.