# 4.7 Controlling the `simp` Set

# 4.7 Controlling the `simp` Set

The behavior of `simp` depends entirely on the set of rewrite rules it uses. This set is composed of built-in lemmas, imported library lemmas, and user-declared rules marked with `@[simp]`. Effective use of Lean requires precise control over this set so that normalization remains predictable, terminating, and efficient.

By default, `simp` uses the global simp set. This includes standard arithmetic identities, logical simplifications, and structural rules. In many cases, this is sufficient. However, as developments grow, uncontrolled use of the global set can introduce unwanted rewrites or performance issues. Local control becomes necessary.

The simplest form of control is to extend the simp set locally:

```lean id="l7x9qa"
simp [h₁, h₂]
```

This adds the lemmas `h₁` and `h₂` for the current invocation only. These lemmas are treated as rewrite rules alongside the global set. This pattern is common when a hypothesis provides the equality needed for simplification.

You can also restrict the simp set explicitly:

```lean id="2v8c4p"
simp only [Nat.add_zero, Nat.zero_add]
```

The keyword `only` disables all other simp lemmas and uses only the listed ones. This is useful when debugging or when you need strict control over rewriting.

Removing lemmas from the simp set is done by excluding them:

```lean id="q1r5xk"
simp [-Nat.add_comm]
```

This prevents `Nat.add_comm` from being used during simplification. Such exclusions are helpful when a lemma causes undesirable rewrites or interferes with termination.

Declaring custom simp lemmas is done with the `@[simp]` attribute:

```lean id="n4z8dw"
@[simp]
theorem my_rule (a : Nat) : a + 0 = a := rfl
```

Once declared, this lemma is available globally. The choice to mark a lemma as `@[simp]` should be deliberate. A good simp lemma satisfies three conditions:

* It reduces structural complexity.
* It orients toward a canonical form.
* It does not overlap with other rules in a way that creates cycles.

For example, `a + 0 = a` is a good simp lemma, while `a = a + 0` is not. The latter expands expressions and risks nontermination.

Local simp attributes allow temporary registration:

```lean id="h3z6pk"
attribute [local simp] my_rule
```

This limits the scope of the lemma to the current section or namespace. It is useful when a rule is context-specific and should not affect the global environment.

Another level of control is simplification at specific locations. You can apply `simp` to selected hypotheses:

```lean id="m8y2qs"
simp at h₁ h₂
```

or to all hypotheses and the goal:

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

This ensures that the context remains normalized, which often simplifies subsequent reasoning.

The simplifier also supports configuration options. For example, you can control unfolding:

```lean id="t1c7vx"
simp (config := { unfoldPartialApp := true })
```

Such options are less common but become relevant in complex developments.

Debugging the simp set is essential when behavior is unexpected. The command:

```lean id="y5p2wa"
simp?
```

suggests a minimal set of lemmas that solve the goal. It reveals which rules are necessary and which may be redundant.

A practical workflow is to start with `simp`, inspect the result, and refine the simp set as needed. When proofs become unstable, switch to `simp only` to isolate the minimal required rules. Once the correct set is identified, decide whether to promote lemmas to the global simp set or keep them local.

In large projects, the simp set becomes part of the system design. Canonical forms must be consistent across modules. Lemmas must be oriented uniformly. Without this discipline, automation degrades and proofs become fragile.

In summary, controlling the simp set is about managing a rewrite system. You choose which rules apply, where they apply, and how they interact. Proper control ensures that simplification remains fast, terminating, and aligned with the intended structure of your development.