def shq

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

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/math/natural/misc.bend as MS
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

62# N 2^t = (Q 2^t) B + r 2^t for N = Q B + r
63def shq(+N0: Nat, +bp: Nat, +t: Nat) -> {C.shift(t, N0) == Nat.add(Nat.mul(C.shift(t, Nat.div(N0, 1n+bp)), 1n+bp), C.shift(t, Nat.mod(N0, 1n+bp))) : Nat}:
64  +B = Nat.add(1n, bp)
65  +Q = Nat.div(N0, B)
66  +r = Nat.mod(N0, B)
67  +e1 = Equal.cong(Nat, Nat, u => C.shift(t, u), N0, Nat.add(Nat.mul(Q, B), r), MS.divmod_eq(N0, bp))
68  +e2 = WW.shift_add(t, Nat.mul(Q, B), r)
69  +e3 = Equal.cong(Nat, Nat, u => Nat.add(u, C.shift(t, r)), C.shift(t, Nat.mul(Q, B)), Nat.mul(C.shift(t, Q), B), Equal.sym(Nat, Nat.mul(C.shift(t, Q), B), C.shift(t, Nat.mul(Q, B)), WW.shift_mul_l(t, Q, B)))
70  Equal.trans(Nat, C.shift(t, N0), C.shift(t, Nat.add(Nat.mul(Q, B), r)), Nat.add(Nat.mul(C.shift(t, Q), B), C.shift(t, r)), e1, Equal.trans(Nat, C.shift(t, Nat.add(Nat.mul(Q, B), r)), Nat.add(C.shift(t, Nat.mul(Q, B)), C.shift(t, r)), Nat.add(Nat.mul(C.shift(t, Q), B), C.shift(t, r)), e2, e3))