RideStateMachine.lean

inductive RideStatus
  | requested
  | rejected
  | assigned
  | pickedUp

structure Driver where
  name : String

-- Ride は現在の状態と、必要なら担当ドライバーを持つ。
-- `driver : Option Driver` の `Option` は
-- 「値があるかもしれないし、ないかもしれない」型。
structure Ride where
  status : RideStatus
  driver : Option Driver

-- 配車リクエスト直後は、状態は requested でドライバーは未定。
def requestRide : Ride := { status := .requested, driver := none }

-- requested のときだけドライバーを割り当てられる。
-- 成功すると `some Ride`、不正な状態なら `none` を返す。
-- `some x` は「値がある」ケースで、`x` を包んだ値。
-- `none` は「値がない」ケース。
def assignDriver (ride : Ride) (driver : Driver) : Option Ride :=
  match ride.status with
  | .requested => some { ride with status := .assigned, driver := some driver }
  | _ => none

-- requested のときだけ rejected に進める。
-- reject しても driver は割り当てられない。
def rejectRide (ride : Ride) : Option Ride :=
  match ride.status with
  | .requested => some { ride with status := .rejected, driver := none }
  | _ => none

-- assigned のときだけ pickedUp に進める。
def pickUp (ride : Ride) : Option Ride :=
  match ride.status with
  | .assigned => some { ride with status := .pickedUp }
  | _ => none

-- requested からは reject できる。
theorem request_can_be_rejected :
  rejectRide requestRide = some { status := .rejected, driver := none } := by
  simp [requestRide, rejectRide]

-- requested から、直接 pickedUp に進めることはできない。
theorem request_cannot_be_picked_up_directly :
  pickUp requestRide = none := by
  simp [requestRide, pickUp]

-- requested から assigned にドライバーを割り当てられる。
theorem request_ride_can_be_picked_up_with_driver (driver : Driver) :
  -- `>>=` は bind と呼ばれる演算子。
  -- ここでは `Option` 用の bind なので、次のように動く:
  --   `some ride >>= pickUp` は `pickUp ride`
  --   `none >>= pickUp` は `none`
  -- つまり「assignDriver が成功したときだけ、その結果を pickUp に渡す」。
  (assignDriver requestRide driver >>= pickUp) =
    some { status := .pickedUp, driver := some driver } := by
  simp [requestRide, assignDriver, pickUp]

-- ここから先は、上で定義した遷移を使って「どんな Ride が到達可能か」を考える。

-- `Reachable ride` は
-- 「その `ride` は、このファイルで定義した正しい遷移だけを使って到達できる」
-- という性質を表す述語。
--
-- `Ride` の型そのものは、例えば
-- `{ status := .pickedUp, driver := none }`
-- のような不正な値も作れてしまう。
-- そこで「ありうる Ride 全体」ではなく、
-- 「初期状態から正しい操作で到達した Ride」に話を限定する。
--
-- `Prop` は `proposition` の略で、「真か偽かを主張する命題の型」を表す。
-- つまり `Reachable : Ride -> Prop` は、各 `Ride` について
-- 「その Ride は到達可能か」という命題を返す、という意味。
--
-- `inductive` で `Prop` を作ると、
-- 「どんなときに `Reachable ride` を証明してよいか」を
-- コンストラクタで列挙できる。
inductive Reachable : Ride -> Prop where
  -- 初期状態 `requestRide` は到達可能。
  | request : Reachable requestRide
  -- 既に到達可能な `ride` に対して、`rejectRide` が成功して `next` になったなら、
  -- その `next` も到達可能。
  | reject (ride : Ride) (next : Ride) :
      Reachable ride ->
      rejectRide ride = some next ->
      Reachable next
  -- 既に到達可能な `ride` に対して、`assignDriver` が成功して `next` になったなら、
  -- その `next` も到達可能。
  | assign (ride : Ride) (driver : Driver) (next : Ride) :
      Reachable ride ->
      assignDriver ride driver = some next ->
      Reachable next
  -- 既に到達可能な `ride` に対して、`pickUp` が成功して `next` になったなら、
  -- その `next` も到達可能。
  | pickUp (ride : Ride) (next : Ride) :
      Reachable ride ->
      pickUp ride = some next ->
      Reachable next

