def carry_fits

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32laws.bend:102

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/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U
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/word.bend as WD
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/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

102# the carry of an addition is "the sum does not fit"
103def carry_fits(+k: Nat, +s: Nat, +n: Nat, +c: Bool, +e: {Nat.add(s, WD.sc(k, S.bit_value(c))) == n : Nat}, +hs: {Nat.is_lt(s, C.pow2(k)) == True{} : Bool}) -> {c == Bool.not(C.fits(k, n)) : Bool}:
104  match c:
105    case False{}:
106      %Equal.sym(Bool, C.fits(k, n), Nat.is_lt(n, C.pow2(k)), WW.fits_lt(k, n)) : {False{} == Bool.not(_) : Bool}
107      %e : {False{} == Bool.not(Nat.is_lt(_, C.pow2(k))) : Bool}
108      %Equal.sym(Nat, WD.sc(k, 0n), 0n, A.sc_zero(k)) : {False{} == Bool.not(Nat.is_lt(Nat.add(s, _), C.pow2(k))) : Bool}
109      %Equal.sym(Nat, Nat.add(s, 0n), s, N.add_zero(s)) : {False{} == Bool.not(Nat.is_lt(_, C.pow2(k))) : Bool}
110      %Equal.sym(Bool, Nat.is_lt(s, C.pow2(k)), True{}, hs) : {False{} == Bool.not(_) : Bool}
111      {==}
112    case True{}:
113      %Equal.sym(Bool, C.fits(k, n), Nat.is_lt(n, C.pow2(k)), WW.fits_lt(k, n)) : {True{} == Bool.not(_) : Bool}
114      %e : {True{} == Bool.not(Nat.is_lt(_, C.pow2(k))) : Bool}
115      %U.pow2_scale(k) : {True{} == Bool.not(Nat.is_lt(Nat.add(s, _), C.pow2(k))) : Bool}
116      +le = L.subst(Nat, z => {Nat.is_le(C.pow2(k), z) == True{} : Bool}, Nat.add(C.pow2(k), s), Nat.add(s, C.pow2(k)), N.add_comm(C.pow2(k), s), N.le_add_right(C.pow2(k), s))
117      %Equal.sym(Bool, Nat.is_lt(Nat.add(s, C.pow2(k)), C.pow2(k)), False{}, N.le_not_lt(Nat.add(s, C.pow2(k)), C.pow2(k), le)) : {True{} == Bool.not(_) : Bool}
118      {==}