The behavior of `simp` depends entirely on the set of rewrite rules it uses.
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:
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:
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:
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:
@[simp]
theorem my_rule (a : Nat) : a + 0 = a := rflOnce 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:
attribute [local simp] my_ruleThis 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:
simp at h₁ h₂or to all hypotheses and the goal:
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:
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:
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.