def gub

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64cmp.bend:36

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/spec/math/f64.bend as SF
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/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

36# G < 2^(1+E) * 2^52
37def gub(+one: Nat, +h1: {one == 1n : Nat}, +E: Nat, +b: Bool, +hb: {Nat.is_eq(E, 0n) == b : Bool}, +c: Nat, +hc: {c == SF.b2n(Bool.not(b)) : Nat}, +F: Nat, +hF: {C.fits(52n, F) == True{} : Bool}) -> {Nat.is_lt(C.shift(SF.pick(Nat, b, 1n, E), Nat.add(F, C.shift(52n, c))), C.shift(1n+E, C.shift(52n, one))) == True{} : Bool}:
38  match b:
39    case True{}:
40      +eE = N.eq_from_is_eq(E, 0n, hb)
41      +ef = Equal.trans(Nat, Nat.add(F, C.shift(52n, c)), Nat.add(F, 0n), F, Equal.cong(Nat, Nat, z => Nat.add(F, C.shift(52n, z)), c, 0n, hc), N.add_zero(F))
42      +h0 = WW.shift_lt(1n, F, C.shift(52n, one), WW.lt_one(52n, one, h1, F, hF))
43      +h2 = L.subst(Nat, z => {Nat.is_lt(C.shift(1n, z), C.shift(1n, C.shift(52n, one))) == True{} : Bool}, F, Nat.add(F, C.shift(52n, c)), Equal.sym(Nat, Nat.add(F, C.shift(52n, c)), F, ef), h0)
44      L.subst(Nat, z => {Nat.is_lt(C.shift(1n, Nat.add(F, C.shift(52n, c))), C.shift(1n+z, C.shift(52n, one))) == True{} : Bool}, 0n, E, Equal.sym(Nat, E, 0n, eE), h2)
45    case False{}:
46      +ec = Equal.trans(Nat, c, 1n, one, hc, Equal.sym(Nat, one, 1n, h1))
47      +es = Equal.cong(Nat, Nat, z => Nat.add(F, C.shift(52n, z)), c, one, ec)
48      +h0 = N.lt_add_r2(F, C.shift(52n, one), C.shift(52n, one), WW.lt_one(52n, one, h1, F, hF))
49      +h1b = L.subst(Nat, z => {Nat.is_lt(Nat.add(F, C.shift(52n, one)), z) == True{} : Bool}, Nat.add(C.shift(52n, one), C.shift(52n, one)), Nat.double(C.shift(52n, one)), Equal.sym(Nat, Nat.double(C.shift(52n, one)), Nat.add(C.shift(52n, one), C.shift(52n, one)), NA.double_self(C.shift(52n, one))), h0)
50      +h2 = WW.shift_lt(E, Nat.add(F, C.shift(52n, one)), Nat.double(C.shift(52n, one)), h1b)
51      +h3 = L.subst(Nat, z => {Nat.is_lt(C.shift(E, Nat.add(F, C.shift(52n, one))), z) == True{} : Bool}, C.shift(E, Nat.double(C.shift(52n, one))), Nat.double(C.shift(E, C.shift(52n, one))), WW.shift_dbl(E, C.shift(52n, one)), h2)
52      L.subst(Nat, z => {Nat.is_lt(C.shift(E, z), Nat.double(C.shift(E, C.shift(52n, one)))) == True{} : Bool}, Nat.add(F, C.shift(52n, one)), Nat.add(F, C.shift(52n, c)), Equal.sym(Nat, Nat.add(F, C.shift(52n, c)), Nat.add(F, C.shift(52n, one)), es), h3)