def c_one

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64add.bend:99

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/logic.bend as L
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/math/typed/width.bend as WW

99# s + 1 carries exactly when s is all ones (1 + vm == 2^32)
100def c_one(+one: Nat, +h1: {one == 1n : Nat}, +r: Nat, +vs: Nat, +vm: Nat, +cc: Bool, +e: {Nat.add(r, C.shift(32n, WD.bo(cc, one))) == Nat.add(vs, 1n) : Nat}, +em: {1n+vm == C.shift(32n, one) : Nat}, +hr: {C.fits(32n, r) == True{} : Bool}, +hs: {C.fits(32n, vs) == True{} : Bool}) -> {cc == Nat.is_eq(vs, vm) : Bool}:
101  match cc:
102    case True{}:
103      +hs1 = L.subst(Nat, z => {Nat.is_lt(vs, z) == True{} : Bool}, C.shift(32n, one), 1n+vm, Equal.sym(Nat, 1n+vm, C.shift(32n, one), em), WW.lt_one(32n, one, h1, vs, hs))
104      +hle = N.lt_succ_le(vs, vm, hs1)
105      +e2 = Equal.trans(Nat, Nat.add(r, 1n+vm), Nat.add(r, C.shift(32n, one)), 1n+vs, Equal.cong(Nat, Nat, z => Nat.add(r, z), 1n+vm, C.shift(32n, one), em), Equal.trans(Nat, Nat.add(r, C.shift(32n, one)), Nat.add(vs, 1n), 1n+vs, e, plus1(vs)))
106      +hge0 = L.subst(Nat, z => {Nat.is_le(1n+vm, z) == True{} : Bool}, Nat.add(r, 1n+vm), 1n+vs, e2, L.subst(Nat, z => {Nat.is_le(1n+vm, z) == True{} : Bool}, Nat.add(1n+vm, r), Nat.add(r, 1n+vm), N.add_comm(1n+vm, r), N.le_add_right(1n+vm, r)))
107      +eqv = N.le_antisym(vs, vm, hle, hge0)
108      Equal.sym(Bool, Nat.is_eq(vs, vm), True{}, L.subst(Nat, z => {Nat.is_eq(z, vm) == True{} : Bool}, vm, vs, Equal.sym(Nat, vs, vm, eqv), N.is_eq_refl(vm)))
109    case False{}:
110      +e0 = Equal.trans(Nat, r, Nat.add(r, 0n), 1n+vs, Equal.sym(Nat, Nat.add(r, 0n), r, N.add_zero(r)), Equal.trans(Nat, Nat.add(r, 0n), Nat.add(r, C.shift(32n, 0n)), 1n+vs, Equal.cong(Nat, Nat, z => Nat.add(r, z), 0n, C.shift(32n, 0n), Equal.sym(Nat, C.shift(32n, 0n), 0n, WW.shift_zero(32n))), Equal.trans(Nat, Nat.add(r, C.shift(32n, 0n)), Nat.add(vs, 1n), 1n+vs, e, plus1(vs))))
111      +hr1 = L.subst(Nat, z => {Nat.is_lt(r, z) == True{} : Bool}, C.shift(32n, one), 1n+vm, Equal.sym(Nat, 1n+vm, C.shift(32n, one), em), WW.lt_one(32n, one, h1, r, hr))
112      +hlt = L.subst(Nat, z => {Nat.is_lt(z, 1n+vm) == True{} : Bool}, r, 1n+vs, e0, hr1)
113      Equal.sym(Bool, Nat.is_eq(vs, vm), False{}, N.is_eq_lt(vs, vm, hlt))