JPYC.sub?_of_le

名称: JPYC.sub?_of_le
種別: theorem
モジュール: JpycFormalVerification.Word
ソース: JpycFormalVerification/Word.lean:65-66
概要: b ≤ a なら sub? は成功して通常の差を返す、という補題。
仕様: 対象

名称・種別

lean

∀ {a b : JPYC.U256}, instLENat.le (BitVec.toNat b) (BitVec.toNat a) → Eq (JPYC.sub? a b) (Except.ok (instHSub.hSub a b))

「b.toNat ≤ a.toNat（自然数として b ≤ a）ならば、sub? a b = .ok (a - b)」という定理です。

何を述べているか。 引ける前提のもとでは sub? は必ず成功して差を返す、という 導入補題 です。

直感。 引き算がマイナスにならない前提（b ≤ a）なら、sub? は成功の枝に入ります。

なぜ安全性に効くか。「残高が十分なら減算が成功する」ことを示す道具で、round-trip 補題 add?_sub?_cancel などの部品になります。

lean

theorem sub?_of_le {a b : U256} (h : b.toNat ≤ a.toNat) :
    sub? a b = .ok (a - b) := by simp [sub?, h]