JPYC.req_neg

名称・種別

• 名称: JPYC.req_neg
• 種別: theorem
• モジュール: JpycFormalVerification.SignaturesTheorems
• ソース: JpycFormalVerification/SignaturesTheorems.lean:38-40
• 概要: 条件が偽の require はちょうど revert と一致する、という補題。
• 仕様: 対象外

型シグネチャ

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

条件 c が成り立たないなら、ガード req c e はちょうど Except.error e（revert）になる、という補題です。

和訳 docstring

failing require が revert に等しいことを示す（条件が偽なら req c e = .error e）。

解説

何を述べているか。 ¬ c（条件が偽）のとき req c e = .error e です。req は「c なら .ok ()、さもなくば .error e」という if なので、偽側（if_neg）に倒して得られます。

直感。 「通行条件を満たさなければ、関所はちょうどこのエラーで閉じる」を、機械が使える形にした補題です。

なぜ安全性に効くか。 これ自体は安全性の主張ではなく 証明インフラ です。各関数の revert 形定理（permit_paused・各 *_not_yet_valid など）が「ガードが破れたとき、ちょうどこのエラーで止まる」と述べるのに使います。

図解

Lean ソースコード

/-- A failing `require` is exactly the revert. -/
theorem req_neg {c : Prop} [Decidable c] {e : Error} (h : ¬ c) : req c e = .error e := by
  unfold req; rw [if_neg h]; rfl

依存

• JPYC.Error
• JPYC.req