Prove both Boolean cases
Split an arbitrary Boolean and verify both exhaustive branches.
In this course 9 / 10
A Boolean has exactly two constructors, true and false. To prove a statement about an arbitrary b : Bool, it is enough to prove the statement in those two cases.
cases b with replaces one symbolic goal by a false branch and a true branch. In each branch, toggleBool can compute because its input constructor is visible.
Both branches finish by reflexivity, but the proof itself is not a one-line calculation about one chosen Boolean. It is an exhaustive argument covering every possible Boolean value.
The distinction matters: testing toggleBool (toggleBool true) checks one example; case analysis proves the law for all inputs and will fail visibly if the data type gains another constructor.
Worked example
example (b : Bool) : toggleBool b ≠ b := by
cases b with
| false => decide
| true => decideThe example establishes that one flip changes either Boolean. Your exercise proves that doing it twice restores the original value.
Case analysis proves a property for every value by covering every constructor. Computation then handles each concrete branch.
Prove for every Boolean that flipping twice returns the original value.
Suggested steps
- Split
binto its two constructors - Close the false branch
- Close the true branch
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