Let the simplifier work
simp rewrites with hundreds of known facts. Read what it leaves.
In this course 2 / 8
simp, the simplifier, knows hundreds of small facts: n + 0 = n, [] ++ xs = xs, (x :: xs).head? = some x, and many more. It rewrites the goal with them, over and over, until nothing more applies.
Three things can happen. It closes the goal. It leaves a simpler goal, which you then read and finish. Or it finds nothing to do and fails with simp made no progress.
simp [h] lets it use your hypothesis h as well. With h : xs = [], it can replace xs everywhere and then simplify further.
Because simp does many steps at once, always look at the goal it leaves. Step through the second example: simp turns n + 0 + 1 = 3 into n = 2 and stops, and exact h finishes.
Worked example
example (xs : List Nat) : ([] ++ xs).length = xs.length := by
simp
example (n : Nat) (h : n = 2) : n + 0 + 1 = 3 := by
simp
exact h
At the start of the proof on line 1. Everything above ⊢ may be used; the line below it is what must be proved.
In the second example simp removed + 0 and rewrote n + 1 = 3 as n = 2, a fact it does not know but you do.
simp rewrites with many known facts and simp [h] adds yours. It may close the goal or leave a simpler one: read what it leaves.
Prove that the first item of every list built as x :: xs is some x.
Suggested steps
- Unfold
firstItem - Simplify
These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.
\to in the editor, or click:Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.
Knowledge check
Answer without looking back, then check your reasoning.
correct