def rne_exact

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

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

270def rne_exact(+k: Nat, +m: Nat) -> {SF.rne(C.shift(k, m), k) == m : Nat}:
271  match k:
272    case 0n:
273      {==}
274    case 1n+ +i:
275      +S = C.shift(1n+i, m)
276      +h = C.shift(i, 1n)
277      +eq = WW.high_u(1n+i, 0n, m, fz(1n+i))
278      +el = WW.low_u(1n+i, 0n, m, fz(1n+i))
279      +e1 = Equal.cong(Nat, Nat, z => SF.rne_up(z, C.low(1n+i, S), h), C.high(1n+i, S), m, eq)
280      +e2 = Equal.cong(Nat, Nat, z => SF.rne_up(m, z, h), C.low(1n+i, S), 0n, el)
281      +hz = N.is_eq_sym_false(h, 0n, Equal.trans(Bool, Nat.is_eq(h, 0n), Nat.is_eq(1n, 0n), False{}, WW.shift_eq0(i, 1n), {==}))
282      +e3 = Equal.cong(Bool, Nat, t => Nat.add(m, SF.b2n(Bool.or(t, Bool.and(Nat.is_eq(0n, h), Nat.is_eq(Nat.mod(m, 2n), 1n))))), Nat.is_lt(h, 0n), False{}, lt0f(h))
283      +e4 = Equal.cong(Bool, Nat, t => Nat.add(m, SF.b2n(Bool.or(False{}, Bool.and(t, Nat.is_eq(Nat.mod(m, 2n), 1n))))), Nat.is_eq(0n, h), False{}, hz)
284      +e5 = N.add_zero(m)
285      Equal.trans(Nat, SF.rne_up(C.high(1n+i, S), C.low(1n+i, S), h), SF.rne_up(m, C.low(1n+i, S), h), m, e1, Equal.trans(Nat, SF.rne_up(m, C.low(1n+i, S), h), SF.rne_up(m, 0n, h), m, e2, Equal.trans(Nat, SF.rne_up(m, 0n, h), Nat.add(m, SF.b2n(Bool.or(False{}, Bool.and(Nat.is_eq(0n, h), Nat.is_eq(Nat.mod(m, 2n), 1n))))), m, e3, Equal.trans(Nat, Nat.add(m, SF.b2n(Bool.or(False{}, Bool.and(Nat.is_eq(0n, h), Nat.is_eq(Nat.mod(m, 2n), 1n))))), Nat.add(m, 0n), m, e4, e5))))