4.15 Avoiding Rewrite Loops and Nontermination

Rewriting systems can diverge if rules are poorly oriented or interact cyclically. In Lean, this risk appears most often with simp, but it can also affect repeated uses of rw. The goal is to design and apply rewrite rules so that every step decreases a clear measure and reaches a stable normal form.

A rewrite loop occurs when two or more lemmas can undo each other:

a + 0 = a
a = a + 0

If both directions are available to simp, the simplifier can alternate indefinitely. Even if Lean enforces termination heuristics, performance degrades and results become unpredictable.

The primary discipline is orientation toward a canonical form. Choose one direction that reduces complexity and use it consistently. For arithmetic on natural numbers, common canonical choices include:

• Eliminate neutral elements: a + 0 → a, 0 + a → a
• Normalize constructors: push successors outward
• Avoid expansion rules such as a → a + 0

Only the reducing direction should be marked with @[simp].

Control the active rule set when necessary:

simp only [Nat.add_zero, Nat.zero_add]

This isolates the rules used and prevents accidental loops from unrelated lemmas. When a particular lemma causes oscillation, exclude it:

simp [-Nat.add_comm]

Commutativity is especially prone to loops when combined with other rules. It should rarely be a global simp lemma; instead, apply it explicitly with rw where needed.

Prefer single-step rewriting when the transformation is specific:

rw [Nat.add_comm]

This avoids giving the simplifier freedom to explore alternative paths.

Break complex rewrites into ordered steps. Use calc or a sequence of rw calls so that each transformation is intentional. This prevents back-and-forth movement between equivalent forms.

Another source of nontermination is overlapping patterns. If two simp lemmas match the same shape but lead to different results, the simplifier may alternate between them. Ensure that left-hand sides are distinct or that one strictly subsumes the other with a reducing orientation.

Localizing rules reduces risk. Use simp [h] for contextual equalities instead of adding them globally. For temporary behavior, register lemmas with a local attribute:

attribute [local simp] my_rule

Remove them once the goal is solved.

Diagnostic tools help identify problematic rules. The command:

simp?

suggests a minimal set of lemmas for the current goal. If the suggested set excludes a lemma you added, that lemma may be unnecessary or harmful.

Performance is a practical indicator. If simp becomes slow or produces unexpected forms, suspect a loop or a poorly oriented rule. Reduce the simp set and reintroduce lemmas incrementally.

A concise checklist:

• Orient rules toward simpler forms.
• Avoid symmetric rules in the simp set.
• Use simp only for critical steps.
• Exclude problematic lemmas explicitly.
• Prefer explicit rw for non-normalizing transformations.
• Keep rules local when possible.

In summary, rewriting must be directed toward a normal form. Without this discipline, automation becomes unstable. Careful orientation, controlled rule sets, and explicit sequencing ensure termination and predictable behavior.