def fits_split

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32laws.bend:221

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as A
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AR

221# fits(k, lo + 2^k hi) exactly when hi == 0 (lo < 2^k)
222def fits_split(+k: Nat, +lo: Nat, +hi: Nat, +hl: {Nat.is_lt(lo, C.pow2(k)) == True{} : Bool}) -> {C.fits(k, Nat.add(lo, WD.sc(k, hi))) == Nat.is_eq(hi, 0n) : Bool}:
223  match hi:
224    case 0n:
225      %Equal.sym(Nat, WD.sc(k, 0n), 0n, A.sc_zero(k)) : {C.fits(k, Nat.add(lo, _)) == True{} : Bool}
226      %Equal.sym(Nat, Nat.add(lo, 0n), lo, N.add_zero(lo)) : {C.fits(k, _) == True{} : Bool}
227      %Equal.sym(Bool, C.fits(k, lo), Nat.is_lt(lo, C.pow2(k)), WW.fits_lt(k, lo)) : {_ == True{} : Bool}
228      hl
229    case 1n+ +h:
230      %Equal.sym(Bool, C.fits(k, Nat.add(lo, WD.sc(k, 1n+h))), Nat.is_lt(Nat.add(lo, WD.sc(k, 1n+h)), C.pow2(k)), WW.fits_lt(k, Nat.add(lo, WD.sc(k, 1n+h)))) : {_ == False{} : Bool}
231      +p1 = L.subst(Nat, z => {Nat.is_le(z, WD.sc(k, 1n+h)) == True{} : Bool}, WD.sc(k, 1n), C.pow2(k), Equal.sym(Nat, C.pow2(k), WD.sc(k, 1n), U.pow2_scale(k)), AR.sc_le(k, 1n, 1n+h, N.zero_le(h)))
232      +p2 = L.subst(Nat, z => {Nat.is_le(WD.sc(k, 1n+h), z) == True{} : Bool}, Nat.add(WD.sc(k, 1n+h), lo), Nat.add(lo, WD.sc(k, 1n+h)), N.add_comm(WD.sc(k, 1n+h), lo), N.le_add_right(WD.sc(k, 1n+h), lo))
233      N.le_not_lt(Nat.add(lo, WD.sc(k, 1n+h)), C.pow2(k), N.le_trans(C.pow2(k), WD.sc(k, 1n+h), Nat.add(lo, WD.sc(k, 1n+h)), p1, p2))