Proving · 7 min
Simplification with simp
simp rewrites with registered simplification lemmas and basic reductions. It simplifies goals such as 0 + n + 0 = n without requiring you to name every step.
simp [bump] additionally unfolds the definition bump. simp only [Nat.zero_add, Nat.add_zero] instead restricts the lemma set. The at h suffix directs simplification at a hypothesis.
Use simp? while exploring a proof to obtain a suggested simp only call. A focused lemma list can make the proof easier to maintain. Simplification is not a complete solver for all mathematics.
Exercise
Prove bump n = n by simplifying the definition of bump.
Open exercise in editordef bump (n : Nat) : Nat := 0 + n + 0
theorem bump_eq (n : Nat) : bump n = n := by
sorry
Hint
The proof is simp [bump]. The brackets ask Lean to unfold bump before simplifying.
Solution
def bump (n : Nat) : Nat := 0 + n + 0
theorem bump_eq (n : Nat) : bump n = n := by
simp [bump]