Prove every constructor case
Split an arbitrary value into cases and prove a property in every branch.
In this course 10 / 14
Pattern matching computes a function. The cases tactic uses the same constructor split inside a proof. For an arbitrary m : Mode, cases m with opens one goal for off, one for warm, and one for bright.
After the split, each branch contains a concrete constructor. brightness and advance can now compute, turning the symbolic theorem into three closed arithmetic facts.
decide proves a closed fact by evaluating it: it works whenever the claim contains no unknowns and Lean knows how to compute whether it holds. The proof is longer than a one-line calculation because the theorem covers every possible Mode, and each case is visible and checked separately.
This pattern scales to real programs: define behaviour by constructors, then prove a property by following the same cases. If a new constructor is added later, both the function and the proof become incomplete until it is handled.
Worked example
example (m : Mode) : brightness m ≤ 2 := by
cases m with
| off => decide
| warm => decide
| bright => decideThe proof covers every mode separately. Your theorem follows two transitions in each branch before checking the arithmetic.
cases turns a theorem about an inductive value into one goal per constructor. Each branch can then use the computation rules for that constructor.
- 21. Roman to integer Easy
Prove that the brightness values of the next two modes always add to a positive number.
Suggested steps
- Split
minto all 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