def iq_parts

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64divn.bend:117

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/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

117# SoftFloat's quotient: (a - b) * 2^64 = Q * b + r2 with r2 < b gives
118# a * 2^62 = T * b + e with T = 2^62 + floor(Q / 4) and e < b
119def iq_parts(+B: Nat, +R: Nat, +Q: Nat, +r2: Nat, +hQ: {Nat.add(Nat.mul(Q, B), r2) == C.shift(64n, R) : Nat}) -> {Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)) == C.shift(2n, C.shift(62n, R)) : Nat}:
120  +q1 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(z, B), r2), Q, Nat.add(C.low(2n, Q), C.shift(2n, C.high(2n, Q))), WW.low_high(2n, Q))
121  +q2 = Equal.cong(Nat, Nat, z => Nat.add(z, r2), Nat.mul(Nat.add(C.low(2n, Q), C.shift(2n, C.high(2n, Q))), B), Nat.add(Nat.mul(C.low(2n, Q), B), Nat.mul(C.shift(2n, C.high(2n, Q)), B)), NA.mul_add_right(C.low(2n, Q), C.shift(2n, C.high(2n, Q)), B))
122  +q3 = Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(C.low(2n, Q), B), z), r2), Nat.mul(C.shift(2n, C.high(2n, Q)), B), C.shift(2n, Nat.mul(C.high(2n, Q), B)), WW.shift_mul_l(2n, C.high(2n, Q), B))
123  +q4 = NA.add_assoc(Nat.mul(C.low(2n, Q), B), C.shift(2n, Nat.mul(C.high(2n, Q), B)), r2)
124  +q5 = NA.add_swap(Nat.mul(C.low(2n, Q), B), C.shift(2n, Nat.mul(C.high(2n, Q), B)), r2)
125  +q7 = Equal.trans(Nat, C.shift(64n, R), C.shift(Nat.add(2n, 62n), R), C.shift(2n, C.shift(62n, R)), {==}, WW.shift_comp(2n, 62n, R))
126  +x1 = Equal.trans(Nat, Nat.add(Nat.mul(Q, B), r2), Nat.add(Nat.mul(Nat.add(C.low(2n, Q), C.shift(2n, C.high(2n, Q))), B), r2), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), q1, Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(C.low(2n, Q), C.shift(2n, C.high(2n, Q))), B), r2), Nat.add(Nat.add(Nat.mul(C.low(2n, Q), B), Nat.mul(C.shift(2n, C.high(2n, Q)), B)), r2), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), q2, Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(C.low(2n, Q), B), Nat.mul(C.shift(2n, C.high(2n, Q)), B)), r2), Nat.add(Nat.add(Nat.mul(C.low(2n, Q), B), C.shift(2n, Nat.mul(C.high(2n, Q), B))), r2), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), q3, Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(C.low(2n, Q), B), C.shift(2n, Nat.mul(C.high(2n, Q), B))), r2), Nat.add(Nat.mul(C.low(2n, Q), B), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), r2)), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), q4, q5))))
127  Equal.trans(Nat, Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), Nat.add(Nat.mul(Q, B), r2), C.shift(2n, C.shift(62n, R)), Equal.sym(Nat, Nat.add(Nat.mul(Q, B), r2), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), x1), Equal.trans(Nat, Nat.add(Nat.mul(Q, B), r2), C.shift(64n, R), C.shift(2n, C.shift(62n, R)), hQ, q7))