def hpick_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:753

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/math/typed/width.bend as WW

753# the high part of a normal q <= 2^53 is the spec's 1 or 2
754def hpick_c(+one: Nat, +h1: {one == 1n : Nat}, +q: Nat, +hq: {Nat.is_le(q, C.shift(53n, one)) == True{} : Bool}, +h52: {C.fits(52n, q) == False{} : Bool}, +f: Bool, +hf: {C.fits(53n, q) == f : Bool}) -> {C.high(52n, q) == SF.pick(Nat, f, 1n, 2n) : Nat}:
755  match f:
756    case True{}:
757      Equal.trans(Nat, C.high(52n, q), 1n, SF.pick(Nat, True{}, 1n, 2n), hi_one(C.high(52n, q), Equal.trans(Bool, Nat.is_eq(C.half(C.high(52n, q)), 0n), C.fits(53n, q), True{}, Equal.sym(Bool, C.fits(53n, q), Nat.is_eq(C.half(C.high(52n, q)), 0n), f53h(q)), hf), h52), Equal.sym(Nat, SF.pick(Nat, True{}, 1n, 2n), 1n, pk_t(Nat, 1n, 2n)))
758    case False{}:
759      +eq = top_q(one, h1, q, hq, hf)
760      +e1 = Equal.trans(Nat, C.high(52n, q), C.high(52n, C.shift(52n, Nat.double(one))), Nat.double(one), Equal.cong(Nat, Nat, z => C.high(52n, z), q, C.shift(52n, Nat.double(one)), eq), WW.high_u(52n, 0n, Nat.double(one), fz(52n)))
761      Equal.trans(Nat, C.high(52n, q), 2n, SF.pick(Nat, False{}, 1n, 2n), Equal.trans(Nat, C.high(52n, q), Nat.double(one), 2n, e1, Equal.cong(Nat, Nat, z => Nat.double(z), one, 1n, h1)), Equal.sym(Nat, SF.pick(Nat, False{}, 1n, 2n), 2n, pk_f(Nat, 1n, 2n)))