def imid_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:1129

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/src/math/generic.bend as G
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
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/math/typed/u32.bend as U32P
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AR2

1129def imid_v(+K: Nat, +hK: {K == 32n : Nat}, +lo: U32, +hi: U32, +a: Nat, +w: Nat, +ha: {v(lo) == a : Nat}, +hh: {v(hi) == Nat.add(a, w) : Nat}) -> {v(G.imid(~U32, ~I.u32_op, lo, hi)) == Nat.add(a, Nat.div(w, 2n)) : Nat}:
1130  +s = I.u32_op(NM.Sub{hi, lo})
1131  +es = Equal.trans(Nat, v(s), Nat.sub(v(hi), v(lo)), w, LW.ops_sub(hi, lo, le_v(lo, hi, a, Nat.add(a, w), ha, hh, N.le_add_right(a, w))), Equal.trans(Nat, Nat.sub(v(hi), v(lo)), Nat.sub(Nat.add(a, w), a), w, nsub(v(hi), v(lo), Nat.add(a, w), a, hh, ha), N.add_sub_cancel(a, w)))
1132  +h = I.u32_op(NM.Half{s})
1133  +eh = Equal.trans(Nat, v(h), Nat.div(v(s), 2n), Nat.div(w, 2n), LW.ops_half(s), Equal.cong(Nat, Nat, t => Nat.div(t, 2n), v(s), w, es))
1134  +sum = Nat.add(a, Nat.div(w, 2n))
1135  +esum = nadd(v(lo), v(h), a, Nat.div(w, 2n), ha, eh)
1136  +hle = N.le_add_left(Nat.div(w, 2n), w, a, AR2.div_le(w, 2n))
1137  +hhk = L.subst(Nat, z => {Nat.is_lt(z, C.pow2(K)) == True{} : Bool}, v(hi), Nat.add(a, w), hh, U32P.val_lt(1n, {==}, K, hK, hi))
1138  +hfit = fits32(K, hK, sum, N.le_lt_trans(sum, Nat.add(a, w), C.pow2(K), hle, hhk))
1139  Equal.trans(Nat, v(I.u32_op(NM.Add{lo, h})), Nat.add(v(lo), v(h)), sum, LW.ops_add(lo, h, ao_of(lo, h, sum, esum, True{}, hfit)), esum)