# 4.24 Rewriting Strategies and Heuristics

# 4.24 Rewriting Strategies and Heuristics

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.

```lean id="0rs61k"
-- 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:

```lean id="7yk2fg"
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:

```lean id="x1v6xp"
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:

```lean id="zj9w6n"
rw [h] at H
```

or:

```lean id="9m3d1p"
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:

```lean id="o8gqz2"
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:

```lean id="n2k8gk"
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:

```lean id="q3j1dr"
#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.