def carry_lt

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

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
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/addition_bounds.bend as AB
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_bounds.bend as DB

157# the carry out of an addition is the wrap-around test sum < x
158def carry_lt(+n: Nat, +one: Nat, +h1: {one == 1n : Nat}, +s: Nat, +x: Nat, +y: Nat, +c: Bool, +e: {Nat.add(s, sc(n, S.bit_value(c))) == Nat.add(x, y) : Nat}, +hy: {Nat.is_lt(y, sc(n, one)) == True{} : Bool}) -> {Nat.is_lt(s, x) == c : Bool}:
159  match c:
160    case False{}:
161      +e0 = Equal.trans(Nat, s, Nat.add(s, 0n), Nat.add(x, y), Equal.sym(Nat, Nat.add(s, 0n), s, N.add_zero(s)), L.subst(Nat, z => {Nat.add(s, z) == Nat.add(x, y) : Nat}, sc(n, 0n), 0n, A.sc_zero(n), e))
162      %Equal.sym(Nat, s, Nat.add(y, x), Equal.trans(Nat, s, Nat.add(x, y), Nat.add(y, x), e0, N.add_comm(x, y))) : {Nat.is_lt(_, x) == False{} : Bool}
163      AB.offset_not_less(x, y)
164    case True{}:
165      +k = sc(n, 1n)
166      +hy1 = lt1(n, one, h1, y, hy)
167      +l1 = N.lt_add_left(y, k, x, hy1)
168      +l2 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(x, k)) == True{} : Bool}, Nat.add(x, y), Nat.add(k, s), Equal.trans(Nat, Nat.add(x, y), Nat.add(s, k), Nat.add(k, s), Equal.sym(Nat, Nat.add(s, k), Nat.add(x, y), e), N.add_comm(s, k)), l1)
169      +l3 = L.subst(Nat, z => {Nat.is_lt(Nat.add(k, s), z) == True{} : Bool}, Nat.add(x, k), Nat.add(k, x), N.add_comm(x, k), l2)
170      Equal.trans(Bool, Nat.is_lt(s, x), Nat.is_lt(Nat.add(k, s), Nat.add(k, x)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(k, s), Nat.add(k, x)), Nat.is_lt(s, x), DB.cancel_less(k, s, x)), l3)