# 4.25 Common Pitfalls and Debugging

# 4.25 Common Pitfalls and Debugging

Rewriting failures in Lean usually come from a small set of recurring issues. This section lists the typical failure modes and the corresponding fixes, with a bias toward fast diagnosis.

## Pattern mismatch

`rw [h]` does nothing when the left-hand side of `h` does not match any subterm.

```lean id="j3v0p1"
-- h : a = b
-- goal contains f a, but rewrite expects a
```

Fix by matching the exact shape:

* Apply congruence: `rw [congrArg f h]`
* Reshape the goal: unfold definitions or introduce arguments
* Use `simp [h]` if normalization is intended

## Wrong orientation

The equality is correct but used in the wrong direction.

```lean id="r9q1y6"
rw [h]     -- no effect
rw [← h]   -- works
```

Always check both orientations. Prefer the direction that moves toward a canonical form.

## Hidden occurrences under binders

`rw` cannot reach terms inside lambdas or quantifiers.

```lean id="c6w3g2"
-- goal: (fun x => x + a) = (fun x => x + b)
```

Fix by exposing the body:

```lean id="v2k9t4"
funext x
rw [h]
```

or use `conv` for targeted rewriting.

## Missing arguments or implicit inference failure

A lemma requires parameters that are not inferred.

```lean id="u4m8x0"
rw [Nat.add_comm]   -- ambiguous
```

Fix by supplying arguments:

```lean id="b7p2h5"
rw [Nat.add_comm a b]
```

or by reshaping the goal so inference succeeds.

## Rewriting too much

`rw` replaces all matching occurrences, which can break structure.

```lean id="z1k5s8"
-- multiple occurrences of a
rw [h]   -- changes all
```

Fix with `conv` to target a specific occurrence.

## Rewrite loops and instability

`simp` or repeated `rw` oscillates between equivalent forms.

```lean id="q8t0n3"
-- conflicting rules
a + b ↔ b + a
```

Fix by:

* Removing symmetric rules from the simp set
* Using `simp only [...]`
* Applying `rw` explicitly for non-canonical steps

## Dependent type mismatch

Rewriting changes indices and breaks types.

```lean id="l0f3d7"
-- goal: P b, hypothesis: P a, h : a = b
```

Fix by rewriting in the correct place:

```lean id="m5v9k1"
rw [← h]
exact Ha
```

or rewrite the hypothesis instead of the goal.

## Function equality not reducing

Trying to rewrite functions directly fails.

```lean id="d9n2p6"
-- goal: f = g
rw [h]   -- no effect
```

Fix with extensionality:

```lean id="s4c7y8"
funext x
rw [h]
```

## Structure equality not decomposed

Rewriting a whole structure fails when field-level reasoning is needed.

```lean id="e3h6w2"
-- goal: p = q
rw [h]   -- insufficient
```

Fix with `ext`:

```lean id="a6u1j9"
ext
-- prove field equalities
```

## Simplifier not doing what you expect

`simp` may miss a rule or apply too many.

Fix by:

* Adding lemmas locally: `simp [h]`
* Restricting rules: `simp only [...]`
* Inspecting suggestions: `simp?`

## Diagnostic workflow

When rewriting fails:

1. Inspect the goal shape.
2. Check the lemma type and orientation.
3. Identify whether the occurrence is visible.
4. Try `rw` in both directions.
5. Switch to `simp`, `calc`, or `conv` if needed.
6. Reduce the problem to a smaller subgoal.

## Minimal example reduction

Isolate the issue:

```lean id="v1n8r4"
-- extract a smaller goal
have : ... := by
  ...
```

Work on the reduced form until the rewrite succeeds, then reinsert into the main proof.

## Summary

Most rewriting issues reduce to mismatched patterns, wrong direction, hidden structure, or uncontrolled rule sets. A systematic approach to inspecting goals, choosing tools, and applying small steps resolves these problems efficiently.