Practise it in the Academy:Simplify a goal →

Module 2 · Lesson 3

simp — Simplification

simp rewrites the goal repeatedly with a large set of simplification lemmas until none applies. It takes care of routine steps, which leaves the parts of the proof that need an idea.

The Power of simp

Where rw applies one rule at a time, simpapplies many rules repeatedly until nothing more simplifies. It's like having an assistant that automatically cleans up your proof:

lean

1example (n : Nat) : n + 0 + 0 + 0 = n := by
2  simp  -- Removes all the + 0s automatically
3
4example (a b c : Nat) : a + b + c + 0 = c + (b + a) := by
5  simp [Nat.add_comm, Nat.add_assoc]
6  -- Simplifies and uses commutativity/associativity
7
8example : [1, 2] ++ [] ++ [3] = [1, 2, 3] := by
9  simp  -- Handles list operations
10
11-- simp can often close goals completely
12example (xs : List Nat) : xs ++ [] = xs := by simp
13example (n : Nat) : 0 + n = n := by simp

Key Takeaway

simp repeatedly applies simplification lemmas until the goal can't be simplified further. It often closes goals completely.

When to Use simp

Reach for simp when:

Cleaning up obvious stuff: Arithmetic identities, list operations, boolean simplification
You don't care about the exact steps: Just want the goal simplified
Combining many small rewrites: Instead of chaining 5 rws
Working interactively: Try simp first, then refine if needed

What simp Knows

Lemmas marked with @[simp] are automatically used by simp. Lean's standard library has hundreds of these:

lean

1-- These are in the library with @[simp]
2#check @Nat.add_zero    -- n + 0 = n
3#check @Nat.zero_add    -- 0 + n = n
4#check @Nat.mul_one     -- n * 1 = n
5#check @Nat.one_mul     -- 1 * n = n
6#check @List.append_nil -- xs ++ [] = xs
7#check @List.nil_append -- [] ++ xs = xs
8#check @Bool.not_not    -- !!b = b
9
10example (n : Nat) : n + 0 = n := by simp
11example (xs : List Nat) : xs ++ [] = xs := by simp
12example (b : Bool) : !!b = b := by simp

Adding Lemmas to simp

Provide extra lemmas in brackets—your hypotheses or other lemmas you want applied:

lean

1example (a b : Nat) (h : a = 5) : a + b = 5 + b := by
2  simp [h]  -- Uses h : a = 5 as a simp rule
3
4example (f : Nat → Nat) (hf : ∀ n, f n = n + 1) : f 5 = 6 := by
5  simp [hf]  -- Applies hf to simplify f 5
6
7-- Multiple lemmas
8example (a b : Nat) (h1 : a = 0) (h2 : b = 0) : a + b = 0 := by
9  simp [h1, h2]
10
11-- Using with local definitions
12def triple (n : Nat) := 3 * n
13example : triple 4 = 12 := by simp [triple]

simp only — Precise Control

Use simp only to control exactly which lemmas are used. This is preferred in libraries because it's reproducible:

lean

1example (n : Nat) : n + 0 + 0 = n := by
2  simp only [Nat.add_zero]
3  -- Only uses Nat.add_zero, not the full simp database
4
5-- This is more predictable and often faster
6example (a b : Nat) (h : a = b) : a + 0 = b := by
7  simp only [Nat.add_zero, h]
8
9-- simp? tells you what simp only would need
10example (n : Nat) : n + 0 = n := by
11  simp?  -- Output: "Try this: simp only [Nat.add_zero]"

💡

simp only is preferred in proof libraries because it's reproducible—it won't break if new simp lemmas are added to the database. Use simp? to discover what lemmas you need.

Common Mistakes

Mistake 1: Expecting simp to prove everything

lean

1-- simp cannot prove everything
2-- example (a b c : Nat) : a * (b + c) = a * b + a * c := by simp  
3-- ❌ Fails! Distributivity isn't a simp lemma
4
5-- ✓ Use ring for algebraic identities
6example (a b c : Nat) : a * (b + c) = a * b + a * c := by ring
7
8-- ✓ Or provide the lemma explicitly
9example (a b c : Nat) : a * (b + c) = a * b + a * c := by
10  rw [Nat.mul_add]

Mistake 2: Using simp in the middle of proofs

lean

1-- simp can change your goal in unexpected ways
2-- This can make it hard to continue the proof
3
4-- ❌ Risky: simp might change things you didn't expect
5example (a b c : Nat) (h : a = b) : a + c = b + c := by
6  simp  -- Does not close the goal: it leaves a = b, because h is not used
7  -- Now what?
8
9-- ✓ Better: use simp only with specific lemmas
10example (a b c : Nat) (h : a = b) : a + c = b + c := by
11  simp only [h]  -- Predictable

