Review: build it without help
Define a type and functions, prove properties by cases and predict output, with no step checklist.
In this course 14 / 14
This lesson has no new material. Each exercise mixes ideas from the whole course, and none of them comes with a checklist of steps. The hints only point you in a direction; the full answer stays behind Reveal a solution.
Work the way you would on your own: read the task, decide what kind of Lean you need to write, write it, check it, and read what Lean reports. If you get stuck, go back to the lesson that introduced the idea before opening a hint.
The exercises cover defining an inductive type and a function by cases, proving a property for every constructor, unfolding a definition with a hypothesis, and reading arithmetic on Nat correctly.
Worked example
-- A reminder of the shapes you will need, on a different type.
inductive Coin where
| heads
| tails
def turnOver : Coin → Coin
| .heads => .tails
| .tails => .heads
example (c : Coin) : turnOver (turnOver c) = c := by
cases c with
| heads => rfl
| tails => rflAn inductive type, a function defined by cases, and a proof that follows the same cases. The exercises ask for each of these on other data, and then for more.
You can now model data, compute with it and prove properties of it without step-by-step guidance. The next course looks closely at how proofs are built from hypotheses.
Define an inductive type Light with constructors red, yellow and green. Define next : Light → Light so that red is followed by green, green by yellow and yellow by red. Define canGo : Light → Bool, which is true only for green.
\to in the editor, or click:These lines run underneath whatever you write. They are what decides the exercise, so your names and types have to match them.
example : next Light.red = Light.green := by rfl example : next Light.green = Light.yellow := by rfl example : next Light.yellow = Light.red := by rfl example : canGo Light.green = true := by rfl example : canGo Light.red = false := by rfl example : canGo Light.yellow = false := by rfl
Knowledge check
Answer without looking back, then check your reasoning.
correct