def rmfix_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:578

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/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA

578# rm_fix on words is the spec's rnear on their values
579def rmfix_v(+s: Bool, +u: Nat, +hu: {Nat.is_le(63n, u) == True{} : Bool}, +b: WU.U64, +r: WU.U64, +q: WU.U64, +Bv: Nat, +Rv: Nat, +Qv: Nat, +eb: {SW.value(b) == Bv : Nat}, +er: {SW.value(r) == Rv : Nat}, +hq: {Nat.mod(SW.value(q), 2n) == Nat.mod(Qv, 2n) : Nat}, +hRB: {Nat.is_le(Rv, Bv) == True{} : Bool}, +hf: {C.fits(53n, Rv) == True{} : Bool}) -> {F.rm_fix(s, u, b, r, q) == SF.rnear(s, Rv, Bv, Qv, u) : F.F64}:
580  +R2 = Nat.add(Rv, Rv)
581  +ea = addrr(r, Rv, er, hf)
582  +f1 = Equal.trans(Bool, X.lt(b, X.add(r, r)), Nat.is_lt(SW.value(b), SW.value(X.add(r, r))), Nat.is_lt(Bv, R2), WA.lt_value(b, X.add(r, r)), Equal.trans(Bool, Nat.is_lt(SW.value(b), SW.value(X.add(r, r))), Nat.is_lt(Bv, SW.value(X.add(r, r))), Nat.is_lt(Bv, R2), Equal.cong(Nat, Bool, t => Nat.is_lt(t, SW.value(X.add(r, r))), SW.value(b), Bv, eb), Equal.cong(Nat, Bool, t => Nat.is_lt(Bv, t), SW.value(X.add(r, r)), R2, ea)))
583  +f2 = Equal.trans(Bool, X.eq(X.add(r, r), b), Nat.is_eq(SW.value(X.add(r, r)), SW.value(b)), Nat.is_eq(R2, Bv), WA.eq_value(X.add(r, r), b), Equal.trans(Bool, Nat.is_eq(SW.value(X.add(r, r)), SW.value(b)), Nat.is_eq(R2, SW.value(b)), Nat.is_eq(R2, Bv), Equal.cong(Nat, Bool, t => Nat.is_eq(t, SW.value(b)), SW.value(X.add(r, r)), R2, addrr(r, Rv, er, hf)), Equal.cong(Nat, Bool, t => Nat.is_eq(R2, t), SW.value(b), Bv, eb)))
584  +f3 = Equal.trans(Bool, X.odd(q), Nat.is_eq(Nat.mod(SW.value(q), 2n), 1n), Nat.is_eq(Nat.mod(Qv, 2n), 1n), WA.odd_value(q), Equal.cong(Nat, Bool, t => Nat.is_eq(t, 1n), Nat.mod(SW.value(q), 2n), Nat.mod(Qv, 2n), hq))
585  +g1 = Equal.cong(Bool, F.F64, t => F.rm_pick(s, u, b, r, Bool.or(t, Bool.and(X.eq(X.add(r, r), b), X.odd(q)))), X.lt(b, X.add(r, r)), Nat.is_lt(Bv, R2), f1)
586  +g2 = Equal.cong(Bool, F.F64, t => F.rm_pick(s, u, b, r, Bool.or(Nat.is_lt(Bv, R2), Bool.and(t, X.odd(q)))), X.eq(X.add(r, r), b), Nat.is_eq(R2, Bv), f2)
587  +g3 = Equal.cong(Bool, F.F64, t => F.rm_pick(s, u, b, r, Bool.or(Nat.is_lt(Bv, R2), Bool.and(Nat.is_eq(R2, Bv), t))), X.odd(q), Nat.is_eq(Nat.mod(Qv, 2n), 1n), f3)
588  +a1 = F.rm_pick(s, u, b, r, Bool.or(Nat.is_lt(Bv, R2), Bool.and(X.eq(X.add(r, r), b), X.odd(q))))
589  +a2 = F.rm_pick(s, u, b, r, Bool.or(Nat.is_lt(Bv, R2), Bool.and(Nat.is_eq(R2, Bv), X.odd(q))))
590  +a3 = F.rm_pick(s, u, b, r, SF.rflip(Rv, Bv, Qv))
591  Equal.trans(F.F64, F.rm_fix(s, u, b, r, q), a1, SF.rnear(s, Rv, Bv, Qv, u), g1, Equal.trans(F.F64, a1, a2, SF.rnear(s, Rv, Bv, Qv, u), g2, Equal.trans(F.F64, a2, a3, SF.rnear(s, Rv, Bv, Qv, u), g3, rmp_c(s, u, hu, b, r, Bv, Rv, eb, er, hRB, SF.rflip(Rv, Bv, Qv)))))