def high_uniq

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

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N

148def high_uniq(+k: Nat, +r: Nat, +q: Nat, +hr: {Nat.is_lt(r, C.pow2(k)) == True{} : Bool}) -> {C.high(k, Nat.add(r, C.shift(k, q))) == q : Nat}:
149  match k:
150    case 0n:
151      match r:
152        case 0n:
153          {==}
154        case 1n+ +rp:
155          Empty.absurd({C.high(0n, Nat.add(1n+rp, C.shift(0n, q))) == q : Nat}, N.lt_zero_absurd(rp, hr))
156    case 1n+ +p:
157      +eh = half_dbl(r, C.shift(p, q))
158      +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)
159      Equal.trans(Nat, C.high(p, C.half(Nat.add(r, Nat.double(C.shift(p, q))))), C.high(p, Nat.add(C.half(r), C.shift(p, q))), q, Equal.cong(Nat, Nat, t => C.high(p, t), C.half(Nat.add(r, Nat.double(C.shift(p, q)))), Nat.add(C.half(r), C.shift(p, q)), eh), high_uniq(p, C.half(r), q, hr2))