1.14 Simple Rewriting

Rewriting replaces one expression with another using an equality. In Lean, equalities are values of type a = b. A rewrite step uses such a value to transform the current goal or a hypothesis. This is the basic mechanism behind many proofs that follow algebraic or equational reasoning.

Problem

You want to transform a goal by replacing a subexpression using a known equality, and you want to control the direction and location of that replacement.

Solution

Use the rw tactic with an equality.

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

Here Nat.add_comm is a theorem stating a + b = b + a. The tactic rewrites the goal using this equality and closes it.

Direction of Rewriting

An equality can be used in either direction.

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

theorem rewrite_backward (a b : Nat) : b + a = a + b := by
  rw [← Nat.add_comm]

The arrow ← reverses the direction.

Rewriting Step by Step

Consider a goal with multiple operations.

theorem step_rewrite (a b c : Nat) :
    a + b + c = c + b + a := by
  rw [Nat.add_assoc]
  rw [Nat.add_comm b c]
  rw [← Nat.add_assoc]
  rw [Nat.add_comm a c]

Each rw performs a single transformation. The sequence expresses a path from the left-hand side to the right-hand side.

Rewriting Multiple Rules

You can apply several rewrites at once.

theorem multi_rewrite (a b c : Nat) :
    a + b + c = c + b + a := by
  rw [Nat.add_assoc, Nat.add_comm b c, ← Nat.add_assoc, Nat.add_comm a c]

Lean applies the rewrites in order.

Rewriting in Hypotheses

Rewriting is not limited to goals. It can transform a hypothesis.

theorem rewrite_in_hyp (a b : Nat) (h : a = b) :
    a + a = b + a := by
  rw [h]

This replaces a with b in the goal.

You can specify the hypothesis:

theorem rewrite_specific (a b : Nat) (h : a = b) :
    a + a = b + a := by
  rw [h] at *

The at * form rewrites everywhere: in the goal and all hypotheses.

To rewrite only a specific hypothesis:

theorem rewrite_at_hyp (a b : Nat) (h : a = b) (k : a + a = a + a) :
    b + b = b + b := by
  rw [h] at k
  rw [h]

Rewriting Subexpressions

Lean rewrites matching subterms. For example:

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

The rule is applied to all matching occurrences.

Rewriting with Custom Equalities

You can define your own equality and use it.

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

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

theorem use_double (n : Nat) :
    double n + double n = (n + n) + (n + n) := by
  rw [double_expand]

The definition unfolds because double_expand provides the equality.

Chaining Rewrites with calc

For longer chains, use a calc block.

theorem calc_example (a b : Nat) :
    a + b = b + a := by
  calc
    a + b = b + a := by rw [Nat.add_comm]

A longer example:

theorem calc_chain (a b c : Nat) :
    a + b + c = c + b + a := by
  calc
    a + b + c = a + (b + c) := by rw [Nat.add_assoc]
    _ = a + (c + b) := by rw [Nat.add_comm b c]
    _ = (a + c) + b := by rw [← Nat.add_assoc]
    _ = (c + a) + b := by rw [Nat.add_comm a c]
    _ = c + (a + b) := by rw [Nat.add_assoc]
    _ = c + (b + a) := by rw [Nat.add_comm a b]

The calc style makes the sequence of equalities explicit.

Rewriting vs Simplification

rw applies specific equalities. The simp tactic applies a collection of rewrite rules automatically.

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

The difference:

• rw uses the rules you specify
• simp uses a database of lemmas

Use rw when you want precise control.

Matching Behavior

Rewriting requires a match between the left side of the equality and a subexpression of the goal.

theorem match_example (a b : Nat) :
    a + b = a + b := by
  rw [Nat.add_comm] -- fails

This fails because a + b does not match b + a. You need to guide the rewrite:

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

Understanding matching is essential when a rewrite does not apply.

Rewriting Under Binders

Rewriting can occur inside lambda expressions and other binders, but sometimes requires care.

theorem rewrite_lambda (a b : Nat) (h : a = b) :
    (fun x => x + a) = (fun x => x + b) := by
  funext x
  rw [h]

The funext step reduces equality of functions to equality of outputs.

Common Pitfalls

If rw does nothing, the pattern may not match. Check the exact form of the goal.

If rw fails, the equality may be oriented incorrectly. Try reversing it.

If too many occurrences are rewritten, use more specific lemmas or structure the goal differently.

If rewriting changes the goal in unexpected ways, inspect intermediate states step by step.

If rewriting inside functions fails, reduce the problem using funext.

Recipe: Controlled Rewriting

Start from a clear goal:

theorem example (a b : Nat) :
    a + b = b + a := by

Apply a single rewrite:

  rw [Nat.add_comm]

If the goal is more complex, rewrite one step at a time and inspect after each step.

This avoids losing track of the transformation.

Takeaway

Rewriting transforms expressions using equalities. The rw tactic applies a rule in a chosen direction to matching subterms. Precise control comes from selecting the rule, choosing its direction, and applying it step by step. Most algebraic proofs in Lean reduce to systematic rewriting.