1	import Base
2	import ../../../spec/lib/common.bend as C
3	import ../../../spec/math/f64.bend as SF
4	import ../../lib/nat.bend as N
5	import ../../lib/logic.bend as L
6	import ../../lib/lemmas/proofs/nat_algebra.bend as NA
7	import ./width.bend as WW
8	import ./u32laws.bend as LW
9	
10	# Comparisons of naturals (Nat.cmp), lexicographic pairs and common scales:
11	# the order facts behind the f64 comparison and rounding proofs.
12	
13	def absurd_tf(-T: Type, +h: {False{} == True{} : Bool}) -> T:
14	  Empty.absurd(T, LW.true_ne_false(Equal.sym(Bool, False{}, True{}, h)))
15	
16	def lex(c: Cmp, d: Cmp) -> Cmp:
17	  match c:
18	    case LT{}:
19	      LT{}
20	    case EQ{}:
21	      d
22	    case GT{}:
23	      GT{}
24	
25	def cmp_dbl(+a: Nat, +b: Nat) -> {Nat.cmp(Nat.double(a), Nat.double(b)) == Nat.cmp(a, b) : Cmp}:
26	  match a b:
27	    case 0n 0n:
28	      {==}
29	    case 0n 1n+ +bp:
30	      {==}
31	    case 1n+ +ap 0n:
32	      {==}
33	    case 1n+ +ap 1n+ +bp:
34	      cmp_dbl(ap, bp)
35	
36	def cmp_shift(+k: Nat, +a: Nat, +b: Nat) -> {Nat.cmp(C.shift(k, a), C.shift(k, b)) == Nat.cmp(a, b) : Cmp}:
37	  match k:
38	    case 0n:
39	      {==}
40	    case 1n+ +p:
41	      Equal.trans(Cmp, Nat.cmp(Nat.double(C.shift(p, a)), Nat.double(C.shift(p, b))), Nat.cmp(C.shift(p, a), C.shift(p, b)), Nat.cmp(a, b), cmp_dbl(C.shift(p, a), C.shift(p, b)), cmp_shift(p, a, b))
42	
43	def cmp_add(+d: Nat, +a: Nat, +b: Nat) -> {Nat.cmp(Nat.add(d, a), Nat.add(d, b)) == Nat.cmp(a, b) : Cmp}:
44	  match d:
45	    case 0n:
46	      {==}
47	    case 1n+ +dp:
48	      cmp_add(dp, a, b)
49	
50	def cmp_addr(+a: Nat, +b: Nat, +s: Nat) -> {Nat.cmp(Nat.add(a, s), Nat.add(b, s)) == Nat.cmp(a, b) : Cmp}:
51	  +e1 = Equal.cong(Nat, Cmp, z => Nat.cmp(z, Nat.add(b, s)), Nat.add(a, s), Nat.add(s, a), NA.add_comm(a, s))
52	  +e2 = Equal.cong(Nat, Cmp, z => Nat.cmp(Nat.add(s, a), z), Nat.add(b, s), Nat.add(s, b), NA.add_comm(b, s))
53	  Equal.trans(Cmp, Nat.cmp(Nat.add(a, s), Nat.add(b, s)), Nat.cmp(Nat.add(s, a), Nat.add(b, s)), Nat.cmp(a, b), e1, Equal.trans(Cmp, Nat.cmp(Nat.add(s, a), Nat.add(b, s)), Nat.cmp(Nat.add(s, a), Nat.add(s, b)), Nat.cmp(a, b), e2, cmp_add(s, a, b)))
54	
55	def lt_c(+c: Cmp, +h: {Cmp.is_lt(c) == True{} : Bool}) -> {c == LT{} : Cmp}:
56	  match c:
57	    case LT{}:
58	      {==}
59	    case EQ{}:
60	      absurd_tf({EQ{} == LT{} : Cmp}, h)
61	    case GT{}:
62	      absurd_tf({GT{} == LT{} : Cmp}, h)
63	
64	def eq_c(+c: Cmp, +h: {Cmp.is_eq(c) == True{} : Bool}) -> {c == EQ{} : Cmp}:
65	  match c:
66	    case LT{}:
67	      absurd_tf({LT{} == EQ{} : Cmp}, h)
68	    case EQ{}:
69	      {==}
70	    case GT{}:
71	      absurd_tf({GT{} == EQ{} : Cmp}, h)
72	
73	def cmp_lt(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.cmp(a, b) == LT{} : Cmp}:
74	  lt_c(Nat.cmp(a, b), h)
75	
76	def cmp_flip(+a: Nat, +b: Nat) -> {SF.flip(Nat.cmp(a, b)) == Nat.cmp(b, a) : Cmp}:
77	  match a b:
78	    case 0n 0n:
79	      {==}
80	    case 0n 1n+ +bp:
81	      {==}
82	    case 1n+ +ap 0n:
83	      {==}
84	    case 1n+ +ap 1n+ +bp:
85	      cmp_flip(ap, bp)
86	
87	def cmp_gt(+a: Nat, +b: Nat, +h: {Nat.is_lt(b, a) == True{} : Bool}) -> {Nat.cmp(a, b) == GT{} : Cmp}:
88	  Equal.trans(Cmp, Nat.cmp(a, b), SF.flip(Nat.cmp(b, a)), GT{}, Equal.sym(Cmp, SF.flip(Nat.cmp(b, a)), Nat.cmp(a, b), cmp_flip(b, a)), Equal.cong(Cmp, Cmp, t => SF.flip(t), Nat.cmp(b, a), LT{}, cmp_lt(b, a, h)))
89	
90	def cmp_refl(+a: Nat) -> {Nat.cmp(a, a) == EQ{} : Cmp}:
91	  eq_c(Nat.cmp(a, a), N.is_eq_refl(a))
92	
93	def eq_of_cmp(+a: Nat, +b: Nat, +h: {Nat.cmp(a, b) == EQ{} : Cmp}) -> {a == b : Nat}:
94	  N.eq_from_is_eq(a, b, Equal.cong(Cmp, Bool, t => Cmp.is_eq(t), Nat.cmp(a, b), EQ{}, h))
95	
96	def lt_of_cmp(+a: Nat, +b: Nat, +h: {Nat.cmp(a, b) == LT{} : Cmp}) -> {Nat.is_lt(a, b) == True{} : Bool}:
97	  Equal.cong(Cmp, Bool, t => Cmp.is_lt(t), Nat.cmp(a, b), LT{}, h)
98	
99	def lt_of_gt(+a: Nat, +b: Nat, +h: {Nat.cmp(a, b) == GT{} : Cmp}) -> {Nat.is_lt(b, a) == True{} : Bool}:
100	  lt_of_cmp(b, a, Equal.trans(Cmp, Nat.cmp(b, a), SF.flip(Nat.cmp(a, b)), LT{}, Equal.sym(Cmp, SF.flip(Nat.cmp(a, b)), Nat.cmp(b, a), cmp_flip(a, b)), Equal.cong(Cmp, Cmp, t => SF.flip(t), Nat.cmp(a, b), GT{}, h)))
101	
102	# two limbs compare lexicographically
103	def cl_c(+k: Nat, +x1: Nat, +y1: Nat, +x2: Nat, +y2: Nat, +hx1: {C.fits(k, x1) == True{} : Bool}, +hx2: {C.fits(k, x2) == True{} : Bool}, +c: Cmp, +hc: {Nat.cmp(y1, y2) == c : Cmp}) -> {Nat.cmp(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))) == lex(c, Nat.cmp(x1, x2)) : Cmp}:
104	  match c:
105	    case LT{}:
106	      cmp_lt(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2)), WW.lt_hi(k, x1, y1, x2, y2, hx1, lt_of_cmp(y1, y2, hc)))
107	    case GT{}:
108	      cmp_gt(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2)), WW.lt_hi(k, x2, y2, x1, y1, hx2, lt_of_gt(y1, y2, hc)))
109	    case EQ{}:
110	      L.subst(Nat, z => {Nat.cmp(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, z))) == Nat.cmp(x1, x2) : Cmp}, y1, y2, eq_of_cmp(y1, y2, hc), cmp_addr(x1, x2, C.shift(k, y1)))
111	
112	def cmp_limbs(+k: Nat, +x1: Nat, +y1: Nat, +x2: Nat, +y2: Nat, +hx1: {C.fits(k, x1) == True{} : Bool}, +hx2: {C.fits(k, x2) == True{} : Bool}) -> {Nat.cmp(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2))) == lex(Nat.cmp(y1, y2), Nat.cmp(x1, x2)) : Cmp}:
113	  cl_c(k, x1, y1, x2, y2, hx1, hx2, Nat.cmp(y1, y2), {==})
114	
115	def min_le_l(+a: Nat, +b: Nat) -> {Nat.is_le(Nat.min(a, b), a) == True{} : Bool}:
116	  match a b:
117	    case 0n _:
118	      {==}
119	    case 1n+ +ap 0n:
120	      {==}
121	    case 1n+ +ap 1n+ +bp:
122	      min_le_l(ap, bp)
123	
124	def min_le_r(+a: Nat, +b: Nat) -> {Nat.is_le(Nat.min(a, b), b) == True{} : Bool}:
125	  match a b:
126	    case 0n _:
127	      N.zero_le(b)
128	    case 1n+ +ap 0n:
129	      {==}
130	    case 1n+ +ap 1n+ +bp:
131	      min_le_r(ap, bp)
132	
133	# shift(a, p) = shift(m, shift(a - m, p)) for m <= a
134	def sh_split(+a: Nat, +m: Nat, +p: Nat, +h: {Nat.is_le(m, a) == True{} : Bool}) -> {C.shift(a, p) == C.shift(m, C.shift(Nat.sub(a, m), p)) : Nat}:
135	  Equal.trans(Nat, C.shift(a, p), C.shift(Nat.add(m, Nat.sub(a, m)), p), C.shift(m, C.shift(Nat.sub(a, m), p)), Equal.cong(Nat, Nat, z => C.shift(z, p), a, Nat.add(m, Nat.sub(a, m)), Equal.sym(Nat, Nat.add(m, Nat.sub(a, m)), a, N.sub_add(a, m, h))), WW.shift_comp(m, Nat.sub(a, m), p))
136	
137	# a common scale 2^min cancels
138	def cmp_min(+a: Nat, +b: Nat, +p: Nat, +q: Nat) -> {Nat.cmp(C.shift(Nat.sub(a, Nat.min(a, b)), p), C.shift(Nat.sub(b, Nat.min(a, b)), q)) == Nat.cmp(C.shift(a, p), C.shift(b, q)) : Cmp}:
139	  +m = Nat.min(a, b)
140	  +X0 = C.shift(Nat.sub(a, m), p)
141	  +Y0 = C.shift(Nat.sub(b, m), q)
142	  +e1 = Equal.cong(Nat, Cmp, z => Nat.cmp(z, C.shift(b, q)), C.shift(a, p), C.shift(m, X0), sh_split(a, m, p, min_le_l(a, b)))
143	  +e2 = Equal.cong(Nat, Cmp, z => Nat.cmp(C.shift(m, X0), z), C.shift(b, q), C.shift(m, Y0), sh_split(b, m, q, min_le_r(a, b)))
144	  Equal.sym(Cmp, Nat.cmp(C.shift(a, p), C.shift(b, q)), Nat.cmp(X0, Y0), Equal.trans(Cmp, Nat.cmp(C.shift(a, p), C.shift(b, q)), Nat.cmp(C.shift(m, X0), C.shift(b, q)), Nat.cmp(X0, Y0), e1, Equal.trans(Cmp, Nat.cmp(C.shift(m, X0), C.shift(b, q)), Nat.cmp(C.shift(m, X0), C.shift(m, Y0)), Nat.cmp(X0, Y0), e2, cmp_shift(m, X0, Y0))))
145