def le_fit

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64bits.bend:148

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/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

148# 2^k <= n exactly when n does not fit k bits
149def le_fit(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +n: Nat) -> {Nat.is_le(C.shift(k, one), n) == Bool.not(C.fits(k, n)) : Bool}:
150  +e2a = Equal.trans(Bool, Nat.is_lt(n, C.shift(k, 1n)), Nat.is_lt(n, C.pow2(k)), C.fits(k, n), Equal.cong(Nat, Bool, z => Nat.is_lt(n, z), C.shift(k, 1n), C.pow2(k), WW.shift_one(k)), Equal.sym(Bool, C.fits(k, n), Nat.is_lt(n, C.pow2(k)), WW.fits_lt(k, n)))
151  +e2 = L.subst(Nat, o => {Nat.is_lt(n, C.shift(k, o)) == C.fits(k, n) : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), e2a)
152  Equal.trans(Bool, Nat.is_le(C.shift(k, one), n), Bool.not(Nat.is_lt(n, C.shift(k, one))), Bool.not(C.fits(k, n)), le_nlt(C.shift(k, one), n), Equal.cong(Bool, Bool, z => Bool.not(z), Nat.is_lt(n, C.shift(k, one)), C.fits(k, n), e2))