2.24 Simplification and Automation

Lean provides automation to reduce routine proof steps. The goal is to remove mechanical transformations while preserving the logical structure of the argument. The main tool is simp, supported by targeted tactics such as dsimp, simp_all, and lightweight automation like aesop.

Problem

Manual rewriting becomes repetitive:

rw [Nat.add_zero]
rw [Nat.zero_add]
rw [Nat.add_comm]

This obscures the intent. You want Lean to perform standard reductions automatically while keeping control over nontrivial steps.

The `simp` Tactic

simp applies a collection of rewrite rules tagged as simplification lemmas.

theorem simp_basic (n : Nat) :
    n + 0 = n := by
  simp

Lean uses lemmas such as Nat.add_zero automatically.

simp reduces expressions to a normal form using:

arithmetic identities
logical simplifications
definitional equalities

Using `simp` with Hypotheses

simp can use local equalities.

theorem simp_with_hyp
    (a b : Nat)
    (hAB : a = b) :
    a + 0 = b := by
  simp [hAB]

The list [hAB] adds custom rewrite rules.

Simplifying Hypotheses

theorem simp_at_hyp
    (a b : Nat)
    (hAB : a = b)
    (ha : a + 0 = 5) :
    b = 5 := by
  simp [hAB] at ha
  exact ha

simp rewrites inside ha.

Simplifying Everything

theorem simp_all_example
    (a b : Nat)
    (hAB : a = b)
    (ha : a + 0 = 5) :
    b = 5 := by
  simp_all

simp_all simplifies the goal and all hypotheses using all available information.

Use it when the context is small and stable.

Controlled Simplification

simp accepts explicit rewrite rules.

theorem simp_controlled (a b : Nat) :
    a + b = b + a := by
  simp [Nat.add_comm]

Without the explicit rule, simp may not use commutativity.

Avoiding Over-Simplification

simp may change expressions more than expected.

theorem simp_caution (a : Nat) :
    (a + 0) + 0 = a := by
  simp

This works, but the intermediate structure disappears. If the structure matters, use rw instead.

The `dsimp` Tactic

dsimp performs definitional simplification only.

def double (n : Nat) := n + n

theorem dsimp_example (n : Nat) :
    double n = n + n := by
  dsimp [double]

dsimp does not use general rewrite lemmas. It unfolds definitions.

Use it when you want predictable, minimal changes.

The `simp?` Helper

Lean can suggest simplifications.

simp?

This prints a suggested simp call with the lemmas it used.

Useful for learning which lemmas are relevant.

The `simp` Normal Form

simp aims to reduce expressions to a canonical form.

Examples:

n + 0 → n
0 + n → n
n = n → True
True ∧ P → P

Understanding this helps predict results.

Combining `simp` with Other Tactics

Typical pattern:

theorem simp_then_apply
    (a b : Nat)
    (hAB : a = b) :
    a + 0 = b := by
  simp [hAB]

Or:

theorem simp_then_exact
    (a : Nat) :
    a + 0 = a := by
  simp

Or mixed:

theorem mixed_simp_rw
    (a b : Nat)
    (hAB : a = b) :
    a + 0 = b := by
  rw [hAB]
  simp

Conditional Simplification

simp can use implications and conditions.

theorem simp_conditional
    (P : Prop)
    (h : P) :
    P ∧ True := by
  simp [h]

Lean simplifies True automatically.

Using `simp` for Logical Goals

theorem simp_logic
    (P : Prop) :
    P ∧ True -> P := by
  intro h
  simpa using h

simpa runs simp and finishes the goal.

The `simpa` Shortcut

simpa combines simp with exact.

theorem simpa_example
    (n : Nat) :
    n + 0 = n := by
  simpa

Or with hypotheses:

theorem simpa_with_hyp
    (a b : Nat)
    (hAB : a = b) :
    a + 0 = b := by
  simpa [hAB]

Lightweight Automation: `aesop`

aesop is a general-purpose automation tactic.

theorem aesop_example
    (P Q : Prop)
    (hp : P)
    (hq : Q) :
    P ∧ Q := by
  aesop

It combines introduction, elimination, and search.

Use it when the structure is routine.

Avoid it when teaching or when proof structure matters.

When to Use Automation

Use simp when:

rewriting follows standard rules
the goal should reduce to normal form
manual rewriting is repetitive

Use dsimp when:

only definitions should be unfolded

Use simpa when:

a simplified expression matches the goal

Use aesop when:

the proof is routine and structure is not important

When to Avoid Automation

Avoid automation when:

the proof teaches a concept
the structure matters
debugging is needed
the context is large and unstable

In these cases, explicit steps are clearer.

Debugging `simp`

If simp fails:

add relevant lemmas explicitly
check if the expression is in normal form
try simp? to see suggestions
use rw to guide the transformation

Example:

theorem simp_needs_help (a b : Nat)
    (hAB : a = b) :
    a + b = b + b := by
  simp [hAB]

Without [hAB], simp does not know how to replace a.

Common Patterns

Basic simplification:

simp

With hypotheses:

simp [h]

At a hypothesis:

simp at h

Everywhere:

simp_all

Shortcut:

simpa

Definition-only:

dsimp [f]

Common Pitfalls

Do not rely on simp without understanding what it does.

Do not expect simp to apply nontrivial lemmas like commutativity unless explicitly provided.

Do not use simp_all in large contexts without checking side effects.

Do not replace meaningful proof steps with automation when clarity matters.

Do not assume simp will preserve expression structure.

Takeaway

Simplification and automation reduce routine proof work. The main tool is simp, which applies standard rewrite rules to reach a canonical form. Use it to eliminate boilerplate, but keep control over key logical steps. Effective proofs combine explicit reasoning with targeted automation.

2.24 Simplification and Automation

Problem

The simp Tactic

Using simp with Hypotheses