~/jendhub

proofs/math/typed/f64light.bend

bend-collections-laws-math@1.0.0.0 · 143 lines · 21 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
3import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
4import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
5import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
6import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
7import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
8import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
9import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
10import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
11import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
12import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
13import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
14import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
15import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC
16import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
17import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
18import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
19import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT
20import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
21
22# Small F64 lemmas shared by the division and the square-root proofs. They
23# live here so that the square-root root does not import (and re-check) the
24# division proofs.
25
26def v(+x: U32) -> Nat:
27  U32.to_nat(x)
28
29def fval_g(+xl: U32, +xh: U32, +m: U32, +hm: {m == U32{WD.mask(32n, 20n)} : U32}) -> {SW.value(WU.U64{xl, U32.and(xh, m)}) == SF.frac(F.Bits{xl, xh}) : Nat}:
30  Equal.cong(Nat, Nat, z => Nat.add(v(xl), C.shift(32n, z)), v(U32.and(xh, m)), C.low(20n, v(xh)), FB.andm(xh, 20n, m, hm))
31
32def hea(+xl: U32, +xh: U32) -> {F.exp_field(F.Bits{xl, xh}) == SF.efield(F.Bits{xl, xh}) : Nat}:
33  FB.ef_g(1n, {==}, xh, 1048576, {==}, 2047, {==})
34
35def hfr(+xl: U32, +xh: U32) -> {SW.value(F.frac(F.Bits{xl, xh})) == SF.frac(F.Bits{xl, xh}) : Nat}:
36  fval_g(xl, xh, 1048575, {==})
37
38def non(+x: F.F64, +b: Bool) -> {F.nan_or(x, b) == SF.pick(F.F64, b, F.nan(), x) : F.F64}:
39  match b:
40    case True{}:
41      Equal.trans(F.F64, F.nan_or(x, True{}), F.nan(), SF.pick(F.F64, True{}, F.nan(), x), {==}, Equal.sym(F.F64, SF.pick(F.F64, True{}, F.nan(), x), F.nan(), FR.pk_t(F.F64, F.nan(), x)))
42    case False{}:
43      Equal.trans(F.F64, F.nan_or(x, False{}), x, SF.pick(F.F64, False{}, F.nan(), x), {==}, Equal.sym(F.F64, SF.pick(F.F64, False{}, F.nan(), x), x, FR.pk_f(F.F64, F.nan(), x)))
44
45def nfit_mono_c(+a: Nat, +b: Nat, +x: Nat, +hab: {Nat.is_le(a, b) == True{} : Bool}, +h: {C.fits(b, x) == False{} : Bool}, +c: Bool, +hc: {C.fits(a, x) == c : Bool}) -> {c == False{} : Bool}:
46  match c:
47    case True{}:
48      Equal.trans(Bool, True{}, C.fits(b, x), False{}, Equal.sym(Bool, C.fits(b, x), True{}, SH.fits_mono(a, b, x, hab, hc)), h)
49    case False{}:
50      {==}
51
52def nfit_mono(+a: Nat, +b: Nat, +x: Nat, +hab: {Nat.is_le(a, b) == True{} : Bool}, +h: {C.fits(b, x) == False{} : Bool}) -> {C.fits(a, x) == False{} : Bool}:
53  nfit_mono_c(a, b, x, hab, h, C.fits(a, x), {==})
54
55def dm2(+l: Bool, +r: Bool) -> {Bool.or(Bool.not(r), Bool.not(l)) == Bool.not(Bool.and(l, r)) : Bool}:
56  match l r:
57    case True{} True{}:
58      {==}
59    case True{} False{}:
60      {==}
61    case False{} True{}:
62      {==}
63    case False{} False{}:
64      {==}
65
66def add_lt2(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_lt(Nat.add(a, a), Nat.add(b, b)) == True{} : Bool}:
67  +l1 = Equal.trans(Bool, Nat.is_lt(Nat.add(a, a), Nat.add(a, b)), Nat.is_lt(a, b), True{}, WW.lt_cancel_l(a, a, b), h)
68  +l2 = Equal.trans(Bool, Nat.is_lt(Nat.add(a, b), Nat.add(b, b)), Nat.is_lt(a, b), True{}, WW.lt_cancel_r(a, b, b), h)
69  N.lt_trans(Nat.add(a, a), Nat.add(a, b), Nat.add(b, b), l1, l2)
70
71def add_eq0(+a: Nat, +b: Nat) -> {Nat.is_eq(Nat.add(a, b), 0n) == Bool.and(Nat.is_eq(a, 0n), Nat.is_eq(b, 0n)) : Bool}:
72  match a:
73    case 0n:
74      {==}
75    case 1n+ +ap:
76      {==}
77
78def shl_v(+a: WU.U64, +k: Nat, +j: Nat, +hk: {Nat.is_lt(k, 64n) == True{} : Bool}, +hj: {Nat.is_le(Nat.add(k, j), 64n) == True{} : Bool}, +ha: {C.fits(j, SW.value(a)) == True{} : Bool}) -> {SW.value(X.shl(a, k)) == C.shift(k, SW.value(a)) : Nat}:
79  sv = SH.shl_value(a, k, hk)
80  +f = SH.fits_mono(Nat.add(k, j), 64n, C.shift(k, SW.value(a)), hj, Equal.trans(Bool, C.fits(Nat.add(k, j), C.shift(k, SW.value(a))), C.fits(j, SW.value(a)), True{}, RT.fits_sh(k, j, SW.value(a)), ha))
81  Equal.trans(Nat, SW.value(X.shl(a, k)), C.low(64n, C.shift(k, SW.value(a))), C.shift(k, SW.value(a)), sv, WW.low_fit(64n, C.shift(k, SW.value(a)), f))
82
83def orv_c(+l: U32, +h: U32, +b: Bool) -> {SW.value(X.or_bit(WU.U64{l, h}, b)) == SW.jam(SW.value(WU.U64{l, h}), SF.b2n(b)) : Nat}:
84  match b:
85    case True{}:
86      +s31 = C.shift(31n, v(h))
87      +e1 = Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, v(h))), v(U32.or(l, 1)), 1n+Nat.double(C.half(v(l))), SH.or1(l))
88      +eh = WW.half_dbl(v(l), s31)
89      +e2 = Equal.trans(Nat, Nat.add(1n+Nat.double(C.half(v(l))), C.shift(32n, v(h))), 1n+Nat.add(Nat.double(C.half(v(l))), Nat.double(s31)), 1n+Nat.double(C.half(SW.value(WU.U64{l, h}))), NA.add_assoc(1n, Nat.double(C.half(v(l))), Nat.double(s31)), Equal.trans(Nat, 1n+Nat.add(Nat.double(C.half(v(l))), Nat.double(s31)), 1n+Nat.double(Nat.add(C.half(v(l)), s31)), 1n+Nat.double(C.half(SW.value(WU.U64{l, h}))), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(Nat.double(C.half(v(l))), Nat.double(s31)), Nat.double(Nat.add(C.half(v(l)), s31)), Equal.sym(Nat, Nat.double(Nat.add(C.half(v(l)), s31)), Nat.add(Nat.double(C.half(v(l))), Nat.double(s31)), NA.double_add(C.half(v(l)), s31))), Equal.cong(Nat, Nat, z => 1n+Nat.double(z), Nat.add(C.half(v(l)), s31), C.half(SW.value(WU.U64{l, h})), Equal.sym(Nat, C.half(SW.value(WU.U64{l, h})), Nat.add(C.half(v(l)), s31), eh))))
90      +e3 = Equal.sym(Nat, SW.jam(SW.value(WU.U64{l, h}), 1n), 1n+Nat.double(C.half(SW.value(WU.U64{l, h}))), SH.jam1_k(SW.value(WU.U64{l, h}), Nat.mod(SW.value(WU.U64{l, h}), 2n), {==}, NR.dm_lt(1n, SW.value(WU.U64{l, h}))))
91      Equal.trans(Nat, Nat.add(v(U32.or(l, 1)), C.shift(32n, v(h))), Nat.add(1n+Nat.double(C.half(v(l))), C.shift(32n, v(h))), SW.jam(SW.value(WU.U64{l, h}), 1n), e1, Equal.trans(Nat, Nat.add(1n+Nat.double(C.half(v(l))), C.shift(32n, v(h))), 1n+Nat.double(C.half(SW.value(WU.U64{l, h}))), SW.jam(SW.value(WU.U64{l, h}), 1n), e2, e3))
92    case False{}:
93      Equal.trans(Nat, Nat.add(v(U32.or(l, 0)), C.shift(32n, v(h))), SW.value(WU.U64{l, h}), SW.jam(SW.value(WU.U64{l, h}), 0n), Equal.cong(U32, Nat, z => Nat.add(v(z), C.shift(32n, v(h))), U32.or(l, 0), l, SH.or0(l)), Equal.sym(Nat, SW.jam(SW.value(WU.U64{l, h}), 0n), SW.value(WU.U64{l, h}), SH.jam0_m(SW.value(WU.U64{l, h}), Nat.mod(SW.value(WU.U64{l, h}), 2n), {==}, NR.dm_lt(1n, SW.value(WU.U64{l, h})))))
94
95def orv(+a: WU.U64, +b: Bool) -> {SW.value(X.or_bit(a, b)) == SW.jam(SW.value(a), SF.b2n(b)) : Nat}:
96  match a:
97    case WU.U64{+l, +h}:
98      orv_c(l, h, b)
99
100def minz(+r: Nat) -> {Nat.min(r, 0n) == 0n : Nat}:
101  match r:
102    case 0n:
103      {==}
104    case 1n+ +rp:
105      {==}
106
107def jmin(+q: Nat, +r: Nat) -> {SW.jam(q, SF.b2n(Bool.not(Nat.is_eq(r, 0n)))) == SW.jam(q, r) : Nat}:
108  match r:
109    case 0n:
110      {==}
111    case 1n+ +rp:
112      Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(2n, Nat.div(q, 2n)), Nat.max(Nat.mod(q, 2n), z)), 1n, Nat.min(1n+rp, 1n), Equal.sym(Nat, 1n+Nat.min(rp, 0n), 1n, Equal.cong(Nat, Nat, z => 1n+z, Nat.min(rp, 0n), 0n, minz(rp))))
113
114def nlb(+s: Bool, +k: Nat, +m: Nat, +x: Nat, +hk: {C.fits(k, m) == False{} : Bool}, +c: Bool, +hc: {Nat.is_le(1n+k, M.bit_length(m)) == c : Bool}) -> {c == True{} : Bool}:
115  match c:
116    case True{}:
117      {==}
118    case False{}:
119      +h1 = N.lt_succ_le(M.bit_length(m), k, N.not_le_lt(1n+k, M.bit_length(m), hc))
120      NC.absurd_tf({False{} == True{} : Bool}, Equal.trans(Bool, False{}, C.fits(k, m), True{}, Equal.sym(Bool, C.fits(k, m), False{}, hk), SH.fits_mono(M.bit_length(m), k, m, h1, RT.bl_fit(m))))
121
122def nfit_bl(+k: Nat, +m: Nat, +hk: {C.fits(k, m) == False{} : Bool}) -> {Nat.is_le(1n+k, M.bit_length(m)) == True{} : Bool}:
123  nlb(False{}, k, m, 0n, hk, Nat.is_le(1n+k, M.bit_length(m)), {==})
124
125# the fraction field has 52 bits (from f64addf, so light roots need not import it)
126def hF(+xl: U32, +xh: U32) -> {C.fits(52n, SF.frac(F.Bits{xl, xh})) == True{} : Bool}:
127  WW.limbs_fit(32n, 20n, v(xl), C.low(20n, v(xh)), LW.vb(xl), WW.low_fits(20n, v(xh)))
128
129def nz_le(+n: Nat, +hz: {Nat.is_eq(n, 0n) == False{} : Bool}) -> {Nat.is_le(1n, n) == True{} : Bool}:
130  match n:
131    case 0n:
132      NC.absurd_tf({Nat.is_le(1n, 0n) == True{} : Bool}, Equal.sym(Bool, True{}, False{}, hz))
133    case 1n+ +np:
134      N.zero_le(np)
135
136# every U64 value fits 64 bits (u64laws.vb, without u64laws' imports)
137def vb64(+x: WU.U64) -> {C.fits(64n, SW.value(x)) == True{} : Bool}:
138  match x:
139    case WU.U64{+l, +h}:
140      WW.limbs_fit(32n, 32n, LW.v(l), LW.v(h), LW.vb(l), LW.vb(h))
141
142def true_ne_false(+h: {True{} == False{} : Bool}) -> Empty:
143  LW.true_ne_false(h)