Skip to content

4.24 Rewriting Strategies and Heuristics

Rewriting is most effective when guided by a small set of consistent strategies.

lean proof-assistant type-theory functional-programming

Rewriting is most effective when guided by a small set of consistent strategies. In Lean, uncontrolled rewriting leads to fragile proofs and poor performance. This section consolidates practical heuristics for predictable, scalable use.

Normalize to canonical forms

Choose a canonical representation and drive all expressions toward it. Examples:

  • Eliminate neutral elements: a + 0 → a
  • Normalize constructors: prefer Nat.succ at the outermost level
  • Fix argument order when using commutativity

This aligns with the simp set and reduces branching in proofs.

Separate normalization from transformation

Use simp for normalization and rw for directed changes.

-- normalization
simp

-- directed transformation
rw [h]

Mixing them without structure often obscures intent. A common pattern:

  1. Normalize (simp)
  2. Transform (rw)
  3. Normalize again (simp)

Control direction explicitly

Always choose rewrite direction deliberately:

rw [h]     -- a → b
rw [← h]   -- b → a

Prefer the direction that reduces complexity or matches a known lemma. Avoid oscillating between equivalent forms.

Keep steps small

Break complex transformations into small steps:

rw [h₁]
rw [h₂]

or use calc for longer chains. This improves debuggability and makes intermediate states visible.

Normalize context early

If a hypothesis will be reused, normalize it once:

rw [h] at H

or:

simp [h] at H

This avoids repeated rewriting and keeps the context consistent.

Prefer local over global effects

Use local rewrites and local simp extensions:

simp [h]

Avoid adding global rules unless they are universally valid and oriented correctly. Local control reduces unintended interactions.

Use extensionality when needed

When rewriting fails due to abstraction, expose structure:

funext x
rw [h]

or use ext for structures. Do not attempt to rewrite through opaque boundaries.

Switch tools when stuck

  • Use rw for precise, single-step changes.
  • Use simp for normalization.
  • Use calc for chained reasoning.
  • Use conv for targeted subterm rewriting.
  • Use cases or funext to expose structure.

Choosing the right tool is often more important than adding more lemmas.

Avoid rewrite loops

Maintain a terminating rewrite system:

  • Orient lemmas toward simpler forms
  • Avoid symmetric rules in simp
  • Use simp only when necessary
  • Exclude problematic lemmas explicitly

Inspect goals frequently

After each step, check the goal:

#check ...

or rely on the editor’s goal view. Early detection of mismatches prevents cascading errors.

Design lemmas for rewriting

Good rewrite lemmas:

  • Have clear left-hand sides
  • Reduce structural complexity
  • Avoid unnecessary premises
  • Compose well with other lemmas

Poorly designed lemmas create ambiguity and instability.

Summary

Effective rewriting follows a disciplined workflow: normalize to canonical forms, apply directed transformations, and maintain control over rule sets and direction. Small, explicit steps combined with appropriate tools yield proofs that are both robust and maintainable.