48. What comes before red

EasyProofFree10 points

A traffic light cycles red → green → yellow → red. Prove that if next l is red, then l is yellow.

Two of the three cases are impossible, and Lean has to be told so.

Solution.lean

1inductive Light where

2 | red

3 | yellow

4 | green

6def next : Light → Light

7 | .red => .green

8 | .green => .yellow

9 | .yellow => .red

10theorem solution (l : Light) (h : next l = Light.red) : l = Light.yellow := by

given

Loading editor…

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

l:Light

h:next l = Light.red

⊢l = Light.yellow

ReadyLn 1, Col 1Lean 4

Draft saved in this browser