Mistake 3: Forgetting simp_all when you need hypotheses

lean

1example (a b : Nat) (h1 : a = 5) (h2 : b = 3) : a + b = 8 := by
2  simp  -- ❌ Might not work—doesn't automatically use h1, h2
3
4example (a b : Nat) (h1 : a = 5) (h2 : b = 3) : a + b = 8 := by
5  simp_all  -- ✓ Uses all hypotheses as simp rules

Simplifying Hypotheses

Like rw, you can simplify hypotheses with at:

lean

1example (n : Nat) (h : n + 0 = 5) : n = 5 := by
2  simp at h
3  -- h becomes: n = 5
4  exact h
5
6example (a b : Nat) (h1 : a + 0 = b) (h2 : b + 0 = 5) : a = 5 := by
7  simp at *
8  -- Simplifies all hypotheses and the goal
9  rw [h1, h2]
10
11-- At specific hypotheses
12example (a b : Nat) (h1 : a + 0 = 3) (h2 : b = 4) : a + b = 7 := by
13  simp at h1
14  simp [h1, h2]

simp Variants — Complete Guide

Lean provides several variants of simp, each optimized for different situations. Knowing which variant to use can make your proofs cleaner and faster.

simp — The Default

Plain simp uses the entire simp lemma database. It's great for exploration but can be unpredictable as the database grows.

lean

1-- Uses all @[simp] lemmas in scope
2example (n : Nat) : n + 0 = n := by simp
3example (xs : List Nat) : xs ++ [] = xs := by simp
4
5-- You can add extra lemmas in brackets
6example (a : Nat) (h : a = 5) : a + 0 = 5 := by simp [h]

simp only — Precise Control

simp only uses ONLY the lemmas you specify—nothing from the database. This is the preferred choice for library code because it's reproducible and won't break when new simp lemmas are added.

lean

1-- Only uses the lemmas you list
2example (n : Nat) : n + 0 + 0 = n := by
3  simp only [Nat.add_zero]
4
5-- Won't change if simp database changes
6example (a b : Nat) (h : a = b) : a + 0 = b := by
7  simp only [Nat.add_zero, h]
8
9-- Use simp? to discover what lemmas you need
10example (n : Nat) : 0 + n + 0 = n := by
11  simp?
12  -- Output: Try this: simp only [Nat.zero_add, Nat.add_zero]

simp_all — Simplify Everything

simp_all simplifies both the goal AND all hypotheses, treating each hypothesis as a potential simp rule. It helps when many hypotheses need tidying at once.

lean

1-- Simplifies hypotheses AND goal, using all hypotheses as rules
2example (a b : Nat) (h1 : a = 5) (h2 : b = 3) : a + b + 0 = 8 := by
3  simp_all
4  -- h1 and h2 are used as rewrite rules + Nat.add_zero is applied
5
6-- Often closes goals that plain simp can't
7example (p q : Prop) (hp : p) (hq : q) : p ∧ q := by simp_all
8
9-- Great for propositional cleanup
10example (a b : Nat) (h : a = b) (hb : b = 0) : a = 0 := by simp_all

simp? — Discovery Mode

simp? runs simp and then suggests the minimal simp onlycall that would achieve the same result. Use this to convert exploratory simpcalls into reproducible simp only calls.

lean

1example (n : Nat) : n + 0 = n := by
2  simp?
3  -- Output: Try this: simp only [Nat.add_zero]
4  -- Click the suggestion or copy it!
5
6-- Also works with extra lemmas
7example (a : Nat) (h : a = 5) : a + 0 = 5 := by
8  simp? [h]
9  -- Output: Try this: simp only [Nat.add_zero, h]

💡

Workflow: Use simp while exploring, then run simp?to get the exact lemmas, and replace with simp only for the final proof.

simp +arith — With Arithmetic

simp +arith turns on simp's arithmetic normalization. It can handle goals involving addition, subtraction, and simple arithmetic. It replacessimp_arith, which is deprecated.

lean

1-- Handles arithmetic that plain simp doesn't
2example (n : Nat) : n + 1 - 1 = n := by simp +arith
3
4example (a b : Nat) : a + b + 1 = 1 + a + b := by simp +arith
5
6-- Combines with regular simp rules
7example (n : Nat) : (n + 0) + 1 - 1 = n := by simp +arith

dsimp — Definitional Simplification Only

dsimp only applies simplifications that are definitionally equal—no proof obligations, just computation. It's lighter than simp, and it fails when it cannot change the goal.

lean

