# 4.6 Simplification with `simp`

# 4.6 Simplification with `simp`

The tactic `simp` performs normalization by repeated rewriting using a curated set of lemmas. In Lean, it serves as the primary automation for routine equalities. Unlike `rw`, which applies a single directed step, `simp` applies many rules until no further change occurs.

At a high level, `simp` transforms an expression into a canonical form. It uses lemmas marked with the `@[simp]` attribute, along with a built-in collection of rules. Each lemma has a left-hand side and a right-hand side. The simplifier replaces the left with the right when it matches, and repeats this process recursively.

A minimal example:

```lean id="p4x2he"
example (a : Nat) : a + 0 = a := by
  simp
```

The lemma `Nat.add_zero` is in the simp set, so `simp` reduces `a + 0` to `a`.

You can supply additional lemmas explicitly:

```lean id="o8n1kq"
example (a b : Nat) (h : a = b) :
  a + 1 = b + 1 := by
  simp [h]
```

Here `h` is used as a rewrite rule during simplification. The bracket form extends the simp set locally.

The direction of simp lemmas is fixed. Each lemma is oriented so that rewriting decreases complexity according to a heuristic measure. For example, `a + 0 = a` is a good simp lemma, while `a = a + 0` is not, since it would expand expressions and risk nontermination.

The simplifier works recursively. It descends into subterms using congruence, applies applicable lemmas, and repeats. This makes it effective for deeply nested expressions:

```lean id="2d0l7q"
example (a : Nat) :
  (a + 0) + (0 + a) = a + a := by
  simp
```

Both occurrences of `+ 0` and `0 +` are reduced automatically.

You can control where simplification applies. To simplify a hypothesis:

```lean id="1o8v3z"
simp at h
```

To simplify everything in the context:

```lean id="k2q7jd"
simp at *
```

This normalizes all hypotheses and the goal.

Custom simp lemmas are declared with an attribute:

```lean id="y3p5an"
@[simp]
theorem double_zero : (0 : Nat) + 0 = 0 := rfl
```

Once declared, the lemma participates in all future `simp` calls. Care is required when adding such lemmas. Poorly oriented or overlapping rules can cause loops or slowdowns.

A common pattern is to combine `simp` with other tactics. For example:

```lean id="3h4m8s"
example (a b : Nat) (h : a = b) :
  a + 0 = b := by
  simp [h]
```

Here `simp` both rewrites using `h` and normalizes `a + 0`.

When `simp` fails to close a goal, inspect the remaining expression. Often a missing lemma or incorrect orientation is the cause. You can test candidate lemmas by adding them locally in the bracket list.

Transparency also affects simplification. Some definitions are unfolded automatically, while others require explicit instruction:

```lean id="r2c9yw"
simp [f]
```

This forces unfolding of `f` during simplification.

A useful debugging tool is:

```lean id="5l0u7p"
simp?
```

This suggests a minimal set of lemmas that would solve the goal. It helps identify missing rules or unnecessary ones.

In practice, `simp` is used to maintain canonical forms throughout a development. Well-designed simp sets ensure that equivalent expressions normalize to the same shape. This reduces the need for manual rewriting and improves robustness.

The discipline is to write lemmas that simplify structure, avoid expansion, and compose cleanly. With this discipline, `simp` becomes a reliable normalization engine rather than a source of unpredictability.