def xsh

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64cmp.bend:107

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/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

107# 2^xexp = 2^1925 * 2^e' with e' = max(E, 1)
108def xsh(+E: Nat, +b: Bool, +m: Nat) -> {C.shift(SF.pick(Nat, b, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), m) == C.shift(1925n, C.shift(SF.pick(Nat, b, 1n, E), m)) : Nat}:
109  match b:
110    case True{}:
111      # each step is stated in the goal's own terms: a conversion that
112      # unfolded C.shift(1925n, _) would walk 1925 doublings per level
113      +e1 = Equal.cong(Nat, Nat, z => C.shift(z, m), SF.pick(Nat, True{}, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), Nat.add(1925n, 1n), {==})
114      +e2 = Equal.cong(Nat, Nat, z => C.shift(1925n, C.shift(z, m)), 1n, SF.pick(Nat, True{}, 1n, E), {==})
115      Equal.trans(Nat, C.shift(SF.pick(Nat, True{}, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), m), C.shift(Nat.add(1925n, 1n), m), C.shift(1925n, C.shift(SF.pick(Nat, True{}, 1n, E), m)), e1, Equal.trans(Nat, C.shift(Nat.add(1925n, 1n), m), C.shift(1925n, C.shift(1n, m)), C.shift(1925n, C.shift(SF.pick(Nat, True{}, 1n, E), m)), WW.shift_comp(1925n, 1n, m), e2))
116    case False{}:
117      +e1 = Equal.cong(Nat, Nat, z => C.shift(z, m), SF.pick(Nat, False{}, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), Nat.add(1925n, E), esub(E))
118      +e2 = Equal.cong(Nat, Nat, z => C.shift(1925n, C.shift(z, m)), E, SF.pick(Nat, False{}, 1n, E), {==})
119      Equal.trans(Nat, C.shift(SF.pick(Nat, False{}, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), m), C.shift(Nat.add(1925n, E), m), C.shift(1925n, C.shift(SF.pick(Nat, False{}, 1n, E), m)), e1, Equal.trans(Nat, C.shift(Nat.add(1925n, E), m), C.shift(1925n, C.shift(E, m)), C.shift(1925n, C.shift(SF.pick(Nat, False{}, 1n, E), m)), WW.shift_comp(1925n, E, m), e2))