def mod_shift

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/montnat.bend:50

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

50# (z mod m) 2^k == z 2^k (mod m)
51def mod_shift(+bp: Nat, +k: Nat, +z0: Nat) -> {Nat.mod(C.shift(k, Nat.mod(z0, 1n+bp)), 1n+bp) == Nat.mod(C.shift(k, z0), 1n+bp) : Nat}:
52  Equal.sym(Nat, Nat.mod(C.shift(k, z0), 1n+bp), Nat.mod(C.shift(k, Nat.mod(z0, 1n+bp)), 1n+bp), Equal.trans(Nat, Nat.mod(C.shift(k, z0), 1n+bp), Nat.mod(C.shift(k, Nat.add(Nat.mul(Nat.div(z0, 1n+bp), 1n+bp), Nat.mod(z0, 1n+bp))), 1n+bp), Nat.mod(C.shift(k, Nat.mod(z0, 1n+bp)), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(C.shift(k, z), 1n+bp), z0, Nat.add(Nat.mul(Nat.div(z0, 1n+bp), 1n+bp), Nat.mod(z0, 1n+bp)), NR.dm_eq(bp, z0)), Equal.trans(Nat, Nat.mod(C.shift(k, Nat.add(Nat.mul(Nat.div(z0, 1n+bp), 1n+bp), Nat.mod(z0, 1n+bp))), 1n+bp), Nat.mod(Nat.add(C.shift(k, Nat.mul(Nat.div(z0, 1n+bp), 1n+bp)), C.shift(k, Nat.mod(z0, 1n+bp))), 1n+bp), Nat.mod(C.shift(k, Nat.mod(z0, 1n+bp)), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), C.shift(k, Nat.add(Nat.mul(Nat.div(z0, 1n+bp), 1n+bp), Nat.mod(z0, 1n+bp))), Nat.add(C.shift(k, Nat.mul(Nat.div(z0, 1n+bp), 1n+bp)), C.shift(k, Nat.mod(z0, 1n+bp))), WW.shift_add(k, Nat.mul(Nat.div(z0, 1n+bp), 1n+bp), Nat.mod(z0, 1n+bp))), Equal.trans(Nat, Nat.mod(Nat.add(C.shift(k, Nat.mul(Nat.div(z0, 1n+bp), 1n+bp)), C.shift(k, Nat.mod(z0, 1n+bp))), 1n+bp), Nat.mod(Nat.add(Nat.mul(C.shift(k, Nat.div(z0, 1n+bp)), 1n+bp), C.shift(k, Nat.mod(z0, 1n+bp))), 1n+bp), Nat.mod(C.shift(k, Nat.mod(z0, 1n+bp)), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(Nat.add(z, C.shift(k, Nat.mod(z0, 1n+bp))), 1n+bp), C.shift(k, Nat.mul(Nat.div(z0, 1n+bp), 1n+bp)), Nat.mul(C.shift(k, Nat.div(z0, 1n+bp)), 1n+bp), Equal.sym(Nat, Nat.mul(C.shift(k, Nat.div(z0, 1n+bp)), 1n+bp), C.shift(k, Nat.mul(Nat.div(z0, 1n+bp), 1n+bp)), WW.shift_mul_l(k, Nat.div(z0, 1n+bp), 1n+bp))), NR.absorb(bp, C.shift(k, Nat.div(z0, 1n+bp)), C.shift(k, Nat.mod(z0, 1n+bp)))))))