JPYC.req_ok

名称・種別

• 名称: JPYC.req_ok
• 種別: theorem
• モジュール: JpycFormalVerification.AccessControlTheorems
• ソース: JpycFormalVerification/AccessControlTheorems.lean:67-71
• 概要: req c e が .ok () になるなら条件 c が成立している、という補題。
• 仕様: 対象外

型シグネチャ

∀ {c : Prop} [inst : Decidable c] {e : JPYC.Error}, Eq (JPYC.req c e) (Except.ok Unit.unit) → c

req c e = .ok ()（require の成功）から、条件 c が成り立っていたことを取り出す補題です。

和訳 docstring

req c e = .ok ()（require が成功）は条件 c の成立を強制する。

解説

何を述べているか。 ガード req が成功した（Except.ok () を返した）という事実から、その条件 c が真であったことを結論します。証明は req を展開して場合分けするだけ（偽なら .error になり成功と矛盾）。

直感。 「関所を通れたのだから、通行条件は満たされていた」という当たり前の逆向き推論を、補題として名付けたものです。

なぜ安全性に効くか。 これ自体は安全性の主張ではなく 証明インフラ です。*_ok / *_guards 系の定理が「成功した呼び出しでは、各ガード条件が満たされていた」と段階的に取り出すのに使います。

図解

Lean ソースコード

/-- `req c e = .ok ()` forces the condition `c`. -/
theorem req_ok {c : Prop} [Decidable c] {e : Error} (h : req c e = .ok ()) : c := by
  unfold req at h; split at h
  · assumption
  · exact absurd h (by simp)

依存

• JPYC.Error
• JPYC.req