Prove both Boolean cases
Split an arbitrary Boolean and verify both exhaustive branches.
In this course 11 / 13
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.
The proof is not a one-line calculation about one chosen Boolean. It is an exhaustive argument covering every possible Boolean value, and each branch is closed by computation.
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. With two Boolean variables there are four combinations, and splitting on one inside each branch of the other covers them all.
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