JPYC.sub?_self

名称: JPYC.sub?_self
種別: theorem
モジュール: JpycFormalVerification.Word
ソース: JpycFormalVerification/Word.lean:80-80
概要: 同じ値どうしの sub? は必ず 0 を返す、という補題。
仕様: 対象外

名称・種別

lean

∀ (a : JPYC.U256), Eq (JPYC.sub? a a) (Except.ok 0)

「sub? a a = .ok 0」という定理です。同じ値どうしの引き算は、必ず 0 で成功します。

何を述べているか。 自分自身を引けば、必ず 0 を返して成功する、という事実です（a ≤ a は常に真だから）。

直感。 どんな値も、それ自身を引けば 0 です。@[simp] 補助定理です。

なぜ安全性に効くか。 自己送金（from == to）のような場面で現れる自明なケースを、証明の中で自動的に単純化します。

lean

@[simp] theorem sub?_self (a : U256) : sub? a a = .ok 0 := by simp [sub?]