def div_sh

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

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
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/width.bend as WW

154# n div 2^k
155def div_sh(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +n: Nat) -> {Nat.div(n, C.shift(k, one)) == C.high(k, n) : Nat}:
156  +pp = Nat.sub(C.shift(k, one), 1n)
157  +ep = Equal.trans(Nat, C.pow2(k), C.shift(k, 1n), C.shift(k, one), Equal.sym(Nat, C.shift(k, 1n), C.pow2(k), WW.shift_one(k)), Equal.cong(Nat, Nat, o => C.shift(k, o), 1n, one, Equal.sym(Nat, one, 1n, h1)))
158  +hpos = L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, C.pow2(k), C.shift(k, one), ep, N.pow2_pos(k))
159  +hs = N.sub_add(C.shift(k, one), 1n, hpos)
160  +hp = Equal.trans(Nat, C.pow2(k), C.shift(k, one), 1n+pp, ep, Equal.sym(Nat, 1n+pp, C.shift(k, one), hs))
161  L.subst(Nat, z => {Nat.div(n, z) == C.high(k, n) : Nat}, 1n+pp, C.shift(k, one), hs, Equal.sym(Nat, C.high(k, n), Nat.div(n, 1n+pp), WW.high_div(k, n, pp, hp)))