-- pickedUp なら、既にドライバーが割り当てられている。
theorem picked_up_has_driver {ride : Ride} :
  Reachable ride ->
  ride.status = .pickedUp ->
  ∃ driver, ride.driver = some driver := by
  -- `->`（含意）が2つ並んでいるので、まず仮定を1つずつ手元に取り出す。
  -- `intro hreach` は「`Reachable ride` という仮定に `hreach` という名前を付けて
  -- 仮定欄（コンテキスト）に置く」操作。これで証明すべきゴールは
  -- 「ride.status = .pickedUp -> ∃ driver, ride.driver = some driver」になる。
  intro hreach
  -- ここがこの証明の山場。
  -- いきなり「pickedUp なら driver がある」を帰納法で示そうとすると、
  -- pickUp 遷移（assigned -> pickedUp）の場面で詰まる。
  -- なぜなら pickUp の「遷移元」は pickedUp ではなく assigned なので、
  -- 「pickedUp なら…」という帰納法の仮定がそこでは使えないから。
  --
  -- そこで、ゴールをあえて「assigned か pickedUp なら driver がある」という
  -- 少し強い主張 h に置き換える。`suffices h : P by ...` は
  -- 「P さえ証明できれば元のゴールが従う。その『従う』部分を今ここで示す」という構文。
  -- ここでは元の仮定 hstatus(pickedUp) を「assigned ∨ pickedUp」の右側 `Or.inr` に
  -- 入れて h に渡すだけで元のゴールが出る。
  suffices h : ride.status = .assigned ∨ ride.status = .pickedUp →
      ∃ driver, ride.driver = some driver by
    intro hstatus
    exact h (Or.inr hstatus)
  -- これ以降のゴールは、上で宣言した強い主張 `h` の中身そのもの。
  --
  -- `induction hreach with` で「ride はどうやって到達可能になったのか」を
  -- Reachable のコンストラクタごとに場合分けする。
  -- Reachable は request / reject / assign / pickUp の4通りで作られるので、4ケースになる。
  induction hreach with
  | request =>
      -- ケース1: ride は初期状態 requestRide。状態は requested。
      -- 強い主張の仮定「assigned ∨ pickedUp」を取り出すと…
      intro hstatus
      -- requestRide を展開すると status は .requested。
      -- 「.requested = .assigned ∨ .requested = .pickedUp」はどちらも成り立たないので、
      -- simp が矛盾(False)を見つけてゴールを閉じてくれる。
      simp [requestRide] at hstatus
  | reject ride next _ hrej _ =>
      -- ケース2: 直前の ride を rejectRide して next になった。
      -- `hrej : rejectRide ride = some next` が手元にある。
      intro hstatus
      -- rejectRide の定義（中身の match）を hrej に展開する。
      unfold rejectRide at hrej
      -- `split` は hrej の中の `match ride.status with ...` を場合分けする。
      -- 「requested だったとき」と「それ以外」の2ケースに割れる。
      split at hrej
      · -- requested だったとき: hrej は `some {status := rejected,..} = some next`。
        -- `injection` は「some a = some b なら a = b」を取り出す（コンストラクタの単射性）。
        injection hrej with hnext
        -- hnext で next の中身が分かったので、ゴール中の next をその値に置き換える。
        subst hnext
        -- next の状態は rejected。assigned でも pickedUp でもないので hstatus は矛盾。
        simp at hstatus
      · -- それ以外のとき: rejectRide は none を返すので hrej は `none = some next`。
        -- これはあり得ない（none と some は別物）ので contradiction で閉じる。
        contradiction
  | assign ride driver next _ hass _ =>
      -- ケース3: 直前の ride に assignDriver driver して next になった。
      -- `hass : assignDriver ride driver = some next` が手元にある。
      -- 状態仮定は使わないので `_` で受け流す。
      intro _
      unfold assignDriver at hass
      split at hass
      · -- requested だったとき: next は driver := some driver で作られている。
        injection hass with hnext
        subst hnext
        -- ゴール `∃ d, next.driver = some d` を満たす d として driver を提示。
        -- `⟨driver, rfl⟩` は ∃ の中身（証拠 driver と、その等式 rfl）の組。
        -- next.driver はまさに `some driver` なので等式は rfl（自明な反射律）で済む。
        exact ⟨driver, rfl⟩
      · contradiction
  | pickUp ride next _ hpick ih =>
      -- ケース4: 直前の ride を pickUp して next になった。
      -- `hpick : pickUp ride = some next`、
      -- `ih` は帰納法の仮定 = 「直前の ride について、強い主張が成り立つ」。
      intro _
      unfold pickUp at hpick
      split at hpick
      · -- pickUp が成功するのは遷移元 ride が assigned のときだけ。
        -- split が作った「ride.status = .assigned」という仮定に名前を付ける。
        -- (split は名前を自動で付けるので、`rename_i` で手前から名付け直す。)
        rename_i hassigned
        injection hpick with hnext
        subst hnext
        -- next.driver は ride.driver をそのまま引き継ぐ。
        -- ride は assigned なので、帰納法の仮定 ih に「左側(assigned)」を渡せば
        -- 「ride に driver がある」が得られる。あとは simp が next と ride の
        -- driver が同じことを使ってゴールに合わせてくれる(`simpa`)。
        simpa using ih (Or.inl hassigned)
      · contradiction