def wsub

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixgen.bend:76

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/spec/math/fixed.bend as SF
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/math/typed/width.bend as WW

76# d == x - y + 2^k modulo 2^k: its low part plus y is x, plus 2^k when x < y
77def wsub(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +y: Nat, +d: Nat, +e: {Nat.add(d, y) == Nat.add(x, C.shift(k, one)) : Nat}, +hx: {C.fits(k, x) == True{} : Bool}, +c: Bool, +hc: {Nat.is_lt(x, y) == c : Bool}) -> {Nat.add(C.low(k, d), y) == Nat.add(x, C.shift(k, SF.bn(c))) : Nat}:
78  match c:
79    case True{}:
80      +S = C.shift(k, one)
81      +g1 = N.lt_add_r2(x, y, S, hc)
82      +g2 = Equal.trans(Bool, Nat.is_lt(Nat.add(d, y), Nat.add(y, S)), Nat.is_lt(Nat.add(x, S), Nat.add(y, S)), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(t, Nat.add(y, S)), Nat.add(d, y), Nat.add(x, S), e), g1)
83      +g3 = Equal.trans(Bool, Nat.is_lt(Nat.add(d, y), Nat.add(S, y)), Nat.is_lt(Nat.add(d, y), Nat.add(y, S)), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(Nat.add(d, y), t), Nat.add(S, y), Nat.add(y, S), N.add_comm(S, y)), g2)
84      +g4 = Equal.trans(Bool, Nat.is_lt(d, S), Nat.is_lt(Nat.add(d, y), Nat.add(S, y)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(d, y), Nat.add(S, y)), Nat.is_lt(d, S), WW.lt_cancel_r(d, S, y)), g3)
85      +hf = WW.fits_one(k, one, h1, d, g4)
86      %h1 : {Nat.add(C.low(k, d), y) == Nat.add(x, C.shift(k, _)) : Nat}
87      %Equal.sym(Nat, C.low(k, d), d, WW.low_fit(k, d, hf)) : {Nat.add(_, y) == Nat.add(x, C.shift(k, one)) : Nat}
88      e
89    case False{}:
90      +S = C.shift(k, one)
91      +z = Nat.sub(x, y)
92      +hle = N.not_lt_le(x, y, hc)
93      +exz = N.sub_add(x, y, hle)
94      +e1 = Equal.trans(Nat, Nat.add(Nat.add(z, S), y), Nat.add(Nat.add(y, z), S), Nat.add(x, S), rot3(z, S, y), Equal.cong(Nat, Nat, t => Nat.add(t, S), Nat.add(y, z), x, exz))
95      +ed = add_cancel_r(d, Nat.add(z, S), y, Equal.trans(Nat, Nat.add(d, y), Nat.add(x, S), Nat.add(Nat.add(z, S), y), e, Equal.sym(Nat, Nat.add(Nat.add(z, S), y), Nat.add(x, S), e1)))
96      +el = Equal.trans(Nat, C.low(k, d), C.low(k, Nat.add(z, S)), z, Equal.cong(Nat, Nat, t => C.low(k, t), d, Nat.add(z, S), ed), WW.low_u(k, z, one, fits_sub(k, x, y, hx)))
97      %Equal.sym(Nat, C.low(k, d), z, el) : {Nat.add(_, y) == Nat.add(x, C.shift(k, 0n)) : Nat}
98      %Equal.sym(Nat, C.shift(k, 0n), 0n, WW.shift_zero(k)) : {Nat.add(z, y) == Nat.add(x, _) : Nat}
99      Equal.trans(Nat, Nat.add(z, y), x, Nat.add(x, 0n), Equal.trans(Nat, Nat.add(z, y), Nat.add(y, z), x, N.add_comm(z, y), exz), Equal.sym(Nat, Nat.add(x, 0n), x, N.add_zero(x)))