def div_uniq

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64dm.bend:142

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW

142# r b <= x < (r + 1) b: r == x / b and x - r b == x mod b
143def div_uniq(+x: Nat, +r: Nat, +bp: Nat, +h1: {Nat.is_le(Nat.mul(r, 1n+bp), x) == True{} : Bool}, +h2: {Nat.is_lt(x, Nat.mul(1n+r, 1n+bp)) == True{} : Bool}) -> {Nat.div(x, 1n+bp) == r : Nat} & {Nat.mod(x, 1n+bp) == Nat.sub(x, Nat.mul(r, 1n+bp)) : Nat}:
144  +t = Nat.sub(x, Nat.mul(r, 1n+bp))
145  +ex = N.sub_add(x, Nat.mul(r, 1n+bp), h1)
146  +h3 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(1n+bp, Nat.mul(r, 1n+bp))) == True{} : Bool}, x, Nat.add(Nat.mul(r, 1n+bp), t), Equal.sym(Nat, Nat.add(Nat.mul(r, 1n+bp), t), x, ex), h2)
147  +h4 = L.subst(Nat, z => {Nat.is_lt(Nat.add(Nat.mul(r, 1n+bp), t), z) == True{} : Bool}, Nat.add(1n+bp, Nat.mul(r, 1n+bp)), Nat.add(Nat.mul(r, 1n+bp), 1n+bp), N.add_comm(1n+bp, Nat.mul(r, 1n+bp)), h3)
148  +ht = Equal.trans(Bool, Nat.is_lt(t, 1n+bp), Nat.is_lt(Nat.add(Nat.mul(r, 1n+bp), t), Nat.add(Nat.mul(r, 1n+bp), 1n+bp)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(Nat.mul(r, 1n+bp), t), Nat.add(Nat.mul(r, 1n+bp), 1n+bp)), Nat.is_lt(t, 1n+bp), WW.lt_cancel_l(Nat.mul(r, 1n+bp), t, 1n+bp)), h4)
149  (Equal.trans(Nat, Nat.div(x, 1n+bp), Nat.div(Nat.add(Nat.mul(r, 1n+bp), t), 1n+bp), r, Equal.cong(Nat, Nat, z => Nat.div(z, 1n+bp), x, Nat.add(Nat.mul(r, 1n+bp), t), Equal.sym(Nat, Nat.add(Nat.mul(r, 1n+bp), t), x, ex)), NR.div_of(r, bp, t, ht)), Equal.trans(Nat, Nat.mod(x, 1n+bp), Nat.mod(Nat.add(Nat.mul(r, 1n+bp), t), 1n+bp), t, Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), x, Nat.add(Nat.mul(r, 1n+bp), t), Equal.sym(Nat, Nat.add(Nat.mul(r, 1n+bp), t), x, ex)), NR.mod_of(r, bp, t, ht)))