Lean4

Review: pick the right tool

Mixed proofs about lights and fees, with no step checklist.

New lesson18 minBeginnerreviewno checklist
0/8 completed in this course
In this course 8 / 8
Go to exercise ↓

No new material: each exercise mixes the tools of this course, and none has a checklist. Before each one, ask which tool fits the goal: unfold to look inside a definition, simp to simplify, omega for arithmetic, cases to split a value of an inductive type, contradiction for impossible branches.

The traffic light from Lean foundations is given above the editor: next moves red to green, green to yellow and yellow to red, and canGo is true only for green.

Worked example

example (l : Light) (h : l = Light.red) : canGo (next l) = true := by
  rw [h]
  rfl
Step through the proof1 / 3

At the start of the proof on line 1. Everything above ⊢ may be used; the line below it is what must be proved.

l:Light
h:l = Light.red
⊢canGo (next l) = true

With h the light is known, so after rewriting everything computes.

Takeaway

Match the tool to the goal: unfold to look inside, simp to simplify, omega for arithmetic, cases to split, contradiction for the impossible.

Exercise 1 of 4

Prove that after three steps a light is back where it started.

Exercise.lean
1inductive Light where
2 | red
3 | yellow
4 | green
5
6def next : Light → Light
7 | .red => .green
8 | .green => .yellow
9 | .yellow => .red
10
11def canGo : Light → Bool
12 | .green => true
13 | _ => false
14theorem exercise (l : Light) : next (next (next l)) = l := by
given
Loading editor…

Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.

l:Light
⊢next (next (next l)) = l
ReadyLn 1, Col 1Lean 4
Draft saved in this browser
Stuck?
Recall and apply

Knowledge check

Answer without looking back, then check your reasoning.

0of 2
correct
Question 1 of 2Which tool splits l : Light into its three cases?
Question 2 of 2After unfold, the goal is plain arithmetic with a hypothesis. What finishes it?