def skip_v

bend-collections-laws-math@1.0.0.0 · proofs/math/random/wrappers.bend:206

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/random/rand.bend as R
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

206# skip(k, n) = n div 2^(8k)
207def skip_v(+k: Nat, +n: Nat) -> {R.skip(k, n) == C.high(sh8(k), n) : Nat}:
208  match k:
209    case 0n:
210      {==}
211    case 1n+j:
212      Equal.trans(Nat, R.skip(j, Nat.div(n, 256n)), C.high(sh8(j), Nat.div(n, 256n)), C.high(Nat.add(8n, sh8(j)), n),
213        skip_v(j, Nat.div(n, 256n)),
214        Equal.trans(Nat, C.high(sh8(j), Nat.div(n, 256n)), C.high(sh8(j), C.high(8n, n)), C.high(Nat.add(8n, sh8(j)), n),
215          Equal.cong(Nat, Nat, z => C.high(sh8(j), z), Nat.div(n, 256n), C.high(8n, n), div256(n)),
216          Equal.sym(Nat, C.high(Nat.add(8n, sh8(j)), n), C.high(sh8(j), C.high(8n, n)), WW.high_comp(sh8(j), 8n, n))))