def low_split

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64bits.bend:200

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/lemmas/proofs/nat_algebra.bend as NA

200# the low a + b bits: the low a, then the next b
201def low_split(+a: Nat, +b: Nat, +n: Nat) -> {C.low(Nat.add(a, b), n) == Nat.add(C.low(a, n), C.shift(a, C.low(b, C.high(a, n)))) : Nat}:
202  match a:
203    case 0n:
204      {==}
205    case 1n+ +p:
206      +l = C.low(p, C.half(n))
207      +s = C.shift(p, C.low(b, C.high(p, C.half(n))))
208      Equal.trans(Nat, Nat.add(C.bit(n), Nat.double(C.low(Nat.add(p, b), C.half(n)))), Nat.add(C.bit(n), Nat.double(Nat.add(l, s))), Nat.add(Nat.add(C.bit(n), Nat.double(l)), Nat.double(s)), Equal.cong(Nat, Nat, z => Nat.add(C.bit(n), Nat.double(z)), C.low(Nat.add(p, b), C.half(n)), Nat.add(l, s), low_split(p, b, C.half(n))), Equal.trans(Nat, Nat.add(C.bit(n), Nat.double(Nat.add(l, s))), Nat.add(C.bit(n), Nat.add(Nat.double(l), Nat.double(s))), Nat.add(Nat.add(C.bit(n), Nat.double(l)), Nat.double(s)), Equal.cong(Nat, Nat, z => Nat.add(C.bit(n), z), Nat.double(Nat.add(l, s)), Nat.add(Nat.double(l), Nat.double(s)), NA.double_add(l, s)), Equal.sym(Nat, Nat.add(Nat.add(C.bit(n), Nat.double(l)), Nat.double(s)), Nat.add(C.bit(n), Nat.add(Nat.double(l), Nat.double(s))), NA.add_assoc(C.bit(n), Nat.double(l), Nat.double(s)))))