Lean4
LanguageTacticsCourse
Module 3 · Lesson 3

simp Attributes

Control simp's behavior with attributes. Mark lemmas as @[simp] to include them automatically in simplification.

The @[simp] Attribute

Mark lemmas with @[simp] to add them to simp's default lemma set:

lean
1@[simp]
2theorem double_zero : double 0 = 0 := rfl
3
4@[simp]
5theorem double_succ (n : Nat) : double (n + 1) = double n + 2 := by
6  simp [double]
7  ring
8
9-- Now simp uses these automatically
10example : double 0 = 0 := by simp
11example : double 1 = 2 := by simp
Key Takeaway
@[simp] lemmas should rewrite left-to-right to simpler forms. They run automatically whenever you callsimp.

Good simp Lemmas

lean
1-- Good: simplifies to a simpler form
2@[simp] theorem add_zero (n : Nat) : n + 0 = n := rfl
3@[simp] theorem mul_one (n : Nat) : n * 1 = n := rfl
4@[simp] theorem not_not (b : Bool) : !!b = b := by cases b <;> rfl
5
6-- Good: reduces constructors
7@[simp] theorem fst_pair (a : α) (b : β) : (a, b).1 = a := rfl
8@[simp] theorem head_cons (x : α) (xs : List α) : (x :: xs).head? = some x := rfl

Bad simp Lemmas

lean
1-- Bad: loops forever!
2-- @[simp] theorem comm (a b : Nat) : a + b = b + a  -- DON'T DO THIS
3
4-- Bad: makes terms bigger
5-- @[simp] theorem expand (n : Nat) : n = n + 0  -- Wrong direction!
6
7-- Bad: conditional without clear simplification
8-- @[simp] theorem weird (n : Nat) (h : n > 0) : n = n  -- Useless
⚠
Never add commutative laws like a + b = b + a as simp lemmas—they cause infinite loops! Simp would keep swapping forever.

simp only

lean
1-- simp only uses ONLY the lemmas you specify
2example (a b : Nat) : a + 0 + b = a + b := by
3  simp only [Nat.add_zero]
4  -- Only applies add_zero, nothing else
5
6-- Useful for controlled simplification
7example (xs : List Nat) : (xs ++ []).length = xs.length := by
8  simp only [List.append_nil]

Local simp Lemmas

lean
1-- Use hypotheses as simp lemmas
2example (a b : Nat) (h : a = b) : a + 1 = b + 1 := by
3  simp [h]  -- Uses h : a = b as a rewrite rule
4
5-- simp [*] uses ALL hypotheses
6example (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c := by
7  simp [*]

simp_all

lean
1-- simp_all simplifies goal AND all hypotheses
2example (a b : Nat) (h : a + 0 = b) : a = b := by
3  simp_all
4  -- Simplified h to: a = b, then used it
5
6-- Powerful for cleaning up messy contexts
7example (P Q : Prop) (h1 : P ∧ True) (h2 : Q ∧ P) : P := by
8  simp_all  -- Simplifies h1 to P, extracts P
Deep Dive: simp's Lemma Database

When you call simp, it uses:

  1. All lemmas marked @[simp] in scope
  2. Built-in definitional equalities
  3. Any lemmas you pass explicitly with simp [lemma]
lean
1-- See what simp lemmas exist for a type
2#check @List.append_nil  -- Has @[simp]
3#check @Nat.add_zero     -- Has @[simp]

simp? for Discovery

lean
1-- simp? tells you which lemmas it used
2example (xs : List Nat) : (xs ++ []).reverse = xs.reverse := by
3  simp?
4  -- Suggests: simp only [List.append_nil]
5
6-- Useful for:
7-- 1. Understanding what simp did
8-- 2. Replacing simp with explicit simp only
9-- 3. Learning which lemmas exist

Examples

Custom Type with simp Lemmas

lean
1structure Vec3 where
2  x : Float
3  y : Float
4  z : Float
5
6def Vec3.zero : Vec3 := ⟨0, 0, 0⟩
7
8def Vec3.add (v w : Vec3) : Vec3 := 
9  ⟨v.x + w.x, v.y + w.y, v.z + w.z⟩
10
11@[simp]
12theorem Vec3.add_zero (v : Vec3) : v.add Vec3.zero = v := by
13  simp [Vec3.add, Vec3.zero]
14  -- Would need Float lemmas to complete

Controlled Simplification

lean
1example (xs ys : List Nat) (h : xs = []) : 
2    (xs ++ ys).length = ys.length := by
3  simp only [h, List.nil_append]
decideNext: calc