def rne_shift

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

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/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/f64round.bend as FR

46# rounding m * 2^k by j + k bits is rounding m by j bits
47def rne_shift(+k: Nat, +m: Nat, +j: Nat) -> {SF.rne(C.shift(k, m), Nat.add(j, k)) == SF.rne(m, j) : Nat}:
48  match j:
49    case 0n:
50      rne_exact(k, m)
51    case 1n+ +i:
52      +a = Nat.add(1n+i, k)
53      +ea = NA.add_comm(1n+i, k)
54      +hq = Equal.trans(Nat, C.high(a, C.shift(k, m)), C.high(Nat.add(k, 1n+i), C.shift(k, m)), C.high(1n+i, m), Equal.cong(Nat, Nat, z => C.high(z, C.shift(k, m)), a, Nat.add(k, 1n+i), ea), Equal.trans(Nat, C.high(Nat.add(k, 1n+i), C.shift(k, m)), C.high(1n+i, C.high(k, C.shift(k, m))), C.high(1n+i, m), WW.high_comp(1n+i, k, C.shift(k, m)), Equal.cong(Nat, Nat, z => C.high(1n+i, z), C.high(k, C.shift(k, m)), m, WW.high_u(k, 0n, m, FR.fz(k)))))
55      +hl = Equal.trans(Nat, C.low(a, C.shift(k, m)), C.low(Nat.add(k, 1n+i), C.shift(k, m)), C.shift(k, C.low(1n+i, m)), Equal.cong(Nat, Nat, z => C.low(z, C.shift(k, m)), a, Nat.add(k, 1n+i), ea), WW.low_shift(k, 1n+i, m))
56      +hh = Equal.trans(Nat, C.shift(Nat.add(i, k), 1n), C.shift(Nat.add(k, i), 1n), C.shift(k, C.shift(i, 1n)), Equal.cong(Nat, Nat, z => C.shift(z, 1n), Nat.add(i, k), Nat.add(k, i), NA.add_comm(i, k)), WW.shift_comp(k, i, 1n))
57      +hc = Equal.trans(Cmp, Nat.cmp(C.low(a, C.shift(k, m)), C.shift(Nat.add(i, k), 1n)), Nat.cmp(C.shift(k, C.low(1n+i, m)), C.shift(Nat.add(i, k), 1n)), Nat.cmp(C.low(1n+i, m), C.shift(i, 1n)), Equal.cong(Nat, Cmp, z => Nat.cmp(z, C.shift(Nat.add(i, k), 1n)), C.low(a, C.shift(k, m)), C.shift(k, C.low(1n+i, m)), hl), Equal.trans(Cmp, Nat.cmp(C.shift(k, C.low(1n+i, m)), C.shift(Nat.add(i, k), 1n)), Nat.cmp(C.shift(k, C.low(1n+i, m)), C.shift(k, C.shift(i, 1n))), Nat.cmp(C.low(1n+i, m), C.shift(i, 1n)), Equal.cong(Nat, Cmp, z => Nat.cmp(C.shift(k, C.low(1n+i, m)), z), C.shift(Nat.add(i, k), 1n), C.shift(k, C.shift(i, 1n)), hh), NC.cmp_shift(k, C.low(1n+i, m), C.shift(i, 1n))))
58      +l1 = FR.rne_cmp(C.high(a, C.shift(k, m)), C.low(a, C.shift(k, m)), C.shift(Nat.add(i, k), 1n))
59      +l2 = Equal.cong(Nat, Nat, z => FR.rne_c(z, Nat.cmp(C.low(a, C.shift(k, m)), C.shift(Nat.add(i, k), 1n))), C.high(a, C.shift(k, m)), C.high(1n+i, m), hq)
60      +l3 = Equal.cong(Cmp, Nat, t => FR.rne_c(C.high(1n+i, m), t), Nat.cmp(C.low(a, C.shift(k, m)), C.shift(Nat.add(i, k), 1n)), Nat.cmp(C.low(1n+i, m), C.shift(i, 1n)), hc)
61      +r1 = FR.rne_cmp(C.high(1n+i, m), C.low(1n+i, m), C.shift(i, 1n))
62      Equal.trans(Nat, SF.rne_up(C.high(a, C.shift(k, m)), C.low(a, C.shift(k, m)), C.shift(Nat.add(i, k), 1n)), FR.rne_c(C.high(1n+i, m), Nat.cmp(C.low(1n+i, m), C.shift(i, 1n))), SF.rne_up(C.high(1n+i, m), C.low(1n+i, m), C.shift(i, 1n)), Equal.trans(Nat, SF.rne_up(C.high(a, C.shift(k, m)), C.low(a, C.shift(k, m)), C.shift(Nat.add(i, k), 1n)), FR.rne_c(C.high(a, C.shift(k, m)), Nat.cmp(C.low(a, C.shift(k, m)), C.shift(Nat.add(i, k), 1n))), FR.rne_c(C.high(1n+i, m), Nat.cmp(C.low(1n+i, m), C.shift(i, 1n))), l1, Equal.trans(Nat, FR.rne_c(C.high(a, C.shift(k, m)), Nat.cmp(C.low(a, C.shift(k, m)), C.shift(Nat.add(i, k), 1n))), FR.rne_c(C.high(1n+i, m), Nat.cmp(C.low(a, C.shift(k, m)), C.shift(Nat.add(i, k), 1n))), FR.rne_c(C.high(1n+i, m), Nat.cmp(C.low(1n+i, m), C.shift(i, 1n))), l2, l3)), Equal.sym(Nat, SF.rne_up(C.high(1n+i, m), C.low(1n+i, m), C.shift(i, 1n)), FR.rne_c(C.high(1n+i, m), Nat.cmp(C.low(1n+i, m), C.shift(i, 1n))), r1))