JPYCv2 形式検証

外観

JPYC.ok_bind ​

名称・種別 ​

  • 名称: JPYC.ok_bind
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:28-31
  • 概要: Except.ok の bind は値を後続へ渡すだけ、という（do ブロック書き換え用の）補題。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ {α β : Type} (a : α) (f : α → Except JPYC.Error β), Eq (Except.instMonad.bind (Except.ok a) f) (f a)

Except.ok a >>= f は f a に等しい、という定義的な等式です。

和訳 docstring ​

Except.ok は値を次へ渡して束縛する（定義的。do ブロック内の書き換え用に命名）。

解説 ​

何を述べているか。 成功値 Except.ok a に続けて f を適用すると、その値 a を f に渡した f a になります。

直感。 「成功したら、その結果を次へ渡す」というモナド束縛のもっとも基本的な振る舞いです。Lean では定義そのものから従う（rfl）ので、証明は一行です。

なぜ安全性に効くか。 do ブロックを 1 ステップずつ簡約するための土台補題です。名前を付けておくことで、証明中の rw [ok_bind] で「成功して次へ」を明示的に進められます。

図解 ​

Lean ソースコード ​

lean
/-- `Except.ok` binds by feeding its value onwards (definitional; named for
rewriting inside `do` blocks). -/
theorem ok_bind {α β : Type} (a : α) (f : α → Except Error β) :
    (Except.ok a >>= f) = f a := rfl

依存 ​