Look inside a definition
unfold replaces a name by its body, so you can reason about what it does.
In this course 1 / 8
In Lean foundations you checked double 3 = 6 by computing. A claim about every n, such as double n = n + n, cannot be computed: n is unknown. You have to reason about what double does.
A proof first sees only the name double. unfold double replaces it by its definition, so you can see and use what is inside. Step through the example on the right: the goal changes from double n = n + n to n + n = n + n after the first line, and rfl closes it.
unfold only replaces names; it never finishes a proof on its own. After it, use what you already know: rfl when both sides are the same, rw [h] with an equation from the context, or exact.
If the name is not in the goal, Lean says so:
example (n : Nat) : n + 1 = 1 + n := by
unfold doubleTactic `unfold` failed to unfold `double`
Worked example
example (n : Nat) : double n = n + n := by
unfold double
rfl
def addFee (n : Nat) : Nat := n + 3
example (n : Nat) (h : n = 10) : addFee (double n) = 23 := by
unfold addFee double
rw [h]
At the start of the proof on line 1. Everything above ⊢ may be used; the line below it is what must be proved.
The second example unfolds two names in one step, then rewrites with h. After rw [h] the goal is 10 + 10 + 3 = 23, which Lean closes by computing.
unfold name shows what a definition does inside the goal. It never finishes a proof: follow it with rfl, rw or exact.
Prove that if n is 5, then double n is 10.
Suggested steps
- Unfold
double - Use the equation
h
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