1	import Base
2	import ../../spec/lib/order.bend as SO
3	import ./logic.bend as L
4	import ./nat.bend as N
5	import ./u32.bend as U
6	import ./lemmas/proofs/string_compare.bend as NM
7	
8	# Total-order laws for a static comparator ~cmp : A -> A -> Cmp, and their
9	# checked U32 (U32.cmp) and String (String.order) instances.
10	#   flip:    cmp(b, a) = flip(cmp(a, b))
11	#   antisym: cmp(a, b) = EQ  implies  a == b
12	#   trans:   a <= b and b <= c  implies  a <= c     (<= is cmp in {LT, EQ})
13	
14	def flipc(c: Cmp) -> Cmp:
15	  SO.flipc(c)
16	
17	def lec(c: Cmp) -> Bool:
18	  Cmp.is_le(c)
19	
20	# the laws are stated in spec/lib/order.bend
21	def Order(~A: Data, ~cmp: A -> A -> Cmp) -> Type:
22	  SO.Order(~A, ~cmp)
23	
24	def flip(~A: Data, ~cmp: A -> A -> Cmp, o: Order(~A, ~cmp), +a: A, +b: A) -> {cmp(b, a) == flipc(cmp(a, b)) : Cmp}:
25	  match o:
26	    case Tuple{f, r}:
27	      f(a, b)
28	
29	def antisym(~A: Data, ~cmp: A -> A -> Cmp, o: Order(~A, ~cmp), +a: A, +b: A, +e: {cmp(a, b) == EQ{} : Cmp}) -> {a == b : A}:
30	  match o:
31	    case Tuple{f, Tuple{s, t}}:
32	      s(a, b, e)
33	
34	def trans(~A: Data, ~cmp: A -> A -> Cmp, o: Order(~A, ~cmp), +a: A, +b: A, +c: A, +ab: {Cmp.is_le(cmp(a, b)) == True{} : Bool}, +bc: {Cmp.is_le(cmp(b, c)) == True{} : Bool}) -> {Cmp.is_le(cmp(a, c)) == True{} : Bool}:
35	  match o:
36	    case Tuple{f, Tuple{s, t}}:
37	      t(a, b, c, ab, bc)
38	
39	# ---- consequences ----
40	
41	def self_flip(+c: Cmp, +e: {c == flipc(c) : Cmp}) -> {c == EQ{} : Cmp}:
42	  match c:
43	    case LT{}:
44	      Empty.absurd({LT{} == EQ{} : Cmp}, L.cmp_lt_gt(e))
45	    case EQ{}:
46	      {==}
47	    case GT{}:
48	      Empty.absurd({GT{} == EQ{} : Cmp}, L.cmp_lt_gt(Equal.sym(Cmp, GT{}, LT{}, e)))
49	
50	def refl(~A: Data, ~cmp: A -> A -> Cmp, ~o: Order(~A, ~cmp), +a: A) -> {cmp(a, a) == EQ{} : Cmp}:
51	  self_flip(cmp(a, a), flip(~A, ~cmp, o, a, a))
52	
53	def le_refl(~A: Data, ~cmp: A -> A -> Cmp, ~o: Order(~A, ~cmp), +a: A) -> {Cmp.is_le(cmp(a, a)) == True{} : Bool}:
54	  %Equal.sym(Cmp, cmp(a, a), EQ{}, refl(~A, ~cmp, ~o, a)) : {Cmp.is_le(_) == True{} : Bool}
55	  {==}
56	
57	def not_le_flip(+c: Cmp, +e: {Cmp.is_le(c) == False{} : Bool}) -> {Cmp.is_le(flipc(c)) == True{} : Bool}:
58	  match c:
59	    case LT{}:
60	      Empty.absurd({Cmp.is_le(flipc(LT{})) == True{} : Bool}, L.true_false(e))
61	    case EQ{}:
62	      Empty.absurd({Cmp.is_le(flipc(EQ{})) == True{} : Bool}, L.true_false(e))
63	    case GT{}:
64	      {==}
65	
66	# Totality: not a <= b gives b <= a.
67	def total(~A: Data, ~cmp: A -> A -> Cmp, ~o: Order(~A, ~cmp), +a: A, +b: A, +e: {Cmp.is_le(cmp(a, b)) == False{} : Bool}) -> {Cmp.is_le(cmp(b, a)) == True{} : Bool}:
68	  %Equal.sym(Cmp, cmp(b, a), flipc(cmp(a, b)), flip(~A, ~cmp, o, a, b)) : {Cmp.is_le(_) == True{} : Bool}
69	  not_le_flip(cmp(a, b), e)
70	
71	def both_le_eq(+c: Cmp, +e1: {Cmp.is_le(c) == True{} : Bool}, +e2: {Cmp.is_le(flipc(c)) == True{} : Bool}) -> {c == EQ{} : Cmp}:
72	  match c:
73	    case LT{}:
74	      Empty.absurd({LT{} == EQ{} : Cmp}, L.false_true(e2))
75	    case EQ{}:
76	      {==}
77	    case GT{}:
78	      Empty.absurd({GT{} == EQ{} : Cmp}, L.false_true(e1))
79	
80	def le_antisym(~A: Data, ~cmp: A -> A -> Cmp, ~o: Order(~A, ~cmp), +a: A, +b: A, +ab: {Cmp.is_le(cmp(a, b)) == True{} : Bool}, +ba: {Cmp.is_le(cmp(b, a)) == True{} : Bool}) -> {a == b : A}:
81	  antisym(~A, ~cmp, o, a, b, both_le_eq(cmp(a, b), ab, L.subst(Cmp, c => {Cmp.is_le(c) == True{} : Bool}, cmp(b, a), flipc(cmp(a, b)), flip(~A, ~cmp, o, a, b), ba)))
82	
83	# ---- Nat comparison ----
84	
85	def nat_flip(+a: Nat, +b: Nat) -> {Nat.cmp(b, a) == flipc(Nat.cmp(a, b)) : Cmp}:
86	  match a b:
87	    case 0n 0n:
88	      {==}
89	    case 0n 1n+q:
90	      {==}
91	    case 1n+p 0n:
92	      {==}
93	    case 1n+p 1n+q:
94	      nat_flip(p, q)
95	
96	def nat_eq(+a: Nat, +b: Nat, +e: {Nat.cmp(a, b) == EQ{} : Cmp}) -> {a == b : Nat}:
97	  N.eq_from_is_eq(a, b, L.subst(Cmp, c => {Cmp.is_eq(c) == True{} : Bool}, EQ{}, Nat.cmp(a, b), Equal.sym(Cmp, Nat.cmp(a, b), EQ{}, e), {==}))
98	
99	# ---- U32 instance ----
100	
101	def u32_flip(+a: U32, +b: U32) -> {U32.cmp(b, a) == flipc(U32.cmp(a, b)) : Cmp}:
102	  %Equal.sym(Cmp, U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), U.u32_cmp(a, b)) : {U32.cmp(b, a) == flipc(_) : Cmp}
103	  %Equal.sym(Cmp, U32.cmp(b, a), Nat.cmp(U32.to_nat(b), U32.to_nat(a)), U.u32_cmp(b, a)) : {_ == flipc(Nat.cmp(U32.to_nat(a), U32.to_nat(b))) : Cmp}
104	  nat_flip(U32.to_nat(a), U32.to_nat(b))
105	
106	def u32_antisym(+a: U32, +b: U32, +e: {U32.cmp(a, b) == EQ{} : Cmp}) -> {a == b : U32}:
107	  U.injective(a, b, nat_eq(U32.to_nat(a), U32.to_nat(b), Equal.trans(Cmp, Nat.cmp(U32.to_nat(a), U32.to_nat(b)), U32.cmp(a, b), EQ{}, Equal.sym(Cmp, U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), U.u32_cmp(a, b)), e)))
108	
109	def u32_trans(+a: U32, +b: U32, +c: U32, +ab: {Cmp.is_le(U32.cmp(a, b)) == True{} : Bool}, +bc: {Cmp.is_le(U32.cmp(b, c)) == True{} : Bool}) -> {Cmp.is_le(U32.cmp(a, c)) == True{} : Bool}:
110	  %Equal.sym(Cmp, U32.cmp(a, c), Nat.cmp(U32.to_nat(a), U32.to_nat(c)), U.u32_cmp(a, c)) : {Cmp.is_le(_) == True{} : Bool}
111	  N.le_trans(U32.to_nat(a), U32.to_nat(b), U32.to_nat(c),
112	    L.subst(Cmp, x => {Cmp.is_le(x) == True{} : Bool}, U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), U.u32_cmp(a, b), ab),
113	    L.subst(Cmp, x => {Cmp.is_le(x) == True{} : Bool}, U32.cmp(b, c), Nat.cmp(U32.to_nat(b), U32.to_nat(c)), U.u32_cmp(b, c), bc))
114	
115	def u32_order() -> Order(~U32, ~U32.cmp):
116	  (u32_flip, (u32_antisym, u32_trans))
117	
118	def nat_trans(+a: Nat, +b: Nat, +c: Nat, +ab: {Cmp.is_le(Nat.cmp(a, b)) == True{} : Bool}, +bc: {Cmp.is_le(Nat.cmp(b, c)) == True{} : Bool}) -> {Cmp.is_le(Nat.cmp(a, c)) == True{} : Bool}:
119	  N.le_trans(a, b, c, ab, bc)
120	
121	def nat_order() -> Order(~Nat, ~Nat.cmp):
122	  (nat_flip, (nat_eq, nat_trans))
123	
124	# ---- String instance (String.order, lexicographic on character codes) ----
125	
126	def lex(c: Cmp, r: Cmp) -> Cmp:
127	  match c:
128	    case LT{}:
129	      LT{}
130	    case EQ{}:
131	      r
132	    case GT{}:
133	      GT{}
134	
135	def order_tag(+a: String, +b: String) -> {String.order(a, b) == NM.comparison_tag(String, String.cmp(a, b)) : Cmp}:
136	  %Equal.sym((String & String) & Cmp, String.cmp(a, b), ((a, b), NM.comparison_tag(String, String.cmp(a, b))), NM.string_comparison_shape(a, b)) : {Pair.snd(String & String, Cmp, _) == NM.comparison_tag(String, _) : Cmp}
137	  {==}
138	
139	def so_cons_c(+x: U32, +t1: String, +y: U32, +t2: String, +c: Cmp, +ec: {U32.cmp(x, y) == c : Cmp}) -> {String.order(SCon{Chr{x}, t1}, SCon{Chr{y}, t2}) == lex(c, String.order(t1, t2)) : Cmp}:
140	  match c:
141	    case LT{}:
142	      %Equal.sym(Cmp, U32.cmp(x, y), LT{}, ec) : {Pair.snd(String & String, Cmp, String.cmp.fin(t1, t2, ((Chr{x}, Chr{y}), _))) == LT{} : Cmp}
143	      {==}
144	    case GT{}:
145	      %Equal.sym(Cmp, U32.cmp(x, y), GT{}, ec) : {Pair.snd(String & String, Cmp, String.cmp.fin(t1, t2, ((Chr{x}, Chr{y}), _))) == GT{} : Cmp}
146	      {==}
147	    case EQ{}:
148	      %Equal.sym(Cmp, U32.cmp(x, y), EQ{}, ec) : {Pair.snd(String & String, Cmp, String.cmp.fin(t1, t2, ((Chr{x}, Chr{y}), _))) == String.order(t1, t2) : Cmp}
149	      %Equal.sym((String & String) & Cmp, String.cmp(t1, t2), ((t1, t2), NM.comparison_tag(String, String.cmp(t1, t2))), NM.string_comparison_shape(t1, t2)) : {Pair.snd(String & String, Cmp, String.cmp.rec(Chr{x}, Chr{y}, _)) == Pair.snd(String & String, Cmp, _) : Cmp}
150	      {==}
151	
152	def so_cons(+x: U32, +t1: String, +y: U32, +t2: String) -> {String.order(SCon{Chr{x}, t1}, SCon{Chr{y}, t2}) == lex(U32.cmp(x, y), String.order(t1, t2)) : Cmp}:
153	  so_cons_c(x, t1, y, t2, U32.cmp(x, y), {==})
154	
155	def flip_lex(+c: Cmp, +r: Cmp) -> {lex(flipc(c), flipc(r)) == flipc(lex(c, r)) : Cmp}:
156	  match c:
157	    case LT{}:
158	      {==}
159	    case EQ{}:
160	      {==}
161	    case GT{}:
162	      {==}
163	
164	def s_flip(+a: String, +b: String) -> {String.order(b, a) == flipc(String.order(a, b)) : Cmp}:
165	  match a b:
166	    case SNil{} SNil{}:
167	      {==}
168	    case SNil{} SCon{h, t}:
169	      {==}
170	    case SCon{h, t} SNil{}:
171	      {==}
172	    case SCon{Chr{+x}, +t1} SCon{Chr{+y}, +t2}:
173	      %Equal.sym(Cmp, String.order(SCon{Chr{y}, t2}, SCon{Chr{x}, t1}), lex(U32.cmp(y, x), String.order(t2, t1)), so_cons(y, t2, x, t1)) : {_ == flipc(String.order(SCon{Chr{x}, t1}, SCon{Chr{y}, t2})) : Cmp}
174	      %Equal.sym(Cmp, String.order(SCon{Chr{x}, t1}, SCon{Chr{y}, t2}), lex(U32.cmp(x, y), String.order(t1, t2)), so_cons(x, t1, y, t2)) : {lex(U32.cmp(y, x), String.order(t2, t1)) == flipc(_) : Cmp}
175	      %Equal.sym(Cmp, U32.cmp(y, x), flipc(U32.cmp(x, y)), u32_flip(x, y)) : {lex(_, String.order(t2, t1)) == flipc(lex(U32.cmp(x, y), String.order(t1, t2))) : Cmp}
176	      %Equal.sym(Cmp, String.order(t2, t1), flipc(String.order(t1, t2)), s_flip(t1, t2)) : {lex(flipc(U32.cmp(x, y)), _) == flipc(lex(U32.cmp(x, y), String.order(t1, t2))) : Cmp}
177	      flip_lex(U32.cmp(x, y), String.order(t1, t2))
178	
179	def s_antisym(+a: String, +b: String, +e: {String.order(a, b) == EQ{} : Cmp}) -> {a == b : String}:
180	  NM.string_equal_from_comparison(a, b, Equal.trans(Cmp, NM.comparison_tag(String, String.cmp(a, b)), String.order(a, b), EQ{}, Equal.sym(Cmp, String.order(a, b), NM.comparison_tag(String, String.cmp(a, b)), order_tag(a, b)), e))
181	
182	def lt_is(+c: Cmp, +e: {Cmp.is_lt(c) == True{} : Bool}) -> {c == LT{} : Cmp}:
183	  match c:
184	    case LT{}:
185	      {==}
186	    case EQ{}:
187	      Empty.absurd({EQ{} == LT{} : Cmp}, L.false_true(e))
188	    case GT{}:
189	      Empty.absurd({GT{} == LT{} : Cmp}, L.false_true(e))
190	
191	def u32_lt_le(+x: U32, +y: U32, +z: U32, +xy: {U32.cmp(x, y) == LT{} : Cmp}, +yz: {Cmp.is_le(U32.cmp(y, z)) == True{} : Bool}) -> {U32.cmp(x, z) == LT{} : Cmp}:
192	  lt_is(U32.cmp(x, z),
193	    L.subst(Cmp, k => {Cmp.is_lt(k) == True{} : Bool}, Nat.cmp(U32.to_nat(x), U32.to_nat(z)), U32.cmp(x, z), Equal.sym(Cmp, U32.cmp(x, z), Nat.cmp(U32.to_nat(x), U32.to_nat(z)), U.u32_cmp(x, z)),
194	      N.lt_le_trans(U32.to_nat(x), U32.to_nat(y), U32.to_nat(z),
195	        L.subst(Cmp, k => {Cmp.is_lt(k) == True{} : Bool}, LT{}, Nat.cmp(U32.to_nat(x), U32.to_nat(y)), Equal.trans(Cmp, LT{}, U32.cmp(x, y), Nat.cmp(U32.to_nat(x), U32.to_nat(y)), Equal.sym(Cmp, U32.cmp(x, y), LT{}, xy), U.u32_cmp(x, y)), {==}),
196	        L.subst(Cmp, k => {Cmp.is_le(k) == True{} : Bool}, U32.cmp(y, z), Nat.cmp(U32.to_nat(y), U32.to_nat(z)), U.u32_cmp(y, z), yz))))
197	
198	# The head-character case of transitivity, given the tails' statement.
199	def s_trans_heads(+x: U32, +y: U32, +z: U32, +o12: Cmp, +o23: Cmp, +o13: Cmp, +cxy: Cmp, +exy: {U32.cmp(x, y) == cxy : Cmp}, +cyz: Cmp, +eyz: {U32.cmp(y, z) == cyz : Cmp}, +ab: {Cmp.is_le(lex(cxy, o12)) == True{} : Bool}, +bc: {Cmp.is_le(lex(cyz, o23)) == True{} : Bool}, ih: @+ab2: {Cmp.is_le(o12) == True{} : Bool} -> @+bc2: {Cmp.is_le(o23) == True{} : Bool} -> {Cmp.is_le(o13) == True{} : Bool}) -> {Cmp.is_le(lex(U32.cmp(x, z), o13)) == True{} : Bool}:
200	  match cxy cyz:
201	    case GT{} _:
202	      Empty.absurd({Cmp.is_le(lex(U32.cmp(x, z), o13)) == True{} : Bool}, L.false_true(ab))
203	    case _ GT{}:
204	      Empty.absurd({Cmp.is_le(lex(U32.cmp(x, z), o13)) == True{} : Bool}, L.false_true(bc))
205	    case LT{} LT{}:
206	      %Equal.sym(Cmp, U32.cmp(x, z), LT{}, u32_lt_le(x, y, z, exy, L.subst(Cmp, k => {Cmp.is_le(k) == True{} : Bool}, LT{}, U32.cmp(y, z), Equal.sym(Cmp, U32.cmp(y, z), LT{}, eyz), {==}))) : {Cmp.is_le(lex(_, o13)) == True{} : Bool}
207	      {==}
208	    case LT{} EQ{}:
209	      %Equal.sym(Cmp, U32.cmp(x, z), LT{}, u32_lt_le(x, y, z, exy, L.subst(Cmp, k => {Cmp.is_le(k) == True{} : Bool}, EQ{}, U32.cmp(y, z), Equal.sym(Cmp, U32.cmp(y, z), EQ{}, eyz), {==}))) : {Cmp.is_le(lex(_, o13)) == True{} : Bool}
210	      {==}
211	    case EQ{} LT{}:
212	      %Equal.sym(U32, x, y, u32_antisym(x, y, exy)) : {Cmp.is_le(lex(U32.cmp(_, z), o13)) == True{} : Bool}
213	      %Equal.sym(Cmp, U32.cmp(y, z), LT{}, eyz) : {Cmp.is_le(lex(_, o13)) == True{} : Bool}
214	      {==}
215	    case EQ{} EQ{}:
216	      %Equal.sym(U32, x, y, u32_antisym(x, y, exy)) : {Cmp.is_le(lex(U32.cmp(_, z), o13)) == True{} : Bool}
217	      %Equal.sym(Cmp, U32.cmp(y, z), EQ{}, eyz) : {Cmp.is_le(lex(_, o13)) == True{} : Bool}
218	      ih(ab, bc)
219	
220	def s_trans(+a: String, +b: String, +c: String, +ab: {Cmp.is_le(String.order(a, b)) == True{} : Bool}, +bc: {Cmp.is_le(String.order(b, c)) == True{} : Bool}) -> {Cmp.is_le(String.order(a, c)) == True{} : Bool}:
221	  match a b c:
222	    case SNil{} _ SNil{}:
223	      {==}
224	    case SNil{} _ SCon{h, t}:
225	      {==}
226	    case SCon{h, t} SNil{} _:
227	      Empty.absurd({Cmp.is_le(String.order(SCon{h, t}, c)) == True{} : Bool}, L.false_true(ab))
228	    case SCon{h1, t1} SCon{h2, t2} SNil{}:
229	      Empty.absurd({Cmp.is_le(String.order(SCon{h1, t1}, SNil{})) == True{} : Bool}, L.false_true(bc))
230	    case SCon{Chr{+x}, +t1} SCon{Chr{+y}, +t2} SCon{Chr{+z}, +t3}:
231	      %Equal.sym(Cmp, String.order(SCon{Chr{x}, t1}, SCon{Chr{z}, t3}), lex(U32.cmp(x, z), String.order(t1, t3)), so_cons(x, t1, z, t3)) : {Cmp.is_le(_) == True{} : Bool}
232	      s_trans_heads(x, y, z, String.order(t1, t2), String.order(t2, t3), String.order(t1, t3), U32.cmp(x, y), {==}, U32.cmp(y, z), {==},
233	        L.subst(Cmp, k => {Cmp.is_le(k) == True{} : Bool}, String.order(SCon{Chr{x}, t1}, SCon{Chr{y}, t2}), lex(U32.cmp(x, y), String.order(t1, t2)), so_cons(x, t1, y, t2), ab),
234	        L.subst(Cmp, k => {Cmp.is_le(k) == True{} : Bool}, String.order(SCon{Chr{y}, t2}, SCon{Chr{z}, t3}), lex(U32.cmp(y, z), String.order(t2, t3)), so_cons(y, t2, z, t3), bc),
235	        ab2 => bc2 => s_trans(t1, t2, t3, ab2, bc2))
236	
237	def string_order() -> Order(~String, ~String.order):
238	  (s_flip, (s_antisym, s_trans))