def sub_wrap

bend-collections-laws-math@1.0.0.0 · proofs/lib/word.bend:71

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as A

71# If x + 2^n == d + b with d < 2^n, the machine difference x - b is d.
72def sub_wrap(+n: Nat, +one: Nat, +h1: {one == 1n : Nat}, +xw: Word(n), +bw: Word(n), +d: Nat, +e: {Nat.add(uw(n, xw), sc(n, one)) == Nat.add(d, uw(n, bw)) : Nat}, +hd: {Nat.is_lt(d, sc(n, one)) == True{} : Bool}) -> {uw(n, Word.sub(n, xw, bw)) == d : Nat}:
73  +us = uw(n, Word.sub(n, xw, bw))
74  +ux = uw(n, xw)
75  +ub = uw(n, bw)
76  +un = uw(n, Word.not(n, bw))
77  +c5 = A.cy(n, xw, Word.not(n, bw), True{})
78  +e5 = A.cons_sub(n, xw, bw)
79  +nv = A.not_value(n, bw)
80  +ew = L.subst(Nat, o => {Nat.add(ux, S.scale_binary(n, o)) == Nat.add(d, ub) : Nat}, one, 1n, h1, e)
81  # (1 + (ux + un)) + ub == ux + (1 + (un + ub)) == ux + 2^n
82  +mid = Equal.trans(Nat, Nat.add(Nat.add(1n, Nat.add(ux, un)), ub), 1n+Nat.add(ux, Nat.add(un, ub)), Nat.add(ux, sc(n, 1n)),
83    N.succ_cong(Nat.add(Nat.add(ux, un), ub), Nat.add(ux, Nat.add(un, ub)), N.add_assoc(ux, un, ub)),
84    Equal.trans(Nat, 1n+Nat.add(ux, Nat.add(un, ub)), Nat.add(ux, 1n+Nat.add(un, ub)), Nat.add(ux, sc(n, 1n)), Equal.sym(Nat, Nat.add(ux, 1n+Nat.add(un, ub)), 1n+Nat.add(ux, Nat.add(un, ub)), N.add_succ(ux, Nat.add(un, ub))), Equal.cong(Nat, Nat, z => Nat.add(ux, z), Nat.add(1n, Nat.add(un, ub)), sc(n, 1n), nv)))
85  +chain = Equal.trans(Nat, Nat.add(Nat.add(us, sc(n, c5)), ub), Nat.add(Nat.add(1n, Nat.add(ux, un)), ub), Nat.add(d, ub),
86    Equal.cong(Nat, Nat, z => Nat.add(z, ub), Nat.add(us, sc(n, c5)), Nat.add(1n, Nat.add(ux, un)), e5),
87    Equal.trans(Nat, Nat.add(Nat.add(1n, Nat.add(ux, un)), ub), Nat.add(ux, sc(n, 1n)), Nat.add(d, ub), mid, ew))
88  +e0 = A.add_cancel_r(Nat.add(us, sc(n, c5)), d, ub, chain)
89  +e1 = Equal.trans(Nat, Nat.add(us, sc(n, c5)), d, Nat.add(d, sc(n, 0n)), e0,
90    Equal.trans(Nat, d, Nat.add(d, 0n), Nat.add(d, sc(n, 0n)), Equal.sym(Nat, Nat.add(d, 0n), d, N.add_zero(d)), Equal.cong(Nat, Nat, z => Nat.add(d, z), 0n, sc(n, 0n), Equal.sym(Nat, sc(n, 0n), 0n, A.sc_zero(n)))))
91  uniq(n, one, h1, us, d, c5, 0n, e1, wb(n, one, h1, Word.sub(n, xw, bw)), hd)