def rp_c

bend-collections-laws-math@1.0.0.0 · proofs/math/random/fround.bend:81

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
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32half.bend as UH

81def rp_c(+q0: Nat, +r0: Nat, +hr: {C.fits(10n, r0) == True{} : Bool}, +c: Cmp, +hc: {Nat.cmp(r0, 512n) == c : Cmp}) -> {SF.pick(Nat, Nat.is_eq(r0, 512n), Nat.sub(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), Nat.mod(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), 2n)), Nat.add(q0, C.high(10n, Nat.add(r0, 512n)))) == SF.rne_up(q0, r0, 512n) : Nat}:
82  match c:
83    case LT{}:
84      +hlt = NC.lt_of_cmp(r0, 512n, hc)
85      +he = Equal.cong(Cmp, Bool, t => Cmp.is_eq(t), Nat.cmp(r0, 512n), LT{}, hc)
86      +hg = Equal.cong(Cmp, Bool, t => Cmp.is_lt(t), Nat.cmp(512n, r0), GT{}, Equal.trans(Cmp, Nat.cmp(512n, r0), SF.flip(Nat.cmp(r0, 512n)), GT{}, Equal.sym(Cmp, SF.flip(Nat.cmp(r0, 512n)), Nat.cmp(512n, r0), NC.cmp_flip(r0, 512n)), Equal.cong(Cmp, Cmp, t => SF.flip(t), Nat.cmp(r0, 512n), LT{}, hc)))
87      +f = WW.fits_of_lt(10n, Nat.add(r0, 512n), N.lt_add_r2(r0, 512n, 512n, hlt))
88      +h0 = N.eq_from_is_eq(C.high(10n, Nat.add(r0, 512n)), 0n, f)
89      +l1 = Equal.cong(Bool, Nat, t => SF.pick(Nat, t, Nat.sub(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), Nat.mod(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), 2n)), Nat.add(q0, C.high(10n, Nat.add(r0, 512n)))), Nat.is_eq(r0, 512n), False{}, he)
90      +l2 = Equal.cong(Nat, Nat, z => Nat.add(q0, z), C.high(10n, Nat.add(r0, 512n)), 0n, h0)
91      +r1 = Equal.cong(Bool, Nat, t => Nat.add(q0, SF.b2n(Bool.or(t, Bool.and(Nat.is_eq(r0, 512n), Nat.is_eq(Nat.mod(q0, 2n), 1n))))), Nat.is_lt(512n, r0), False{}, hg)
92      +r2 = Equal.cong(Bool, Nat, t => Nat.add(q0, SF.b2n(Bool.or(False{}, Bool.and(t, Nat.is_eq(Nat.mod(q0, 2n), 1n))))), Nat.is_eq(r0, 512n), False{}, he)
93      Equal.trans(Nat, SF.pick(Nat, Nat.is_eq(r0, 512n), Nat.sub(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), Nat.mod(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), 2n)), Nat.add(q0, C.high(10n, Nat.add(r0, 512n)))), Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), SF.rne_up(q0, r0, 512n), l1, Equal.trans(Nat, Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), Nat.add(q0, 0n), SF.rne_up(q0, r0, 512n), l2, Equal.sym(Nat, SF.rne_up(q0, r0, 512n), Nat.add(q0, 0n), Equal.trans(Nat, SF.rne_up(q0, r0, 512n), Nat.add(q0, SF.b2n(Bool.or(False{}, Bool.and(Nat.is_eq(r0, 512n), Nat.is_eq(Nat.mod(q0, 2n), 1n))))), Nat.add(q0, 0n), r1, r2))))
94    case GT{}:
95      +hgt = NC.lt_of_gt(r0, 512n, hc)
96      +he = Equal.cong(Cmp, Bool, t => Cmp.is_eq(t), Nat.cmp(r0, 512n), GT{}, hc)
97      +d = Nat.sub(r0, 512n)
98      +ed = N.sub_add(r0, 512n, N.lt_le(512n, r0, hgt))
99      +ex = Equal.trans(Nat, Nat.add(r0, 512n), Nat.add(Nat.add(512n, d), 512n), Nat.add(d, C.shift(10n, 1n)), Equal.cong(Nat, Nat, z => Nat.add(z, 512n), r0, Nat.add(512n, d), Equal.sym(Nat, Nat.add(512n, d), r0, ed)), Equal.trans(Nat, Nat.add(Nat.add(512n, d), 512n), Nat.add(512n, Nat.add(d, 512n)), Nat.add(d, C.shift(10n, 1n)), NA.add_assoc(512n, d, 512n), Equal.trans(Nat, Nat.add(512n, Nat.add(d, 512n)), Nat.add(1024n, d), Nat.add(d, C.shift(10n, 1n)), Equal.cong(Nat, Nat, z => Nat.add(512n, z), Nat.add(d, 512n), Nat.add(512n, d), NA.add_comm(d, 512n)), NA.add_comm(1024n, d))))
100      +hd = SH.fits_lek(10n, d, r0, UH.sub_le(r0, 512n), hr)
101      +h1 = Equal.trans(Nat, C.high(10n, Nat.add(r0, 512n)), C.high(10n, Nat.add(d, C.shift(10n, 1n))), 1n, Equal.cong(Nat, Nat, z => C.high(10n, z), Nat.add(r0, 512n), Nat.add(d, C.shift(10n, 1n)), ex), WW.high_u(10n, d, 1n, hd))
102      +l1 = Equal.cong(Bool, Nat, t => SF.pick(Nat, t, Nat.sub(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), Nat.mod(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), 2n)), Nat.add(q0, C.high(10n, Nat.add(r0, 512n)))), Nat.is_eq(r0, 512n), False{}, he)
103      +l2 = Equal.cong(Nat, Nat, z => Nat.add(q0, z), C.high(10n, Nat.add(r0, 512n)), 1n, h1)
104      +r1 = Equal.cong(Bool, Nat, t => Nat.add(q0, SF.b2n(Bool.or(t, Bool.and(Nat.is_eq(r0, 512n), Nat.is_eq(Nat.mod(q0, 2n), 1n))))), Nat.is_lt(512n, r0), True{}, hgt)
105      Equal.trans(Nat, SF.pick(Nat, Nat.is_eq(r0, 512n), Nat.sub(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), Nat.mod(Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), 2n)), Nat.add(q0, C.high(10n, Nat.add(r0, 512n)))), Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), SF.rne_up(q0, r0, 512n), l1, Equal.trans(Nat, Nat.add(q0, C.high(10n, Nat.add(r0, 512n))), Nat.add(q0, 1n), SF.rne_up(q0, r0, 512n), l2, Equal.sym(Nat, SF.rne_up(q0, r0, 512n), Nat.add(q0, 1n), r1)))
106    case EQ{}:
107      +er = NC.eq_of_cmp(r0, 512n, hc)
108      +b1 = subm(Nat.add(q0, 1n))
109      +b2 = Equal.trans(Nat, Nat.add(q0, SF.b2n(Nat.is_eq(Nat.mod(q0, 2n), 1n))), Nat.add(q0, SF.b2n(Nat.is_eq(C.bit(q0), 1n))), Nat.double(C.half(Nat.add(q0, 1n))), Equal.cong(Nat, Nat, z => Nat.add(q0, SF.b2n(Nat.is_eq(z, 1n))), Nat.mod(q0, 2n), C.bit(q0), Equal.sym(Nat, C.bit(q0), Nat.mod(q0, 2n), WW.bit_mod(q0))), parq(q0))
110      +base = Equal.trans(Nat, Nat.sub(Nat.add(q0, 1n), Nat.mod(Nat.add(q0, 1n), 2n)), Nat.double(C.half(Nat.add(q0, 1n))), Nat.add(q0, SF.b2n(Nat.is_eq(Nat.mod(q0, 2n), 1n))), b1, Equal.sym(Nat, Nat.add(q0, SF.b2n(Nat.is_eq(Nat.mod(q0, 2n), 1n))), Nat.double(C.half(Nat.add(q0, 1n))), b2))
111      L.subst(Nat, z => {SF.pick(Nat, Nat.is_eq(z, 512n), Nat.sub(Nat.add(q0, C.high(10n, Nat.add(z, 512n))), Nat.mod(Nat.add(q0, C.high(10n, Nat.add(z, 512n))), 2n)), Nat.add(q0, C.high(10n, Nat.add(z, 512n)))) == SF.rne_up(q0, z, 512n) : Nat}, 512n, r0, Equal.sym(Nat, r0, 512n, er), base)