Proofs

Simplify with simp

Simplify expressions with library lemmas and selected definitions.

-- simp repeatedly applies registered simplification lemmas.
example (n : Nat) : 0 + n + 0 = n := by
  simp

-- simp only makes the lemma list explicit.
example (n : Nat) : 0 + n + 0 = n := by
  simp only [Nat.zero_add, Nat.add_zero]

def addZero (n : Nat) : Nat := 0 + n

-- [addZero] asks simp to unfold this definition.
example (n : Nat) : addZero n = n := by
  simp [addZero]

-- Simplify a hypothesis, then use it to finish the goal.
example (n : Nat) (h : n + 0 = 8) : n = 8 := by
  simp only [Nat.add_zero] at h
  exact h

Explanation

`simp`

Rewrites toward simpler forms using tagged lemmas and simplification procedures. It may close a goal, but it is not a procedure for proving every true statement.

`simp [addZero]`

Adds the defining equations of addZero to the simplification rules.

`simp only […] at h`

Restricts the lemma set and simplifies the hypothesis named h. Without at h, the tactic simplifies the goal.

Expected output

Reference only. Run the file to check its actual result.

File checked successfully.

Exercise

Add a proof that addZero (addZero n) = n using simp [addZero].