JPYCv2 形式検証

外観

JPYC.bind_eq_ok ​

名称・種別 ​

  • 名称: JPYC.bind_eq_ok
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:40-46
  • 概要: bind の成功は前段の成功と後続の成功に分解できる、という補題。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ {α β : Type} {x : Except JPYC.Error α} {f : α → Except JPYC.Error β} {b : β}, Eq (Except.instMonad.bind x f) (Except.ok b) → Exists fun a => And (Eq x (Except.ok a)) (Eq (f a) (Except.ok b))

束縛 x >>= f が Except.ok b で成功するなら、最初の計算 x も何らかの a で成功し（x = .ok a）、続く f a も .ok b で成功する、という分解補題です。

和訳 docstring ​

束縛が成功するのは、最初の計算が成功し、続く計算も成功するときに限る。do ブロックを（ゴールを書き換えずに）分解できる。

解説 ​

何を述べているか。 「合成が成功した」という事実から、「各段が成功した」という事実を取り出します。x >>= f = .ok b なら ∃ a, x = .ok a ∧ f a = .ok b。

直感。 ok_bind / error_bind の逆向きの使い方です。x で場合分けし、error だったら矛盾（成功と仮定したのに）、ok a だったら欲しい結論が出ます。

なぜ安全性に効くか。 証明の主力です。transferFrom_eq_ok などが「成功 ⇒ 各ステップ（許可額・残高）が成功」と段階的に分解するのに繰り返し使います。do ブロックを書き換えずに「中身」を取り出せるのが利点です。

図解 ​

Lean ソースコード ​

lean
/-- A bind succeeds only if its first action succeeds and the continuation then
succeeds. Lets a `do` block be split without rewriting the goal. -/
theorem bind_eq_ok {α β : Type} {x : Except Error α} {f : α → Except Error β} {b : β}
    (h : (x >>= f) = .ok b) : ∃ a, x = .ok a ∧ f a = .ok b := by
  cases x with
  | error e => rw [error_bind] at h; exact absurd h (by simp)
  | ok a => rw [ok_bind] at h; exact ⟨a, rfl, h⟩

依存 ​