1-- Only unfolds definitions, no rewriting
2def myConst := 42
3example : myConst = 42 := by dsimp [myConst]  -- unfolds, then 42 = 42 closes
4
5-- Great for unfolding let-bindings
6example : (let x := 5; x + x) = 10 := by
7  dsimp only  -- Unfolds the let and computes 5 + 5
8
9-- dsimp only uses lemmas that hold by rfl. List.append_nil is proved
10-- by induction, so dsimp would make no progress here; simp can use it
11example (xs : List Nat) : xs ++ [] = xs := by
12  simp

simp at — Target Specific Locations

Use at to simplify hypotheses instead of (or in addition to) the goal.

lean

1-- Simplify a specific hypothesis
2example (n : Nat) (h : n + 0 = 5) : n = 5 := by
3  simp at h  -- h becomes: n = 5
4  exact h
5
6-- Simplify multiple hypotheses
7example (a b : Nat) (h1 : a + 0 = 3) (h2 : b + 0 = 4) : a + b = 7 := by
8  simp at h1 h2  -- Both get simplified
9  omega
10
11-- Simplify everything (all hypotheses + goal)
12example (a b : Nat) (h1 : a + 0 = b) (h2 : b + 0 = 5) : a = 5 := by
13  simp at *  -- Simplifies h1, h2, and goal
14  omega
15
16-- Simplify hypothesis and NOT the goal (use ⊢ for goal)
17example (n : Nat) (h : n + 0 = n + 0) : n + 0 = n := by
18  simp only [Nat.add_zero] at h ⊢

simp [-lemma] — Excluding Lemmas

Sometimes simp applies a lemma you don't want. Use -lemma_nameto exclude specific lemmas from being used.

lean

1-- Remove a lemma from the simp set with -name
2example (xs : List Nat) : (xs ++ []).length = xs.length := by
3  simp [-List.length_append]  -- simp still succeeds, using List.append_nil instead
4
5-- Useful when a lemma loops or rewrites the goal into a form you do not want

Defining Your Own Simp Lemmas

lean

1def double (n : Nat) : Nat := n + n
2
3-- Mark as simp lemma with @[simp]
4@[simp]
5theorem double_zero : double 0 = 0 := rfl
6
7@[simp]
8theorem double_succ (n : Nat) : double (n + 1) = double n + 2 := by
9  simp [double]
10  ring
11
12-- Now simp uses these automatically
13example : double 0 + double 0 = 0 := by simp
14example : double 1 = 2 := by simp

Deep Dive: How simp Works

simp works by repeatedly applying rewrite rules in a specific order until a fixed point is reached:

Collect all applicable simp lemmas (from database + provided list)
Try to apply each lemma to subterms of the goal
If any lemma matches, apply it and restart from step 2
Continue until no more lemmas apply (fixed point)

Good simp lemmas always "simplify"—they make terms smaller or more canonical. Bad simp lemmas can cause infinite loops (like bare commutativitya + b = b + a).

lean

1-- ✓ Good simp lemma: always simplifies
2@[simp] theorem add_zero (n : Nat) : n + 0 = n := ...
3
4-- ❌ Bad simp lemma: would loop forever
5-- @[simp] theorem add_comm : a + b = b + a  -- Don't do this!

When simp Doesn't Work

If simp doesn't close your goal, try these alternatives:

lean

1-- For arithmetic/algebra: use ring, omega, or linarith
2example (a b c : Nat) : a + (b + c) = (a + b) + c := by
3  ring  -- or: rw [Nat.add_assoc]
4
5example (n : Nat) (h : n > 5) : n > 3 := by
6  omega
7
8-- For specific rewrites: use rw
9example (a b : Nat) (h : a = b) : a + 1 = b + 1 := by
10  rw [h]
11
12-- For case analysis: use cases or decide
13example (b : Bool) : b || true = true := by
14  cases b <;> simp

Best Practices

Try simp first when exploring. It often closes the goal or gets close.
Use simp? to discover what lemmas you need, then convert to simp only
In libraries, prefer simp only for reproducibility
Use simp_all when you want hypotheses used automatically
Don't fight simp. If it does not help, switch to rw or another tactic.

Exercise 1: Basic simp

Use simp to close this goal.

lean

1example (xs : List Nat) : [] ++ xs ++ [] = xs := by
2  simp

Exercise 2: simp with Hypothesis

Use simp with a hypothesis to close the goal.

lean

1example (n : Nat) (h : n = 3) : n + 0 = 3 := by
2  simp [h]

Exercise 3: simp? Discovery

Use simp? to find out what lemmas you need.

lean

1example (a b : Nat) : a + 0 + b + 0 = a + b := by
2  simp?  -- Proves it and suggests: simp only [Nat.add_zero]
3
4-- Then replace simp? with the suggestion:
5example (a b : Nat) : a + 0 + b + 0 = a + b := by
6  simp only [Nat.add_zero]

rw — Rewriting Next: exact & apply