comparisonScript.sml

1Theory comparison
2Ancestors
3  option pair string list arithmetic toto
4Libs
5  BasicProvers
6
7val _ = temp_tight_equality ();
8val every_case_tac = BasicProvers.EVERY_CASE_TAC;
9
10val comparison_distinct = TypeBase.distinct_of ``:ordering``
11val comparison_case_def = TypeBase.case_def_of ``:ordering``
12val comparison_nchotomy = TypeBase.nchotomy_of ``:ordering``
13Overload Less = ``LESS``
14Overload Equal = ``EQUAL``
15Overload Greater = ``GREATER``
16
17Definition good_cmp_def:
18good_cmp cmp <=>
19  (!x. cmp x x = Equal) /\
20  (!x y. cmp x y = Equal ==> cmp y x = Equal) /\
21  (!x y. cmp x y = Greater <=> cmp y x = Less) /\
22  (!x y z. cmp x y = Equal /\ cmp y z = Less ==> cmp x z = Less) /\
23  (!x y z. cmp x y = Less /\ cmp y z = Equal ==> cmp x z = Less) /\
24  (!x y z. cmp x y = Equal /\ cmp y z = Equal ==> cmp x z = Equal) /\
25  (!x y z. cmp x y = Less /\ cmp y z = Less ==> cmp x z = Less)
26End
27
28Theorem good_cmp_thm:
29 !cmp.
30  good_cmp cmp <=>
31  (!x. cmp x x = Equal) /\
32  (!x y z.
33    (cmp x y = Greater <=> cmp y x = Less) /\
34    (cmp x y = Less /\ cmp y z = Equal ==> cmp x z = Less) /\
35    (cmp x y = Less /\ cmp y z = Less ==> cmp x z = Less))
36Proof
37 rw [good_cmp_def] >>
38 metis_tac [comparison_distinct, comparison_nchotomy]
39QED
40
41Theorem cmp_thms = LIST_CONJ [comparison_distinct, comparison_case_def, comparison_nchotomy, good_cmp_def]
42
43Overload option_cmp = ``option_compare``
44Theorem option_cmp_def =
45  ternaryComparisonsTheory.option_compare_def
46
47Definition option_cmp2_def:
48  (option_cmp2 cmp NONE NONE = Equal) /\
49  (option_cmp2 cmp NONE (SOME x) = Greater) /\
50  (option_cmp2 cmp (SOME x) NONE = Less) /\
51  (option_cmp2 cmp (SOME x) (SOME y) = cmp x y)
52End
53
54Overload list_cmp = ``list_compare``
55val list_cmp_def = ternaryComparisonsTheory.list_compare_def
56val list_cmp_ind = ternaryComparisonsTheory.list_compare_ind
57
58Overload pair_cmp = ``pair_compare``
59Theorem pair_cmp_def =
60  PART_MATCH lhs ternaryComparisonsTheory.pair_compare_def
61     ``pair_cmp c1 c2 (FST x, SND x) (FST y, SND y)``
62     |> REWRITE_RULE [pairTheory.PAIR];
63
64Overload bool_cmp = ``bool_compare``
65Theorem bool_cmp_def =
66  ternaryComparisonsTheory.bool_compare_def
67
68Overload num_cmp = ``num_compare``
69Theorem num_cmp_def =
70  ternaryComparisonsTheory.num_compare_def
71
72Overload char_cmp = “char_compare”
73Theorem char_cmp_def = stringTheory.char_compare_def
74
75Overload string_cmp = “string_compare”
76Theorem string_cmp_def = stringTheory.string_compare_def
77(* relationship to toto *)
78
79Theorem TotOrder_imp_good_cmp:
80    !cmp. TotOrd cmp ==> good_cmp cmp
81Proof
82  rw[TotOrd,good_cmp_thm] >> metis_tac[]
83QED
84
85Overload invert[local] = ``ternaryComparisons$invert_comparison``
86
87Theorem TO_inv_invert:
88    !c. TotOrd c ==> TO_inv c = CURRY (invert o UNCURRY c)
89Proof
90  simp[FUN_EQ_THM,TO_inv] >> gen_tac >> strip_tac >>
91  map_every qx_gen_tac[`x`,`y`] >>
92  Cases_on`c x y`>>simp[]>>
93  fs[TotOrd] >> metis_tac[]
94QED
95
96Theorem option_cmp2_TO_inv:
97    !c. option_cmp2 c = TO_inv (option_cmp (TO_inv c))
98Proof
99  simp[FUN_EQ_THM,TO_inv] >>
100  gen_tac >> Cases >> Cases >>
101  simp[option_cmp2_def,option_cmp_def,TO_inv]
102QED
103
104Theorem list_cmp_ListOrd:
105    !c. TotOrd c ==> list_cmp c = ListOrd (TO c)
106Proof
107  simp[FUN_EQ_THM,PULL_FORALL] >>
108  ho_match_mp_tac list_cmp_ind >>
109  simp[list_cmp_def,ListOrd,TO_of_LinearOrder,
110       StrongLinearOrder_of_TO,TO_apto_TO_ID,listorder] >>
111  rw[] >>
112  fs[GSYM TO_apto_TO_ID,TotOrd] >>
113  BasicProvers.CASE_TAC >>
114  metis_tac[cmp_thms]
115QED
116
117Theorem TotOrd_list_cmp:
118    !c. TotOrd c ==> TotOrd (list_cmp c)
119Proof
120  srw_tac[][] >> imp_res_tac list_cmp_ListOrd >> simp[TO_ListOrd]
121QED
122
123Theorem pair_cmp_lexTO:
124    !R V. TotOrd R /\ TotOrd V ==> pair_cmp R V = R lexTO V
125Proof
126  simp[FUN_EQ_THM,lexTO_thm,pair_cmp_def,pairTheory.FORALL_PROD]
127QED
128
129Theorem num_cmp_numOrd:
130    num_cmp = numOrd
131Proof
132  simp[FUN_EQ_THM,num_cmp_def,numOrd,TO_of_LinearOrder]
133QED
134
135Theorem char_cmp_charOrd:
136    char_cmp = charOrd
137Proof
138  simp[FUN_EQ_THM,char_cmp_def,charOrd,num_cmp_numOrd]
139QED
140
141Theorem string_cmp_stringto:
142    string_cmp = apto stringto
143Proof
144  simp[FUN_EQ_THM,stringto] >>
145  Induct >- ( Cases >> simp[aplistoto,string_cmp_def,list_cmp_def] ) >>
146  gen_tac >> Cases >>
147  simp[aplistoto,string_cmp_def,list_cmp_def,apcharto_thm,char_cmp_charOrd] >>
148  BasicProvers.CASE_TAC >>
149  simp[MATCH_MP list_cmp_ListOrd TO_charOrd,listoto,charto] >>
150  rpt AP_THM_TAC >>
151  match_mp_tac (GSYM TO_apto_TO_IMP) >>
152  simp[TO_ListOrd]
153QED
154
155(* cmps are good *)
156
157Theorem option_cmp_good:
158 !cmp. good_cmp cmp ==> good_cmp (option_cmp cmp)
159Proof
160 rw [good_cmp_def] >>
161 Cases_on `x` >>
162 TRY (Cases_on `y`) >>
163 TRY (Cases_on `z`) >>
164 metis_tac [option_cmp_def, comparison_distinct]
165QED
166
167Theorem option_cmp2_good:
168 !cmp. good_cmp cmp ==> good_cmp (option_cmp2 cmp)
169Proof
170 rw [good_cmp_def] >>
171 Cases_on `x` >>
172 TRY (Cases_on `y`) >>
173 TRY (Cases_on `z`) >>
174 metis_tac [option_cmp2_def, comparison_distinct]
175QED
176
177Theorem list_cmp_good:
178 !cmp. good_cmp cmp ==> good_cmp (list_cmp cmp)
179Proof
180 simp [good_cmp_def] >>
181 rpt gen_tac >>
182 strip_tac >>
183 rpt conj_tac >>
184 Induct_on `x` >>
185 TRY (Cases_on `y`) >>
186 TRY (Cases_on `z`) >>
187 REWRITE_TAC [list_cmp_def] >>
188 rpt strip_tac >>
189 every_case_tac >>
190 metis_tac [list_cmp_def, comparison_distinct, comparison_case_def, comparison_nchotomy]
191QED
192
193Theorem pair_cmp_good:
194 !cmp1 cmp2. good_cmp cmp1 /\ good_cmp cmp2 ==> good_cmp (pair_cmp cmp1 cmp2)
195Proof
196 simp [good_cmp_def] >>
197 rpt gen_tac >>
198 strip_tac >>
199 rpt conj_tac >>
200 TRY (Cases_on `x`) >>
201 TRY (Cases_on `y`) >>
202 TRY (Cases_on `z`) >>
203 REWRITE_TAC [pair_cmp_def] >>
204 rpt strip_tac >>
205 every_case_tac >>
206 metis_tac [pair_cmp_def, comparison_distinct, comparison_case_def, comparison_nchotomy]
207QED
208
209Theorem bool_cmp_good[simp]:
210 good_cmp bool_cmp
211Proof
212 simp [good_cmp_def] >>
213 rpt conj_tac >>
214 TRY (Cases_on `x`) >>
215 TRY (Cases_on `y`) >>
216 TRY (Cases_on `z`) >>
217 REWRITE_TAC [bool_cmp_def] >>
218 every_case_tac >>
219 fs []
220QED
221
222Theorem num_cmp_good[simp]:
223 good_cmp num_cmp
224Proof
225 simp [good_cmp_def] >>
226 rpt conj_tac >>
227 TRY (Cases_on `x`) >>
228 TRY (Cases_on `y`) >>
229 TRY (Cases_on `z`) >>
230 REWRITE_TAC [num_cmp_def] >>
231 every_case_tac >>
232 full_simp_tac (srw_ss()++ARITH_ss) []
233QED
234
235Theorem char_cmp_good[simp]:
236 good_cmp char_cmp
237Proof
238 simp [good_cmp_def] >>
239 rpt conj_tac >>
240 TRY (Cases_on `x`) >>
241 TRY (Cases_on `y`) >>
242 TRY (Cases_on `z`) >>
243 REWRITE_TAC [char_cmp_def, num_cmp_def] >>
244 every_case_tac >>
245 full_simp_tac (srw_ss()++ARITH_ss) []
246QED
247
248Theorem string_cmp_good[simp]:
249 good_cmp string_cmp
250Proof
251 metis_tac [string_cmp_def, char_cmp_good, list_cmp_good]
252QED
253
254Theorem list_cmp_cong[defncong]:
255  !cmp l1 l2 cmp' l1' l2'.
256    l1 = l1' /\ l2 = l2' /\
257    (!x x'. MEM x l1' /\ MEM x' l2' ==> cmp x x' = cmp' x x')
258    ==>
259    list_cmp cmp l1 l2 = list_cmp cmp' l1' l2'
260Proof
261 ho_match_mp_tac list_cmp_ind >>
262 rw [list_cmp_def] >>
263 rw [list_cmp_def] >>
264 every_case_tac >>
265 rw []
266QED
267
268Theorem option_cmp_cong[defncong]:
269  !cmp v1 v2 cmp' v1' v2'.
270    v1 = v1' /\ v2 = v2' /\
271    (!x x'. v1' = SOME x /\ v2' = SOME x' ==> cmp x x' = cmp' x x') ==>
272    option_cmp cmp v1 v2 = option_cmp cmp' v1' v2'
273Proof
274 ho_match_mp_tac ternaryComparisonsTheory.option_compare_ind >>
275 rw [option_cmp_def] >>
276 rw [option_cmp_def]
277QED
278
279Theorem option_cmp2_cong[defncong]:
280  !cmp v1 v2 cmp' v1' v2'.
281    v1 = v1' /\ v2 = v2' /\
282    (!x x'. v1' = SOME x /\ v2' = SOME x' ==> cmp x x' = cmp' x x')
283    ==>
284    option_cmp2 cmp v1 v2 = option_cmp2 cmp' v1' v2'
285Proof
286  ho_match_mp_tac (fetch "-" "option_cmp2_ind") >>
287  rw [option_cmp2_def] >>
288  rw [option_cmp2_def]
289QED
290
291Theorem pair_cmp_cong[defncong]:
292  !cmp1 cmp2 v1 v2 cmp1' cmp2' v1' v2'.
293    v1 = v1' /\
294    v2 = v2' /\
295    (!a b c d. v1' = (a,b) /\ v2' = (c,d) ==> cmp1 a c = cmp1' a c) /\
296    (!a b c d. v1' = (a,b) /\ v2' = (c,d) ==> cmp2 b d = cmp2' b d)
297  ==>
298    pair_cmp cmp1 cmp2 v1 v2 = pair_cmp cmp1' cmp2' v1' v2'
299Proof simp [pair_cmp_def, pairTheory.FORALL_PROD]
300QED
301
302Theorem good_cmp_trans:
303 !cmp. good_cmp cmp ==> transitive (\ (k,v) (k',v'). cmp k k' = Less)
304Proof
305 rw [relationTheory.transitive_def] >>
306 Cases_on `x` >>
307 Cases_on `y` >>
308 Cases_on `z` >>
309 fs [] >>
310 metis_tac [cmp_thms]
311QED
312
313Theorem good_cmp_Less_trans:
314 !cmp. good_cmp cmp ==> transitive (\k k'. cmp k k' = Less)
315Proof
316 rw [relationTheory.transitive_def] >>
317 fs [] >>
318 metis_tac [cmp_thms]
319QED
320
321Theorem good_cmp_Less_irrefl_trans:
322 !cmp. good_cmp cmp ==> (irreflexive (\k k'. cmp k k' = Less) /\
323    transitive (\k k'. cmp k k' = Less))
324Proof
325 simp [good_cmp_Less_trans, relationTheory.irreflexive_def] >>
326 simp [cmp_thms]
327QED
328
329Theorem bool_cmp_antisym[simp]:
330 !x y. bool_cmp x y = Equal <=> x = y
331Proof
332 rw [] >>
333 Cases_on `x` >>
334 Cases_on `y` >>
335 rw [bool_cmp_def]
336QED
337
338Theorem num_cmp_antisym[simp]:
339 !x y. num_cmp x y = Equal <=> x = y
340Proof
341 rw [num_cmp_def]
342QED
343
344Theorem char_cmp_antisym[simp]:
345 !x y. char_cmp x y = Equal <=> x = y
346Proof
347 rw [char_cmp_def, num_cmp_antisym] >>
348 rw [ORD_11]
349QED
350
351Theorem list_cmp_antisym:
352 !cmp x y. (!x y. cmp x y = Equal <=> x = y) ==> (list_cmp cmp x y = Equal <=> x = y)
353Proof
354 ho_match_mp_tac list_cmp_ind >>
355 rw [list_cmp_def] >>
356 every_case_tac >>
357 rw [] >>
358 metis_tac [comparison_distinct]
359QED
360
361Theorem string_cmp_antisym[simp]:
362 !x y. string_cmp x y = Equal <=> x = y
363Proof
364 metis_tac [string_cmp_def, char_cmp_antisym, list_cmp_antisym]
365QED
366
367Theorem pair_cmp_antisym:
368 !cmp1 cmp2 x y.
369  (!x y. cmp1 x y = Equal <=> x = y) /\
370  (!x y. cmp2 x y = Equal <=> x = y)
371  ==>
372  (pair_cmp cmp1 cmp2 x y = Equal <=> x = y)
373Proof
374 Cases_on `x` >>
375 Cases_on `y` >>
376 rw [pair_cmp_def] >>
377 every_case_tac >>
378 rw [] >>
379 metis_tac [comparison_distinct]
380QED
381
382Theorem option_cmp_antisym:
383 !cmp x y.
384  (!x y. cmp x y = Equal <=> x = y)
385  ==>
386  (option_cmp cmp x y = Equal <=> x = y)
387Proof
388 Cases_on `x` >>
389 Cases_on `y` >>
390 rw [option_cmp_def] >>
391 every_case_tac >>
392 rw [] >>
393 metis_tac [comparison_distinct]
394QED
395
396Theorem option_cmp2_antisym:
397 !cmp x y.
398  (!x y. cmp x y = Equal <=> x = y)
399  ==>
400  (option_cmp2 cmp x y = Equal <=> x = y)
401Proof
402 Cases_on `x` >>
403 Cases_on `y` >>
404 rw [option_cmp2_def] >>
405 every_case_tac >>
406 rw [] >>
407 metis_tac [comparison_distinct]
408QED
409
410Definition resp_equiv_def:
411resp_equiv cmp f <=> !k1 k2 v. cmp k1 k2 = Equal ==> f k1 v = f k2 v
412End
413
414Definition resp_equiv2_def:
415resp_equiv2 cmp cmp2 f <=> (!k1 k2. cmp k1 k2 = Equal ==> cmp2 (f k1) (f k2) = Equal)
416End
417
418Definition equiv_inj_def:
419equiv_inj cmp cmp2 f <=> (!k1 k2. cmp2 (f k1) (f k2) = Equal ==> cmp k1 k2 = Equal)
420End
421
422Theorem antisym_resp_equiv:
423 !cmp f.
424  (!x y. cmp x y = Equal ==> x = y)
425  ==>
426  resp_equiv cmp f /\ !cmp2. good_cmp cmp2 ==> resp_equiv2 cmp cmp2 f
427Proof
428 rw [resp_equiv_def, resp_equiv2_def] >>
429 metis_tac [cmp_thms]
430QED
431
432Theorem list_cmp_equal_list_rel:
433 !cmp l1 l2.
434  list_cmp cmp l1 l2 = Equal <=> LIST_REL (\x y. cmp x y = Equal) l1 l2
435Proof
436 Induct_on `l1` >>
437 rw [] >>
438 Cases_on `l2` >>
439 fs [list_cmp_def] >>
440 every_case_tac >>
441 fs []
442QED
443
444Theorem TO_of_LinearOrder_LLEX:
445    !R. irreflexive R ==> (TO_of_LinearOrder (LLEX R) = list_cmp (TO_of_LinearOrder R))
446Proof
447  srw_tac[][relationTheory.irreflexive_def] >>
448  simp[FUN_EQ_THM] >>
449  Induct >- (
450    Cases >> simp[list_cmp_def,TO_of_LinearOrder] ) >>
451  gen_tac >> Cases >>
452  simp[list_cmp_def,TO_of_LinearOrder] >>
453  pop_assum(assume_tac o GSYM) >> simp[] >>
454  srw_tac[][TO_of_LinearOrder] >> full_simp_tac(srw_ss())[] >> rev_full_simp_tac(srw_ss())[]
455QED