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:

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:

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:

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:

simp at h

To simplify everything in the context:

simp at *

This normalizes all hypotheses and the goal.

Custom simp lemmas are declared with an attribute:

@[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:

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:

simp [f]

This forces unfolding of f during simplification.

A useful debugging tool is:

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.