1	import Base
2	import ../../../spec/lib/common.bend as C
3	import ../../../spec/math/f64.bend as SF
4	import ../../../src/math/f64.bend as F
5	import ../../lib/nat.bend as N
6	import ../../lib/logic.bend as L
7	import ../../lib/lemmas/proofs/nat_algebra.bend as NA
8	import ./width.bend as WW
9	import ./natcmp.bend as NC
10	import ./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	
15	def 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	
22	def 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	
26	def 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	
29	def v(+x: U32) -> Nat:
30	  U32.to_nat(x)
31	
32	# the scale and significand of a finite double with exponent field e
33	def 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	
36	def mt(+e: Nat, +F: Nat) -> Nat:
37	  Nat.add(F, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(e, 0n)))))
38	
39	def 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	
42	def 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	
47	def 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	
50	def 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	
54	def 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	
63	def 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	
74	def 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	
81	def 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	
92	def 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
100	def 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	
111	def zero_v(+s: Bool) -> {F.zero(s) == SF.zero(s) : F.F64}:
112	  match s:
113	    case True{}:
114	      {==}
115	    case False{}:
116	      {==}
117	
118	def 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	
124	def 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	
130	def 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	
158	def 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