def low_uniq

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/width.bend:131

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

131# r < 2^k: low(k, r + shift(k, q)) == r and high(k, r + shift(k, q)) == q
132def low_uniq(+k: Nat, +r: Nat, +q: Nat, +hr: {Nat.is_lt(r, C.pow2(k)) == True{} : Bool}) -> {C.low(k, Nat.add(r, C.shift(k, q))) == r : Nat}:
133  match k:
134    case 0n:
135      match r:
136        case 0n:
137          {==}
138        case 1n+ +rp:
139          Empty.absurd({C.low(0n, Nat.add(1n+rp, C.shift(0n, q))) == 1n+rp : Nat}, N.lt_zero_absurd(rp, hr))
140    case 1n+ +p:
141      +eh = half_dbl(r, C.shift(p, q))
142      +eb = bit_dbl(r, C.shift(p, q))
143      +hr2 = Equal.trans(Bool, Nat.is_lt(C.half(r), C.pow2(p)), Nat.is_lt(r, Nat.double(C.pow2(p))), True{}, lt_half(r, C.pow2(p)), hr)
144      +ih = low_uniq(p, C.half(r), q, hr2)
145      +el = Equal.trans(Nat, C.low(p, C.half(Nat.add(r, Nat.double(C.shift(p, q))))), C.low(p, Nat.add(C.half(r), C.shift(p, q))), C.half(r), Equal.cong(Nat, Nat, t => C.low(p, t), C.half(Nat.add(r, Nat.double(C.shift(p, q)))), Nat.add(C.half(r), C.shift(p, q)), eh), ih)
146      Equal.trans(Nat, Nat.add(C.bit(Nat.add(r, Nat.double(C.shift(p, q)))), Nat.double(C.low(p, C.half(Nat.add(r, Nat.double(C.shift(p, q))))))), Nat.add(C.bit(r), Nat.double(C.half(r))), r, Equal.trans(Nat, Nat.add(C.bit(Nat.add(r, Nat.double(C.shift(p, q)))), Nat.double(C.low(p, C.half(Nat.add(r, Nat.double(C.shift(p, q))))))), Nat.add(C.bit(r), Nat.double(C.low(p, C.half(Nat.add(r, Nat.double(C.shift(p, q))))))), Nat.add(C.bit(r), Nat.double(C.half(r))), Equal.cong(Nat, Nat, t => Nat.add(t, Nat.double(C.low(p, C.half(Nat.add(r, Nat.double(C.shift(p, q))))))), C.bit(Nat.add(r, Nat.double(C.shift(p, q)))), C.bit(r), eb), Equal.cong(Nat, Nat, t => Nat.add(C.bit(r), Nat.double(t)), C.low(p, C.half(Nat.add(r, Nat.double(C.shift(p, q))))), C.half(r), el)), Equal.sym(Nat, r, Nat.add(C.bit(r), Nat.double(C.half(r))), hb(r)))