Prove every case
Split a value of your own type into cases; close impossible ones with contradiction.
In this course 5 / 8
A claim about an unknown m : Mode cannot be computed, because Lean does not know which mode m is. But there are only three possibilities. cases m with splits the proof into one goal for each constructor:
example (m : Mode) : advance (advance (advance m)) = m := by
cases m with
| off => rfl
| warm => rfl
| bright => rflIn each branch m is replaced by one concrete constructor, so everything computes and rfl closes it. For a claim that is not an equation, such as brightness m ≤ 2, use decide: it works out a claim with no unknowns left and accepts it if it is true.
Sometimes a branch is impossible. If you know h : brightness m = 2, then in the off branch h becomes 0 = 2, which can never hold. contradiction closes a goal whose hypotheses contradict themselves, such as an equation between two different numbers or constructors.
This is how proofs about programs often go: the function was defined case by case, so the proof follows the same cases.
Worked example
example (m : Mode) : brightness m ≤ 2 := by
cases m with
| off => decide
| warm => decide
| bright => decide
At the start of the proof on line 1. Everything above ⊢ may be used; the line below it is what must be proved.
Each branch is a concrete comparison, such as 1 ≤ 2 for warm, which decide settles.
cases gives one goal per constructor. In each one things compute, decide settles concrete claims, and contradiction closes impossible branches.
Prove that the brightness of the next two modes always adds up to a positive number.
Suggested steps
- Split
minto its three constructors - Prove the
offbranch - Prove the
warmbranch - Prove the
brightbranch
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