def bl_le_n

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/f64bl.bend:46

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/bits.bend as BT
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW

46def bl_le_n(+K: Nat, +n: Nat, +hn: {C.fits(K, n) == True{} : Bool}, +hp: {Nat.is_le(C.pow2(1n+K), C.pow2(M.bit_length(n))) == True{} : Bool}) -> {False{} == True{} : Bool}:
47  match n:
48    case 0n:
49      +h0 = BT.bit_length_zero()
50      +hp2 = L.subst(Nat, z => {Nat.is_le(C.pow2(1n+K), C.pow2(z)) == True{} : Bool}, M.bit_length(0n), 0n, h0, hp)
51      Equal.trans(Bool, False{}, Nat.is_le(C.pow2(1n+K), 1n), True{}, Equal.sym(Bool, Nat.is_le(C.pow2(1n+K), 1n), False{}, N.lt_not_le(1n, C.pow2(1n+K), N.le_lt_trans(1n, C.pow2(K), C.pow2(1n+K), N.pow2_pos(K), N.pow2_lt_succ(K)))), hp2)
52    case 1n+ +np:
53      +hd = N.double_lt(1n+np, C.pow2(K), WW.lt_of_fits(K, 1n+np, hn))
54      +P = C.pow2(1n+K)
55      Equal.trans(Bool, False{}, Nat.is_lt(P, P), True{}, Equal.sym(Bool, Nat.is_lt(P, P), False{}, N.lt_irrefl(P)), N.le_lt_trans(P, Nat.double(1n+np), P, N.le_trans(P, C.pow2(M.bit_length(1n+np)), Nat.double(1n+np), hp, BT.bit_length_le(np)), hd))