TraficLight.lean

-- 信号の色を表す型を定義する。
-- `inductive` は、場合の候補を並べて新しい型を作る。
inductive Light
  | red
  | yellow
  | green

-- 次の信号の色を返す関数。
def next
  | Light.red => Light.green
  | Light.green => Light.yellow
  | Light.yellow => Light.red

theorem red_never_direct_to_yellow : next Light.red ≠ Light.yellow := by
  -- `simp` は定義を展開して式を簡単にする。
  simp [next]

theorem next_three_times_returns_same (l : Light) : next (next (next l)) = l := by
  -- `cases l` は `l` を `red` `yellow` `green` の各場合に分ける。
  -- `<;>` は、右側の tactic をすべてのゴールに適用する。
  -- `rfl` は左右が定義上同じときに証明を閉じる。
  cases l <;> rfl