~/jendhub

proofs/math/typed/f64ratio.bend

bend-collections-laws-math@1.0.0.0 · 159 lines · 13 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
4import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
5import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
6import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
7import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
8import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NE
9import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
10import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
11import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
12import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64clz.bend as CZ
15import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
16import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL
17import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT
18import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64nrp.bend as NR
19import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend as BL
20import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64tools.bend as T
21import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64conv.bend as CV
22
23# as_integer_ratio (python_style_math_stdlib_design.pdf 3.3; CPython's
24# float.as_integer_ratio, with the denominator as its exponent):
25# AsIntegerRatio.value. Below 2^52 the significand loses its trailing zeros
26# into the denominator (ctz, one halving at a time, is the spec's tz by
27# Odd.value / Half.value); above, it is shifted left and must fit 64 bits
28# (Clz.value, f64nrp.tbf / tbn, as in f64conv).
29
30# ---- trailing zeros ----
31
32def cz(+fuel: Nat, +w: WU.U64, +o: Bool, +ho: {X.odd(w) == o : Bool}) -> {F.ctz_go(fuel, w, o) == SF.tz(fuel, SW.value(w)) : Nat}:
33  match fuel o:
34    case 0n _:
35      {==}
36    case 1n+ +f True{}:
37      +h = Equal.trans(Bool, Nat.is_eq(Nat.mod(SW.value(w), 2n), 1n), X.odd(w), True{}, Equal.sym(Bool, X.odd(w), Nat.is_eq(Nat.mod(SW.value(w), 2n), 1n), WA.odd_value(w)), ho)
38      Equal.sym(Nat, SF.tz(1n+f, SW.value(w)), 0n, Equal.cong(Bool, Nat, b => SF.pick(Nat, b, 0n, 1n+SF.tz(f, Nat.div(SW.value(w), 2n))), Nat.is_eq(Nat.mod(SW.value(w), 2n), 1n), True{}, h))
39    case 1n+ +f False{}:
40      +h = Equal.trans(Bool, Nat.is_eq(Nat.mod(SW.value(w), 2n), 1n), X.odd(w), False{}, Equal.sym(Bool, X.odd(w), Nat.is_eq(Nat.mod(SW.value(w), 2n), 1n), WA.odd_value(w)), ho)
41      +e0 = Equal.cong(Bool, Nat, b => SF.pick(Nat, b, 0n, 1n+SF.tz(f, Nat.div(SW.value(w), 2n))), Nat.is_eq(Nat.mod(SW.value(w), 2n), 1n), False{}, h)
42      +e1 = cz(f, X.half(w), X.odd(X.half(w)), {==})
43      +e2 = Equal.cong(Nat, Nat, t => SF.tz(f, t), SW.value(X.half(w)), Nat.div(SW.value(w), 2n), WA.half_value(w))
44      +e3 = Equal.trans(Nat, F.ctz_go(f, X.half(w), X.odd(X.half(w))), SF.tz(f, SW.value(X.half(w))), SF.tz(f, Nat.div(SW.value(w), 2n)), e1, e2)
45      Equal.trans(Nat, 1n+F.ctz_go(f, X.half(w), X.odd(X.half(w))), 1n+SF.tz(f, Nat.div(SW.value(w), 2n)), SF.tz(1n+f, SW.value(w)), Equal.cong(Nat, Nat, t => 1n+t, F.ctz_go(f, X.half(w), X.odd(X.half(w))), SF.tz(f, Nat.div(SW.value(w), 2n)), e3), Equal.sym(Nat, SF.tz(1n+f, SW.value(w)), 1n+SF.tz(f, Nat.div(SW.value(w), 2n)), e0))
46
47def ctz_v(+w: WU.U64) -> {F.ctz(w) == SF.tz(64n, SW.value(w)) : Nat}:
48  cz(64n, w, X.odd(w), {==})
49
50# ---- below 2^52 ----
51
52def SMALL(+x: F.F64) -> Result<&2, &2, NE.NumError, SF.Rat>:
53  Done{SF.Rat{SF.sign(x), C.high(Nat.min(SF.tz(64n, SF.mant(x)), Nat.sub(SF.zb(), SF.xexp(x))), SF.mant(x)), Nat.sub(Nat.sub(SF.zb(), SF.xexp(x)), Nat.min(SF.tz(64n, SF.mant(x)), Nat.sub(SF.zb(), SF.xexp(x))))}}
54
55def G(+s: Bool, +V: Nat, +k: Nat, +j: Nat) -> Result<&2, &2, NE.NumError, SF.Rat>:
56  Done{SF.Rat{s, C.high(j, V), Nat.sub(k, j)}}
57
58def small_v(+x: F.F64) -> {SF.rtriple(F.ar_small(F.signbit(x), F.dmant(x), Nat.sub(3000n, F.dexp(x)), Nat.min(F.ctz(F.dmant(x)), Nat.sub(3000n, F.dexp(x))))) == SMALL(x) : Result<&2, &2, NE.NumError, SF.Rat>}:
59  +w = F.dmant(x)
60  +V = SW.value(w)
61  +k = Nat.sub(3000n, F.dexp(x))
62  +j = Nat.min(F.ctz(w), k)
63  +e1 = Equal.cong(Nat, Result<&2, &2, NE.NumError, SF.Rat>, t => Done{SF.Rat{F.signbit(x), t, Nat.sub(k, j)}}, SW.value(X.shr(w, j)), C.high(j, V), SH.shr_value(w, j))
64  +e2 = Equal.cong(Nat, Result<&2, &2, NE.NumError, SF.Rat>, t => G(F.signbit(x), V, k, Nat.min(t, k)), F.ctz(w), SF.tz(64n, V), ctz_v(w))
65  +e3 = Equal.cong(Bool, Result<&2, &2, NE.NumError, SF.Rat>, t => G(t, V, k, Nat.min(SF.tz(64n, V), k)), F.signbit(x), SF.sign(x), FB.signbit_value(x))
66  +e4 = Equal.cong(Nat, Result<&2, &2, NE.NumError, SF.Rat>, t => G(SF.sign(x), t, k, Nat.min(SF.tz(64n, t), k)), V, SF.mant(x), T.dmant_value(x))
67  +e5 = Equal.cong(Nat, Result<&2, &2, NE.NumError, SF.Rat>, t => G(SF.sign(x), SF.mant(x), Nat.sub(3000n, t), Nat.min(SF.tz(64n, SF.mant(x)), Nat.sub(3000n, t))), F.dexp(x), SF.xexp(x), T.dexp_value(x))
68  +r1 = G(F.signbit(x), V, k, j)
69  +r2 = G(F.signbit(x), V, k, Nat.min(SF.tz(64n, V), k))
70  +r3 = G(SF.sign(x), V, k, Nat.min(SF.tz(64n, V), k))
71  +r4 = G(SF.sign(x), SF.mant(x), k, Nat.min(SF.tz(64n, SF.mant(x)), k))
72  Equal.trans(Result<&2, &2, NE.NumError, SF.Rat>, Done{SF.Rat{F.signbit(x), SW.value(X.shr(w, j)), Nat.sub(k, j)}}, r1, SMALL(x), e1, Equal.trans(Result<&2, &2, NE.NumError, SF.Rat>, r1, r2, SMALL(x), e2, Equal.trans(Result<&2, &2, NE.NumError, SF.Rat>, r2, r3, SMALL(x), e3, Equal.trans(Result<&2, &2, NE.NumError, SF.Rat>, r3, r4, SMALL(x), e4, e5))))
73
74# ---- at least 2^52 ----
75
76def BIGR(+s: Bool, +n: Nat) -> Result<&2, &2, NE.NumError, SF.Rat>:
77  SF.pick(Result<&2, &2, NE.NumError, SF.Rat>, C.fits(64n, n), Done{SF.Rat{s, n, 0n}}, Fail{NE.Overflow{}})
78
79def ab_c(+s: Bool, +w: WU.U64, +k: Nat, +hz: {Nat.is_eq(SW.value(w), 0n) == False{} : Bool}, +c: Bool, +hc: {Nat.is_le(Nat.add(k, M.bit_length(SW.value(w))), 64n) == c : Bool}) -> {SF.rtriple(F.ar_big(s, w, k, c)) == BIGR(s, C.shift(k, SW.value(w))) : Result<&2, &2, NE.NumError, SF.Rat>}:
80  match c:
81    case True{}:
82      +V = SW.value(w)
83      +B = M.bit_length(V)
84      +S = C.shift(k, V)
85      +hb1 = BL.bl_pos(V, hz, B, {==})
86      +hkl = Equal.trans(Bool, Nat.is_lt(k, Nat.add(k, B)), Nat.is_lt(Nat.add(k, 0n), Nat.add(k, B)), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(t, Nat.add(k, B)), k, Nat.add(k, 0n), Equal.sym(Nat, Nat.add(k, 0n), k, N.add_zero(k))), N.lt_add_left(0n, B, k, N.succ_le_lt(0n, B, hb1)))
87      +hk = N.lt_le_trans(k, Nat.add(k, B), 64n, hkl, hc)
88      +ev = FL.shl_v(w, k, B, hk, hc, RT.bl_fit(V))
89      +hf = SH.fits_mono(Nat.add(k, B), 64n, S, hc, NR.tbf(k, V, Nat.add(k, B), {==}))
90      +e1 = Equal.cong(Nat, Result<&2, &2, NE.NumError, SF.Rat>, n => Done{SF.Rat{s, n, 0n}}, SW.value(X.shl(w, k)), S, ev)
91      +e2 = Equal.cong(Bool, Result<&2, &2, NE.NumError, SF.Rat>, b => SF.pick(Result<&2, &2, NE.NumError, SF.Rat>, b, Done{SF.Rat{s, S, 0n}}, Fail{NE.Overflow{}}), C.fits(64n, S), True{}, hf)
92      Equal.trans(Result<&2, &2, NE.NumError, SF.Rat>, Done{SF.Rat{s, SW.value(X.shl(w, k)), 0n}}, Done{SF.Rat{s, S, 0n}}, BIGR(s, S), e1, Equal.sym(Result<&2, &2, NE.NumError, SF.Rat>, BIGR(s, S), Done{SF.Rat{s, S, 0n}}, e2))
93    case False{}:
94      +V = SW.value(w)
95      +B = M.bit_length(V)
96      +S = C.shift(k, V)
97      +J = Nat.add(k, B)
98      +K = Nat.sub(J, 1n)
99      +hJ = N.not_le_lt(J, 64n, hc)
100      +hJ1 = N.le_trans(1n, 65n, J, {==}, N.lt_succ_le_succ(64n, J, hJ))
101      +ek = Equal.sym(Nat, Nat.add(1n, K), J, N.sub_add(J, 1n, hJ1))
102      +hK = N.lt_succ_le(64n, K, L.subst(Nat, t => {Nat.is_lt(64n, t) == True{} : Bool}, J, 1n+K, ek, hJ))
103      +nf = FL.nfit_mono(64n, K, S, hK, NR.tbn(k, V, K, hz, ek))
104      Equal.sym(Result<&2, &2, NE.NumError, SF.Rat>, BIGR(s, S), Fail{NE.Overflow{}}, Equal.cong(Bool, Result<&2, &2, NE.NumError, SF.Rat>, b => SF.pick(Result<&2, &2, NE.NumError, SF.Rat>, b, Done{SF.Rat{s, S, 0n}}, Fail{NE.Overflow{}}), C.fits(64n, S), False{}, nf))
105
106def big_v(+x: F.F64, +hc: {Nat.is_le(3000n, F.dexp(x)) == True{} : Bool}) -> {SF.rtriple(F.ar_big(F.signbit(x), F.dmant(x), Nat.sub(F.dexp(x), 3000n), Nat.is_le(Nat.add(Nat.sub(F.dexp(x), 3000n), Nat.sub(64n, X.clz(F.dmant(x)))), 64n))) == BIGR(SF.sign(x), C.shift(Nat.sub(SF.xexp(x), SF.zb()), SF.mant(x))) : Result<&2, &2, NE.NumError, SF.Rat>}:
107  +w = F.dmant(x)
108  +V = SW.value(w)
109  +B = M.bit_length(V)
110  +k = Nat.sub(F.dexp(x), 3000n)
111  +hB = N.le_trans(B, 53n, 64n, BL.bl_le(53n, V, T.mw53(x), Nat.is_le(B, 53n), {==}), {==})
112  +eb = Equal.trans(Nat, Nat.sub(64n, X.clz(w)), Nat.sub(64n, Nat.sub(64n, B)), B, Equal.cong(Nat, Nat, t => Nat.sub(64n, t), X.clz(w), Nat.sub(64n, B), CZ.clz_value(w)), T.subsub(64n, B, hB))
113  +e0 = Equal.cong(Nat, Result<&2, &2, NE.NumError, SF.Rat>, t => SF.rtriple(F.ar_big(F.signbit(x), w, k, Nat.is_le(Nat.add(k, t), 64n))), Nat.sub(64n, X.clz(w)), B, eb)
114  +e1 = ab_c(F.signbit(x), w, k, CV.big_nz(x, hc), Nat.is_le(Nat.add(k, B), 64n), {==})
115  +e2 = Equal.cong(Bool, Result<&2, &2, NE.NumError, SF.Rat>, t => BIGR(t, C.shift(k, V)), F.signbit(x), SF.sign(x), FB.signbit_value(x))
116  +e3 = Equal.cong(Nat, Result<&2, &2, NE.NumError, SF.Rat>, t => BIGR(SF.sign(x), C.shift(k, t)), V, SF.mant(x), T.dmant_value(x))
117  +e4 = Equal.cong(Nat, Result<&2, &2, NE.NumError, SF.Rat>, t => BIGR(SF.sign(x), C.shift(Nat.sub(t, 3000n), SF.mant(x))), F.dexp(x), SF.xexp(x), T.dexp_value(x))
118  +r0 = SF.rtriple(F.ar_big(F.signbit(x), w, k, Nat.is_le(Nat.add(k, Nat.sub(64n, X.clz(w))), 64n)))
119  +r1 = SF.rtriple(F.ar_big(F.signbit(x), w, k, Nat.is_le(Nat.add(k, B), 64n)))
120  +r2 = BIGR(F.signbit(x), C.shift(k, V))
121  +r3 = BIGR(SF.sign(x), C.shift(k, V))
122  +r4 = BIGR(SF.sign(x), C.shift(k, SF.mant(x)))
123  +r5 = BIGR(SF.sign(x), C.shift(Nat.sub(SF.xexp(x), SF.zb()), SF.mant(x)))
124  Equal.trans(Result<&2, &2, NE.NumError, SF.Rat>, r0, r1, r5, e0, Equal.trans(Result<&2, &2, NE.NumError, SF.Rat>, r1, r2, r5, e1, Equal.trans(Result<&2, &2, NE.NumError, SF.Rat>, r2, r3, r5, e2, Equal.trans(Result<&2, &2, NE.NumError, SF.Rat>, r3, r4, r5, e3, e4))))
125
126# ---- the cases ----
127
128def FINR(+x: F.F64, +c: Bool) -> Result<&2, &2, NE.NumError, SF.Rat>:
129  SF.pick(Result<&2, &2, NE.NumError, SF.Rat>, c, BIGR(SF.sign(x), CV.IPc(x, c)), SMALL(x))
130
131def arf_c(+x: F.F64, +c: Bool, +hc: {Nat.is_le(3000n, F.dexp(x)) == c : Bool}) -> {SF.rtriple(F.ar_fin(x, c)) == FINR(x, c) : Result<&2, &2, NE.NumError, SF.Rat>}:
132  match c:
133    case True{}:
134      big_v(x, hc)
135    case False{}:
136      small_v(x)
137
138def arz_c(+x: F.F64, +iz: Bool) -> {SF.rtriple(F.ar_z(x, iz)) == SF.pick(Result<&2, &2, NE.NumError, SF.Rat>, iz, Done{SF.Rat{False{}, 0n, 0n}}, FINR(x, Nat.is_le(SF.zb(), SF.xexp(x)))) : Result<&2, &2, NE.NumError, SF.Rat>}:
139  match iz:
140    case True{}:
141      {==}
142    case False{}:
143      +e1 = arf_c(x, Nat.is_le(3000n, F.dexp(x)), {==})
144      +e2 = Equal.cong(Nat, Result<&2, &2, NE.NumError, SF.Rat>, t => FINR(x, Nat.is_le(3000n, t)), F.dexp(x), SF.xexp(x), T.dexp_value(x))
145      Equal.trans(Result<&2, &2, NE.NumError, SF.Rat>, SF.rtriple(F.ar_fin(x, Nat.is_le(3000n, F.dexp(x)))), FINR(x, Nat.is_le(3000n, F.dexp(x))), FINR(x, Nat.is_le(3000n, SF.xexp(x))), e1, e2)
146
147def ar_c(+x: F.F64, +t: Bool, +z: Bool, +hz: {X.is_zero(F.frac(x)) == z : Bool}) -> {SF.rtriple(F.ar_cls(x, t)) == SF.pick(Result<&2, &2, NE.NumError, SF.Rat>, Bool.and(t, Bool.not(z)), Fail{NE.BadDomain{}}, SF.pick(Result<&2, &2, NE.NumError, SF.Rat>, Bool.and(t, z), Fail{NE.Overflow{}}, SF.pick(Result<&2, &2, NE.NumError, SF.Rat>, SF.is_zero(x), Done{SF.Rat{False{}, 0n, 0n}}, FINR(x, Nat.is_le(SF.zb(), SF.xexp(x)))))) : Result<&2, &2, NE.NumError, SF.Rat>}:
148  match t z:
149    case True{} True{}:
150      Equal.cong(Bool, Result<&2, &2, NE.NumError, SF.Rat>, b => SF.rtriple(F.ar_top(Bool.not(b))), X.is_zero(F.frac(x)), True{}, hz)
151    case True{} False{}:
152      Equal.cong(Bool, Result<&2, &2, NE.NumError, SF.Rat>, b => SF.rtriple(F.ar_top(Bool.not(b))), X.is_zero(F.frac(x)), False{}, hz)
153    case False{} _:
154      +e1 = Equal.cong(Bool, Result<&2, &2, NE.NumError, SF.Rat>, b => SF.rtriple(F.ar_z(x, b)), F.is_zero(x), SF.is_zero(x), FB.is_zero_value(x))
155      Equal.trans(Result<&2, &2, NE.NumError, SF.Rat>, SF.rtriple(F.ar_z(x, F.is_zero(x))), SF.rtriple(F.ar_z(x, SF.is_zero(x))), SF.pick(Result<&2, &2, NE.NumError, SF.Rat>, SF.is_zero(x), Done{SF.Rat{False{}, 0n, 0n}}, FINR(x, Nat.is_le(SF.zb(), SF.xexp(x)))), e1, arz_c(x, SF.is_zero(x)))
156
157def as_integer_ratio_value(+x: F.F64) -> SF.AsIntegerRatio.value(x):
158  +e1 = Equal.cong(Nat, Result<&2, &2, NE.NumError, SF.Rat>, u => SF.rtriple(F.ar_cls(x, Nat.is_eq(u, 2047n))), F.exp_field(x), SF.efield(x), T.ea(x))
159  Equal.trans(Result<&2, &2, NE.NumError, SF.Rat>, SF.rtriple(F.as_integer_ratio(x)), SF.rtriple(F.ar_cls(x, Nat.is_eq(SF.efield(x), 2047n))), SF.as_ratio(x), e1, ar_c(x, Nat.is_eq(SF.efield(x), 2047n), Nat.is_eq(SF.frac(x), 0n), T.fz(x)))