JPYC.req_pos

名称・種別

• 名称: JPYC.req_pos
• 種別: theorem
• モジュール: JpycFormalVerification.SignaturesTheorems
• ソース: JpycFormalVerification/SignaturesTheorems.lean:42-44
• 概要: 条件が真の require は () で続行する、という補題。
• 仕様: 対象外

型シグネチャ

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

条件 c が成り立つなら、ガード req c e は Except.ok () で素通りする、という補題です。

和訳 docstring

passing require が () で続行することを示す（条件が真なら req c e = .ok ()）。

解説

何を述べているか。 c（条件が真）のとき req c e = .ok () です。req の真側（if_pos）に倒して得られます。

直感。 「通行条件を満たせば、関所は何もせず () を返して先へ進ませる」を補題にしたものです。

なぜ安全性に効くか。 req_neg と対になる 証明インフラ です。do ブロックを「ガードを通過した後の続き」へ簡約する前向き計算で使います。

図解

Lean ソースコード

/-- A passing `require` proceeds with `()`. -/
theorem req_pos {c : Prop} [Decidable c] {e : Error} (h : c) : req c e = .ok () := by
  unfold req; rw [if_pos h]; rfl

依存

• JPYC.Error
• JPYC.req