proofs/math/typed/f64addg.bend

bend-collections-laws-math@1.0.0.0 · 160 lines · 21 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/src/math/f64.bend as F
5import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
6import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
7import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
8import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
9import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC
10import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
11
12# Scale and significand bookkeeping for Add.value: the spec's common-scale
13# operands of two finite doubles, and the order of an aligned pair.
14
15def posz(+n: Nat, +h: {Nat.is_le(1n, n) == True{} : Bool}) -> {Nat.is_eq(n, 0n) == False{} : Bool}:
16  match n:
17    case 0n:
18      NC.absurd_tf({Nat.is_eq(0n, 0n) == False{} : Bool}, h)
19    case 1n+ +np:
20      {==}
21
22def shmk(+a: Nat, +b: Nat, +x: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(C.shift(a, x), C.shift(b, x)) == True{} : Bool}:
23  +h0 = WW.shift_mono(a, x, C.shift(Nat.sub(b, a), x), WW.shift_ge(Nat.sub(b, a), x))
24  L.subst(Nat, z => {Nat.is_le(C.shift(a, x), z) == True{} : Bool}, C.shift(a, C.shift(Nat.sub(b, a), x)), C.shift(b, x), Equal.sym(Nat, C.shift(b, x), C.shift(a, C.shift(Nat.sub(b, a), x)), NC.sh_split(b, a, x, h)), h0)
25
26def f53(+one: Nat, +h1: {one == 1n : Nat}, +Fr: Nat, +hF: {C.fits(52n, Fr) == True{} : Bool}) -> {C.fits(53n, Nat.add(Fr, C.shift(52n, one))) == True{} : Bool}:
27  WW.limbs_fit(52n, 1n, Fr, one, hF, L.subst(Nat, z => {C.fits(1n, z) == True{} : Bool}, 1n, one, Equal.sym(Nat, one, 1n, h1), {==}))
28
29def v(+x: U32) -> Nat:
30  U32.to_nat(x)
31
32# the scale and significand of a finite double with exponent field e
33def xe(+e: Nat) -> Nat:
34  SF.pick(Nat, Nat.is_eq(e, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(e, SF.zb()), 1075n))
35
36def mt(+e: Nat, +F: Nat) -> Nat:
37  Nat.add(F, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(e, 0n)))))
38
39def xe_z(+e: Nat, +hz: {Nat.is_eq(e, 0n) == True{} : Bool}) -> {xe(e) == 1926n : Nat}:
40  Equal.cong(Bool, Nat, t => SF.pick(Nat, t, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(e, SF.zb()), 1075n)), Nat.is_eq(e, 0n), True{}, hz)
41
42def xe_n(+e: Nat, +hz: {Nat.is_eq(e, 0n) == False{} : Bool}) -> {xe(e) == Nat.add(1925n, e) : Nat}:
43  +e1 = Equal.cong(Bool, Nat, t => SF.pick(Nat, t, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(e, SF.zb()), 1075n)), Nat.is_eq(e, 0n), False{}, hz)
44  +e2 = Equal.cong(Nat, Nat, z => Nat.sub(z, 1075n), Nat.add(e, 3000n), Nat.add(3000n, e), NA.add_comm(e, 3000n))
45  Equal.trans(Nat, xe(e), Nat.sub(Nat.add(e, 3000n), 1075n), Nat.add(1925n, e), e1, Equal.trans(Nat, Nat.sub(Nat.add(e, 3000n), 1075n), Nat.sub(Nat.add(3000n, e), 1075n), Nat.add(1925n, e), e2, FR.sub_add_r(3000n, e, 1075n, {==})))
46
47def mt_z(+e: Nat, +F: Nat, +hz: {Nat.is_eq(e, 0n) == True{} : Bool}) -> {mt(e, F) == F : Nat}:
48  Equal.trans(Nat, mt(e, F), Nat.add(F, 0n), F, Equal.cong(Bool, Nat, t => Nat.add(F, C.shift(52n, SF.b2n(Bool.not(t)))), Nat.is_eq(e, 0n), True{}, hz), N.add_zero(F))
49
50def mt_n(+one: Nat, +h1: {one == 1n : Nat}, +e: Nat, +F: Nat, +hz: {Nat.is_eq(e, 0n) == False{} : Bool}) -> {mt(e, F) == Nat.add(F, C.shift(52n, one)) : Nat}:
51  +ec = Equal.trans(Nat, SF.b2n(Bool.not(Nat.is_eq(e, 0n))), 1n, one, Equal.cong(Bool, Nat, t => SF.b2n(Bool.not(t)), Nat.is_eq(e, 0n), False{}, hz), Equal.sym(Nat, one, 1n, h1))
52  Equal.cong(Nat, Nat, z => Nat.add(F, C.shift(52n, z)), SF.b2n(Bool.not(Nat.is_eq(e, 0n))), one, ec)
53
54def min_l(+a: Nat, +b: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.min(a, b) == a : Nat}:
55  match a b:
56    case 0n _:
57      {==}
58    case 1n+ +ap 0n:
59      NC.absurd_tf({Nat.min(1n+ap, 0n) == 1n+ap : Nat}, h)
60    case 1n+ +ap 1n+ +bp:
61      N.succ_cong(Nat.min(ap, bp), ap, min_l(ap, bp, h))
62
63def min_r(+a: Nat, +b: Nat, +h: {Nat.is_le(b, a) == True{} : Bool}) -> {Nat.min(a, b) == b : Nat}:
64  match a b:
65    case 0n 0n:
66      {==}
67    case 0n 1n+ +bp:
68      NC.absurd_tf({Nat.min(0n, 1n+bp) == 1n+bp : Nat}, h)
69    case 1n+ +ap 0n:
70      {==}
71    case 1n+ +ap 1n+ +bp:
72      N.succ_cong(Nat.min(ap, bp), bp, min_r(ap, bp, h))
73
74def sub_kk(+k: Nat, +a: Nat, +b: Nat) -> {Nat.sub(Nat.add(k, a), Nat.add(k, b)) == Nat.sub(a, b) : Nat}:
75  match k:
76    case 0n:
77      {==}
78    case 1n+ +kp:
79      sub_kk(kp, a, b)
80
81def sub_le(+a: Nat, +b: Nat) -> {Nat.is_le(Nat.sub(a, b), a) == True{} : Bool}:
82  match a b:
83    case 0n 0n:
84      {==}
85    case 0n 1n+ +bp:
86      {==}
87    case 1n+ +ap 0n:
88      N.le_refl(1n+ap)
89    case 1n+ +ap 1n+ +bp:
90      N.le_trans(Nat.sub(ap, bp), ap, 1n+ap, sub_le(ap, bp), N.le_succ(ap))
91
92def pred_eq(+n: Nat, +hz: {Nat.is_eq(n, 0n) == False{} : Bool}) -> {1n+N.pred(n) == n : Nat}:
93  match n:
94    case 0n:
95      NC.absurd_tf({1n+N.pred(0n) == 0n : Nat}, Equal.sym(Bool, True{}, False{}, hz))
96    case 1n+ +np:
97      {==}
98
99# the sign of a difference of opposite signs
100def sgn(+sa: Bool, +sb: Bool, +h: {Bool.not(Bool.xor(sa, sb)) == False{} : Bool}) -> {Bool.not(sa) == sb : Bool}:
101  match sa sb:
102    case True{} True{}:
103      NC.absurd_tf({False{} == True{} : Bool}, Equal.sym(Bool, True{}, False{}, h))
104    case True{} False{}:
105      {==}
106    case False{} True{}:
107      {==}
108    case False{} False{}:
109      NC.absurd_tf({True{} == False{} : Bool}, Equal.sym(Bool, True{}, False{}, h))
110
111def zero_v(+s: Bool) -> {F.zero(s) == SF.zero(s) : F.F64}:
112  match s:
113    case True{}:
114      {==}
115    case False{}:
116      {==}
117
118def rca(+s: Bool, +a: Nat, +a2: Nat, +ha: {a == a2 : Nat}, +k: Nat, +k2: Nat, +hk: {k == k2 : Nat}, +m: Nat, +m2: Nat, +hm: {m == m2 : Nat}, +x: Nat, +x2: Nat, +hx: {x == x2 : Nat}) -> {SF.round(s, Nat.add(a, C.shift(k, m)), x) == SF.round(s, Nat.add(a2, C.shift(k2, m2)), x2) : F.F64}:
119  +e1 = L.subst(Nat, z => {SF.round(s, Nat.add(a, C.shift(k, m)), x) == SF.round(s, Nat.add(z, C.shift(k, m)), x) : F.F64}, a, a2, ha, {==})
120  +e2 = L.subst(Nat, z => {SF.round(s, Nat.add(a, C.shift(k, m)), x) == SF.round(s, Nat.add(a2, C.shift(z, m)), x) : F.F64}, k, k2, hk, e1)
121  +e3 = L.subst(Nat, z => {SF.round(s, Nat.add(a, C.shift(k, m)), x) == SF.round(s, Nat.add(a2, C.shift(k2, z)), x) : F.F64}, m, m2, hm, e2)
122  L.subst(Nat, z => {SF.round(s, Nat.add(a, C.shift(k, m)), x) == SF.round(s, Nat.add(a2, C.shift(k2, m2)), z) : F.F64}, x, x2, hx, e3)
123
124def rcs(+s: Bool, +a: Nat, +a2: Nat, +ha: {a == a2 : Nat}, +k: Nat, +k2: Nat, +hk: {k == k2 : Nat}, +m: Nat, +m2: Nat, +hm: {m == m2 : Nat}, +x: Nat, +x2: Nat, +hx: {x == x2 : Nat}) -> {SF.round(s, Nat.sub(C.shift(k, m), a), x) == SF.round(s, Nat.sub(C.shift(k2, m2), a2), x2) : F.F64}:
125  +e1 = L.subst(Nat, z => {SF.round(s, Nat.sub(C.shift(k, m), a), x) == SF.round(s, Nat.sub(C.shift(k, m), z), x) : F.F64}, a, a2, ha, {==})
126  +e2 = L.subst(Nat, z => {SF.round(s, Nat.sub(C.shift(k, m), a), x) == SF.round(s, Nat.sub(C.shift(z, m), a2), x) : F.F64}, k, k2, hk, e1)
127  +e3 = L.subst(Nat, z => {SF.round(s, Nat.sub(C.shift(k, m), a), x) == SF.round(s, Nat.sub(C.shift(k2, z), a2), x) : F.F64}, m, m2, hm, e2)
128  L.subst(Nat, z => {SF.round(s, Nat.sub(C.shift(k, m), a), x) == SF.round(s, Nat.sub(C.shift(k2, m2), a2), z) : F.F64}, x, x2, hx, e3)
129
130def bigcmp_c(+one: Nat, +h1: {one == 1n : Nat}, +el: Nat, +es: Nat, +Fl: Nat, +Fs: Nat, +hFl: {C.fits(52n, Fl) == True{} : Bool}, +hFs: {C.fits(52n, Fs) == True{} : Bool}, +hlt: {Nat.is_lt(es, el) == True{} : Bool}, +z: Bool, +hz: {Nat.is_eq(es, 0n) == z : Bool}) -> {Nat.is_lt(mt(es, Fs), C.shift(Nat.sub(xe(el), xe(es)), mt(el, Fl))) == True{} : Bool}:
131  match z:
132    case True{}:
133      +hl1 = N.lt_succ_le_succ(es, el, hlt)
134      +hel = posz(el, N.le_trans(1n, 1n+es, el, N.zero_le(es), hl1))
135      +ml = mt_n(one, h1, el, Fl, hel)
136      +hPl = L.subst(Nat, w => {Nat.is_le(C.shift(52n, one), w) == True{} : Bool}, Nat.add(C.shift(52n, one), Fl), Nat.add(Fl, C.shift(52n, one)), NA.add_comm(C.shift(52n, one), Fl), N.le_add_right(C.shift(52n, one), Fl))
137      +hPm = L.subst(Nat, w => {Nat.is_le(C.shift(52n, one), w) == True{} : Bool}, Nat.add(Fl, C.shift(52n, one)), mt(el, Fl), Equal.sym(Nat, mt(el, Fl), Nat.add(Fl, C.shift(52n, one)), ml), hPl)
138      +ms = mt_z(es, Fs, hz)
139      +l0 = Equal.trans(Bool, Nat.is_lt(Fs, C.shift(52n, one)), C.fits(52n, Fs), True{}, FR.lt_fit(52n, one, h1, Fs), hFs)
140      +l1 = N.lt_le_trans(Fs, C.shift(52n, one), C.shift(Nat.sub(xe(el), xe(es)), mt(el, Fl)), l0, N.le_trans(C.shift(52n, one), mt(el, Fl), C.shift(Nat.sub(xe(el), xe(es)), mt(el, Fl)), hPm, WW.shift_ge(Nat.sub(xe(el), xe(es)), mt(el, Fl))))
141      L.subst(Nat, w => {Nat.is_lt(w, C.shift(Nat.sub(xe(el), xe(es)), mt(el, Fl))) == True{} : Bool}, Fs, mt(es, Fs), Equal.sym(Nat, mt(es, Fs), Fs, ms), l1)
142    case False{}:
143      +hl1 = N.lt_succ_le_succ(es, el, hlt)
144      +hel = posz(el, N.le_trans(1n, 1n+es, el, N.zero_le(es), hl1))
145      +ml = mt_n(one, h1, el, Fl, hel)
146      +hPl = L.subst(Nat, w => {Nat.is_le(C.shift(52n, one), w) == True{} : Bool}, Nat.add(C.shift(52n, one), Fl), Nat.add(Fl, C.shift(52n, one)), NA.add_comm(C.shift(52n, one), Fl), N.le_add_right(C.shift(52n, one), Fl))
147      +hPm = L.subst(Nat, w => {Nat.is_le(C.shift(52n, one), w) == True{} : Bool}, Nat.add(Fl, C.shift(52n, one)), mt(el, Fl), Equal.sym(Nat, mt(el, Fl), Nat.add(Fl, C.shift(52n, one)), ml), hPl)
148      +ms = mt_n(one, h1, es, Fs, hz)
149      +xs = xe_n(es, hz)
150      +xl = xe_n(el, hel)
151      +ed = Equal.trans(Nat, Nat.sub(xe(el), xe(es)), Nat.sub(Nat.add(1925n, el), Nat.add(1925n, es)), Nat.sub(el, es), Equal.trans(Nat, Nat.sub(xe(el), xe(es)), Nat.sub(Nat.add(1925n, el), xe(es)), Nat.sub(Nat.add(1925n, el), Nat.add(1925n, es)), Equal.cong(Nat, Nat, w => Nat.sub(w, xe(es)), xe(el), Nat.add(1925n, el), xl), Equal.cong(Nat, Nat, w => Nat.sub(Nat.add(1925n, el), w), xe(es), Nat.add(1925n, es), xs)), sub_kk(1925n, el, es))
152      +hd = L.subst(Nat, w => {Nat.is_le(1n, w) == True{} : Bool}, Nat.sub(el, es), Nat.sub(xe(el), xe(es)), Equal.sym(Nat, Nat.sub(xe(el), xe(es)), Nat.sub(el, es), ed), FR.lt_sub_pos(es, el, hlt))
153      +l0 = Equal.trans(Bool, Nat.is_lt(Nat.add(Fs, C.shift(52n, one)), C.shift(53n, one)), C.fits(53n, Nat.add(Fs, C.shift(52n, one))), True{}, FR.lt_fit(53n, one, h1, Nat.add(Fs, C.shift(52n, one))), f53(one, h1, Fs, hFs))
154      +l2 = N.le_trans(C.shift(1n, C.shift(52n, one)), C.shift(1n, mt(el, Fl)), C.shift(Nat.sub(xe(el), xe(es)), mt(el, Fl)), WW.shift_mono(1n, C.shift(52n, one), mt(el, Fl), hPm), shmk(1n, Nat.sub(xe(el), xe(es)), mt(el, Fl), hd))
155      +l1 = N.lt_le_trans(Nat.add(Fs, C.shift(52n, one)), C.shift(53n, one), C.shift(Nat.sub(xe(el), xe(es)), mt(el, Fl)), l0, l2)
156      L.subst(Nat, w => {Nat.is_lt(w, C.shift(Nat.sub(xe(el), xe(es)), mt(el, Fl))) == True{} : Bool}, Nat.add(Fs, C.shift(52n, one)), mt(es, Fs), Equal.sym(Nat, mt(es, Fs), Nat.add(Fs, C.shift(52n, one)), ms), l1)
157
158def bigcmp(+one: Nat, +h1: {one == 1n : Nat}, +el: Nat, +es: Nat, +Fl: Nat, +Fs: Nat, +hFl: {C.fits(52n, Fl) == True{} : Bool}, +hFs: {C.fits(52n, Fs) == True{} : Bool}, +hlt: {Nat.is_lt(es, el) == True{} : Bool}) -> {Nat.cmp(mt(es, Fs), C.shift(Nat.sub(xe(el), xe(es)), mt(el, Fl))) == LT{} : Cmp}:
159  NC.cmp_lt(mt(es, Fs), C.shift(Nat.sub(xe(el), xe(es)), mt(el, Fl)), bigcmp_c(one, h1, el, es, Fl, Fs, hFl, hFs, hlt, Nat.is_eq(es, 0n), {==}))
160