Prove every constructor case
Split an arbitrary value into cases and prove a property in every branch.
In this course 10 / 13
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 each closed fact by evaluation. 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.
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