mergesortScript.sml
1Theory mergesort
2Ancestors
3 pred_set arithmetic list rich_list option pair relation sorting
4Libs
5 BasicProvers permLib
6
7val _ = temp_tight_equality ();
8
9val every_case_tac = BasicProvers.EVERY_CASE_TAC;
10
11Theorem last_reverse[local]:
12 !l. l <> [] ==> LAST (REVERSE l) = HD l
13Proof
14 Induct_on `l` >>
15 srw_tac[][]
16QED
17
18Theorem mem_sorted_append[local]:
19 !R l1 l2 x y.
20 transitive R /\
21 SORTED R (l1 ++ l2) /\
22 MEM x l1 /\
23 MEM y l2
24 ==>
25 R x y
26Proof
27 Induct_on `l1` >>
28 srw_tac[][] >>
29 REV_FULL_SIMP_TAC (srw_ss()) [SORTED_EQ] >>
30 metis_tac []
31QED
32
33Definition stable_def:
34stable R l1 l2 =
35 !p. (!x y. p x /\ p y ==> R x y) ==> FILTER p l1 = FILTER p l2
36End
37
38Definition sort2_def:
39sort2 R x y =
40 if R x y then
41 [x;y]
42 else
43 [y;x]
44End
45
46Definition sort3_def:
47sort3 R x y z =
48 if R x y then
49 if R y z then
50 [x;y;z]
51 else if R x z then
52 [x;z;y]
53 else
54 [z;x;y]
55 else if R y z then
56 if R x z then
57 [y;x;z]
58 else
59 [y;z;x]
60 else
61 [z;y;x]
62End
63
64Definition merge_def:
65 (merge R [] [] = []) /\
66 (merge R l [] = l) /\
67 (merge R [] l = l) /\
68 (merge R (x::l1) (y::l2) =
69 if R x y then
70 x::merge R l1 (y::l2)
71 else
72 y::merge R (x::l1) l2)
73End
74
75Definition mergesortN_def:
76 (mergesortN R 0 l = []) /\
77 (mergesortN R 1 (x::l) = [x]) /\
78 (mergesortN R 1 [] = []) /\
79 (mergesortN R 2 (x::y::l) = sort2 R x y) /\
80 (mergesortN R 2 [x] = [x]) /\
81 (mergesortN R 2 [] = []) /\
82 (mergesortN R 3 (x::y::z::l) = sort3 R x y z) /\
83 (mergesortN R 3 [x;y] = sort2 R x y) /\
84 (mergesortN R 3 [x] = [x]) /\
85 (mergesortN R 3 [] = []) /\
86 (mergesortN R n l =
87 let len1 = DIV2 n in
88 merge R
89 (mergesortN R (DIV2 n) l)
90 (mergesortN R (n - len1) (DROP len1 l)))
91End
92
93Definition mergesort_def:
94 mergesort R l = mergesortN R (LENGTH l) l
95End
96
97(* A mergesort using tail recursive merging. This is what OCaml's standard
98 * library does, but instead of parameterizing with negate, it just copies the
99 * code for merge_rev sort. *)
100
101Definition sort2_tail_def:
102 sort2_tail (neg:bool) R x y =
103 if R x y <> neg then
104 [x;y]
105 else
106 [y;x]
107End
108
109Definition sort3_tail_def:
110 sort3_tail (neg:bool) R x y z =
111 if R x y <> neg then
112 if R y z <> neg then
113 [x;y;z]
114 else if R x z <> neg then
115 [x;z;y]
116 else
117 [z;x;y]
118 else if R y z <> neg then
119 if R x z <> neg then
120 [y;x;z]
121 else
122 [y;z;x]
123 else
124 [z;y;x]
125End
126
127Definition merge_tail_def:
128 (merge_tail (negate:bool) R [] [] acc = acc) /\
129 (merge_tail negate R l [] acc = REV l acc) /\
130 (merge_tail negate R [] l acc = REV l acc) /\
131 (merge_tail negate R (x::l1) (y::l2) acc =
132 if R x y <> negate then
133 merge_tail negate R l1 (y::l2) (x::acc)
134 else
135 merge_tail negate R (x::l1) l2 (y::acc))
136End
137
138Definition mergesortN_tail_def:
139 (mergesortN_tail (negate :bool) R 0 l = []) /\
140 (mergesortN_tail negate R 1 (x::l) = [x]) /\
141 (mergesortN_tail negate R 1 [] = []) /\
142 (mergesortN_tail negate R 2 (x::y::l) = sort2_tail negate R x y) /\
143 (mergesortN_tail negate R 2 [x] = [x]) /\
144 (mergesortN_tail negate R 2 [] = []) /\
145 (mergesortN_tail negate R 3 (x::y::z::l) = sort3_tail negate R x y z) /\
146 (mergesortN_tail negate R 3 [x;y] = sort2_tail negate R x y) /\
147 (mergesortN_tail negate R 3 [x] = [x]) /\
148 (mergesortN_tail negate R 3 [] = []) /\
149 (mergesortN_tail negate R n l =
150 let len1 = DIV2 n in
151 let neg = ~negate in
152 merge_tail neg R (mergesortN_tail neg R (DIV2 n) l)
153 (mergesortN_tail neg R (n - len1) (DROP len1 l))
154 [])
155End
156
157Definition mergesort_tail_def:
158 mergesort_tail R l = mergesortN_tail F R (LENGTH l) l
159End
160
161
162(* ------------------------- proofs ----------------------- *)
163
164(* mergesort permutes its input *)
165
166Theorem sort2_perm:
167 !R x y. PERM [x;y] (sort2 R x y)
168Proof
169 srw_tac [PERM_ss] [sort2_def]
170QED
171
172Theorem sort3_perm:
173 !R x y z. PERM [x;y;z] (sort3 R x y z)
174Proof
175 srw_tac [PERM_ss] [sort3_def]
176QED
177
178Theorem merge_perm:
179 !R l1 l2. PERM (l1++l2) (merge R l1 l2)
180Proof
181 ho_match_mp_tac merge_ind >>
182 srw_tac[][merge_def] >>
183 full_simp_tac (srw_ss()++PERM_ss) []
184QED
185
186Theorem mergesortN_perm:
187 !R n l. PERM (TAKE n l) (mergesortN R n l)
188Proof
189 ho_match_mp_tac mergesortN_ind >>
190 srw_tac[][] >>
191 ONCE_REWRITE_TAC [mergesortN_def] >>
192 srw_tac[][sort2_perm, sort3_perm]
193 >- (every_case_tac >>
194 fs [])
195 >- (every_case_tac >>
196 fs [sort2_perm] >>
197 metis_tac [])
198 >- (every_case_tac >>
199 fs [sort2_perm, sort3_perm] >>
200 metis_tac []) >>
201 `len1 <= n`
202 by (UNABBREV_ALL_TAC >>
203 fs [DIV2_def, DIV_LESS_EQ]) >>
204 metis_tac [take_drop_partition, PERM_TRANS, PERM_CONG, merge_perm]
205QED
206
207Theorem mergesort_perm:
208 !R l. PERM l (mergesort R l)
209Proof
210 srw_tac[][mergesort_def] >>
211 metis_tac [TAKE_LENGTH_ID, mergesortN_perm]
212QED
213
214(* mergesort's output is sorted *)
215
216Theorem sort2_sorted:
217 !R x y.
218 total R
219 ==>
220 SORTED R (sort2 R x y)
221Proof
222 srw_tac[][sort2_def, SORTED_DEF, total_def] >>
223 metis_tac []
224QED
225
226Theorem sort3_sorted:
227 !R x y z.
228 total R
229 ==>
230 SORTED R (sort3 R x y z)
231Proof
232 srw_tac[][sort3_def, SORTED_DEF, total_def] >>
233 metis_tac []
234QED
235
236Theorem merge_sorted:
237 !R l1 l2.
238 transitive R /\ total R /\ SORTED R l1 /\ SORTED R l2
239 ==>
240 SORTED R (merge R l1 l2)
241Proof
242 ho_match_mp_tac merge_ind >>
243 srw_tac[][merge_def] >>
244 REV_FULL_SIMP_TAC (srw_ss()) [SORTED_EQ] >>
245 srw_tac[][] >>
246 fs [transitive_def, total_def]
247 >- (`PERM (l1++(y::l2)) (merge R l1 (y::l2))` by metis_tac [merge_perm] >>
248 imp_res_tac MEM_PERM >>
249 fs [] >>
250 metis_tac [])
251 >- (`PERM ((x::l1)++l2) (merge R (x::l1) l2)` by metis_tac [merge_perm] >>
252 imp_res_tac MEM_PERM >>
253 fs [] >>
254 metis_tac [])
255QED
256
257Theorem mergesortN_sorted:
258 !R n l.
259 total R /\ transitive R
260 ==>
261 SORTED R (mergesortN R n l)
262Proof
263 ho_match_mp_tac mergesortN_ind >>
264 srw_tac[][] >>
265 ONCE_REWRITE_TAC [mergesortN_def] >>
266 srw_tac[][SORTED_EQ, SORTED_DEF, sort2_sorted, sort3_sorted]
267 >- (Cases_on `l` >>
268 srw_tac[][])
269 >- (Cases_on `l` >>
270 srw_tac[][] >>
271 Cases_on `t` >>
272 srw_tac[][sort2_sorted])
273 >- (Cases_on `l` >>
274 srw_tac[][] >>
275 Cases_on `t` >>
276 srw_tac[][sort2_sorted] >>
277 Cases_on `t'` >>
278 srw_tac[][sort2_sorted, sort3_sorted])
279 >- metis_tac [merge_sorted]
280QED
281
282Theorem mergesort_sorted:
283 !R l. transitive R /\ total R ==> SORTED R (mergesort R l)
284Proof
285 metis_tac [mergesort_def, mergesortN_sorted]
286QED
287
288(* mergesort is stable *)
289
290Theorem stable_cong:
291 !R l1 l2 l3 l4.
292 stable R l1 l2 /\ stable R l3 l4
293 ==>
294 stable R (l1++l3) (l2++l4)
295Proof
296 srw_tac[][stable_def, FILTER_APPEND]
297QED
298
299Theorem stable_trans:
300 !R l1 l2 l3.
301 stable R l1 l2 /\ stable R l2 l3
302 ==>
303 stable R l1 l3
304Proof
305 srw_tac[][stable_def]
306QED
307
308Theorem sort2_stable:
309 !R x y. stable R [x;y] (sort2 R x y)
310Proof
311 srw_tac[][stable_def, sort2_def] >>
312 every_case_tac >>
313 srw_tac[][] >>
314 metis_tac []
315QED
316
317Theorem sort3_stable:
318 !R x y z.
319 total R /\ transitive R
320 ==>
321 stable R [x;y;z] (sort3 R x y z)
322Proof
323 srw_tac[][sort3_def, stable_def] >>
324 every_case_tac >>
325 srw_tac[][] >>
326 metis_tac [total_def, transitive_def]
327QED
328
329Theorem filter_merge:
330 !P R l1 l2.
331 transitive R /\
332 (!x y. P x /\ P y ==> R x y) /\
333 SORTED R l1
334 ==>
335 FILTER P (merge R l1 l2) = FILTER P (l1 ++ l2)
336Proof
337 gen_tac >>
338 ho_match_mp_tac merge_ind >>
339 srw_tac[][merge_def, SORTED_EQ] >>
340 srw_tac[][merge_def, FILTER_APPEND] >>
341 REV_FULL_SIMP_TAC (srw_ss()) [SORTED_EQ, FILTER_APPEND]
342 >- metis_tac []
343 >- metis_tac []
344 >- (`FILTER P l1 = []`
345 by (srw_tac[][FILTER_EQ_NIL] >>
346 CCONTR_TAC >>
347 fs [EXISTS_MEM] >>
348 metis_tac [transitive_def]) >>
349 srw_tac[][])
350QED
351
352Theorem merge_stable:
353 !R l1 l2.
354 transitive R /\
355 SORTED R l1
356 ==>
357 stable R (l1 ++ l2) (merge R l1 l2)
358Proof
359 srw_tac[][stable_def, filter_merge]
360QED
361
362Theorem mergesortN_stable:
363 !R n l.
364 total R /\ transitive R
365 ==>
366 stable R (TAKE n l) (mergesortN R n l)
367Proof
368 ho_match_mp_tac mergesortN_ind >>
369 srw_tac[][] >>
370 ONCE_REWRITE_TAC [mergesortN_def] >>
371 srw_tac[][sort2_stable, sort3_stable] >>
372 TRY (srw_tac[][stable_def] >> NO_TAC)
373 >- (Cases_on `l` >>
374 srw_tac[][stable_def])
375 >- (Cases_on `l` >>
376 srw_tac[][] >>
377 TRY (srw_tac[][stable_def] >> NO_TAC) >>
378 Cases_on `t` >>
379 srw_tac[][sort2_stable] >>
380 srw_tac[][stable_def])
381 >- (Cases_on `l` >>
382 srw_tac[][] >>
383 TRY (srw_tac[][stable_def] >> NO_TAC) >>
384 Cases_on `t` >>
385 srw_tac[][sort2_stable] >>
386 TRY (srw_tac[][stable_def] >> NO_TAC) >>
387 Cases_on `t'` >>
388 srw_tac[][sort2_stable, sort3_stable])
389 >- (`len1 <= n`
390 by (UNABBREV_ALL_TAC >>
391 fs [DIV2_def, DIV_LESS_EQ]) >>
392 metis_tac [stable_cong, merge_stable, take_drop_partition, stable_trans,
393 mergesortN_sorted])
394QED
395
396Theorem mergesort_stable:
397 !R l. transitive R /\ total R ==> stable R l (mergesort R l)
398Proof
399 metis_tac [mergesortN_stable, mergesort_def, TAKE_LENGTH_ID]
400QED
401
402(* packaging things up *)
403
404Theorem mergesort_STABLE_SORT:
405 !R. transitive R /\ total R ==> STABLE mergesort R
406Proof
407 srw_tac[][STABLE_DEF, SORTS_DEF] >>
408 metis_tac [mergesort_perm, mergesort_sorted, mergesort_stable, stable_def]
409QED
410
411Theorem mergesort_mem:
412 !R L x. MEM x (mergesort R L) <=> MEM x L
413Proof
414 metis_tac [mergesort_perm, MEM_PERM]
415QED
416
417(* On to mergesort_tail *)
418
419Theorem sort2_tail_correct:
420 !neg R x y.
421 sort2_tail neg R x y = if neg then REVERSE (sort2 R x y) else sort2 R x y
422Proof
423 srw_tac[][sort2_def, sort2_tail_def] >>
424 fs []
425QED
426
427Theorem sort3_tail_correct:
428 !neg R x y z.
429 sort3_tail neg R x y z = if neg then REVERSE (sort3 R x y z)
430 else sort3 R x y z
431Proof srw_tac[][sort3_def, sort3_tail_def] >> fs []
432QED
433
434Theorem merge_tail_correct1:
435 !neg R l1 l2 acc.
436 (neg = F)
437 ==>
438 merge_tail neg R l1 l2 acc = REVERSE (merge R l1 l2) ++ acc
439Proof
440 ho_match_mp_tac merge_tail_ind >>
441 srw_tac[][merge_tail_def, merge_def, REV_REVERSE_LEM]
442QED
443
444Theorem merge_empty:
445 !R l acc.
446 merge R l [] = l /\
447 merge R [] l = l
448Proof
449 Cases_on `l` >>
450 srw_tac[][merge_def]
451QED
452
453Theorem merge_last_lem1[local]:
454 !R l1 l2 x.
455 (!y. MEM y l2 ==> ~R x y)
456 ==>
457 merge R (l1 ++ [x]) l2 = merge R l1 l2 ++ [x]
458Proof
459 ho_match_mp_tac merge_ind >>
460 srw_tac[][merge_def, merge_empty] >>
461 Induct_on `v5` >>
462 srw_tac[][merge_empty, merge_def] >>
463 metis_tac []
464QED
465
466Theorem merge_last_lem2[local]:
467 !R l1 l2 y.
468 (!x. MEM x l1 ==> R x y)
469 ==>
470 merge R l1 (l2 ++ [y]) = merge R l1 l2 ++ [y]
471Proof
472 ho_match_mp_tac merge_ind >>
473 srw_tac[][merge_def, merge_empty] >>
474 Induct_on `v9` >>
475 srw_tac[][merge_empty, merge_def] >>
476 metis_tac []
477QED
478
479Theorem merge_tail_correct2:
480 !neg R l1 l2 acc.
481 (neg = T) /\
482 transitive R /\
483 SORTED R (REVERSE l1) /\
484 SORTED R (REVERSE l2)
485 ==>
486 merge_tail neg R l1 l2 acc = (merge R (REVERSE l1) (REVERSE l2)) ++ acc
487Proof
488 ho_match_mp_tac merge_tail_ind >>
489 srw_tac[][merge_tail_def, merge_def, REV_REVERSE_LEM, merge_empty] >>
490 fs [] >>
491 `SORTED R (REVERSE l1) /\ SORTED R (REVERSE l2)`
492 by metis_tac [SORTED_APPEND_GEN] >>
493 fs []
494 >- (match_mp_tac (GSYM merge_last_lem1) >>
495 srw_tac[][] >>
496 srw_tac[][] >>
497 CCONTR_TAC >>
498 fs [] >>
499 `R y' y` by metis_tac [mem_sorted_append, MEM_REVERSE, MEM] >>
500 metis_tac [transitive_def])
501 >- (match_mp_tac (GSYM merge_last_lem2) >>
502 srw_tac[][] >>
503 srw_tac[][] >>
504 `R x' x` by metis_tac [mem_sorted_append, MEM_REVERSE, MEM] >>
505 metis_tac [transitive_def])
506QED
507
508Theorem mergesortN_correct:
509 !negate R n l.
510 total R /\
511 transitive R
512 ==>
513 mergesortN_tail negate R n l =
514 (if negate then REVERSE (mergesortN R n l) else mergesortN R n l)
515Proof
516 ho_match_mp_tac mergesortN_tail_ind >>
517 srw_tac[][] >>
518 ONCE_REWRITE_TAC [mergesortN_tail_def, mergesortN_def] >>
519 srw_tac[][sort2_tail_correct, sort3_tail_correct] >>
520 fs [] >>
521 every_case_tac >>
522 fs [] >>
523 UNABBREV_ALL_TAC >>
524 srw_tac[][merge_tail_correct1] >>
525 metis_tac [merge_tail_correct2, mergesortN_sorted, REVERSE_REVERSE,APPEND_NIL]
526QED
527
528Theorem mergesort_tail_correct:
529 !R l.
530 total R /\
531 transitive R
532 ==>
533 mergesort_tail R l = mergesort R l
534Proof
535 srw_tac[][mergesort_tail_def, mergesort_def, mergesortN_correct]
536QED
537
538
539 (*
540(* Timings *)
541
542load "intLib";
543
544val mergesortN'_def = tDefine "mergesortN'" `
545(mergesortN' R 0 l = []) /\
546(mergesortN' R 1 (x::l) = [x]) /\
547(mergesortN' R 1 [] = []) /\
548(mergesortN' R 2 (x::y::l) = sort2 R x y) /\
549(mergesortN' R 2 [x] = [x]) /\
550(mergesortN' R 2 [] = []) /\
551(mergesortN' R n l =
552 let len1 = DIV2 n in
553 merge R (mergesortN' R (DIV2 n) l)
554 (mergesortN' R (n - len1) (DROP len1 l)))`
555 (WF_REL_TAC `measure (λ(R,n,l). n)` >>
556 srw_tac[][DIV2_def] >>
557 COOPER_TAC);
558
559val mergesortN''_def = tDefine "mergesortN''" `
560(mergesortN'' R 0 l = []) /\
561(mergesortN'' R 1 (x::l) = [x]) /\
562(mergesortN'' R 1 [] = []) /\
563(mergesortN'' R n l =
564 let len1 = DIV2 n in
565 merge R (mergesortN'' R (DIV2 n) l)
566 (mergesortN'' R (n - len1) (DROP len1 l)))`
567 (WF_REL_TAC `measure (λ(R,n,l). n)` >>
568 srw_tac[][DIV2_def] >>
569 COOPER_TAC);
570
571val rand_list_def = Define `
572(rand_list 0 seed = []) /\
573(rand_list (SUC n) seed =
574 let v = (1664525 * seed + 1013904223) MOD 4294967296 in
575 v::rand_list n v)`;
576
577val l = (time EVAL ``rand_list 10000 353``) |> concl |> rand;
578val len_l = ``10000:num``;
579
580val l' = (time EVAL ``MAP (\x. x MOD 65536) ^l``) |> concl |> rand;
581
582
583time (fn x => (EVAL x; ())) ``LENGTH (COUNT_LIST 10000)``;
584time (fn x => (EVAL x; ())) ``COUNT_LIST 10000``;
585
586time (fn x => (EVAL x; ())) ``mergesortN $<= 10000 (COUNT_LIST 10000)``;
587>runtime: 10.905s, gctime: 0.29495s, systime: 0.06740s.
588time (fn x => (EVAL x; ())) ``mergesortN $<= ^len_l ^l``;
589> runtime: 27.618s, gctime: 1.106s, systime: 0.24801s.
590time (fn x => (EVAL x; ())) ``mergesortN $<= ^len_l ^l'``;
591> runtime: 18.192s, gctime: 0.76859s, systime: 0.16917s.
592
593time (fn x => (EVAL x; ())) ``mergesortN' $<= 10000 (COUNT_LIST 10000)``;
594> runtime: 11.322s, gctime: 0.33336s, systime: 0.07988s
595time (fn x => (EVAL x; ())) ``mergesortN' $<= ^len_l ^l``;
596> runtime: 28.974s, gctime: 1.162s, systime: 0.31028s.
597time (fn x => (EVAL x; ())) ``mergesortN' $<= ^len_l ^l'``;
598> runtime: 18.985s, gctime: 0.94506s, systime: 0.22901s.
599
600time (fn x => (EVAL x; ())) ``mergesortN'' $<= 10000 (COUNT_LIST 10000)``;
601> runtime: 11.977s, gctime: 0.34678s, systime: 0.08751s.
602time (fn => (EVAL x; ())) ``mergesortN'' $<= ^len_l ^l``;
603> runtime: 29.934s, gctime: 1.386s, systime: 0.38797s.
604time (fn x => (EVAL x; ())) ``mergesortN'' $<= ^len_l ^l'``;
605> runtime: 20.251s, gctime: 1.180s, systime: 0.26435s.
606
607time (fn x => (EVAL x; ())) ``mergesort_tail $<= (COUNT_LIST 10000)``;
608> runtime: 13.388s, gctime: 0.59262s, systime: 0.15220s.
609time (fn x => (EVAL x; ())) ``mergesort_tail $<= ^l``;
610> runtime: 30.701s, gctime: 1.878s, systime: 0.68566s.
611time (fn x => (EVAL x; ())) ``mergesort_tail $<= ^l'``;
612> runtime: 20.488s, gctime: 0.64356s, systime: 0.59357s.
613
614time (fn x => (EVAL x; ())) ``QSORT3 $<= (COUNT_LIST 500)``;
615> runtime: 31.436s, gctime: 0.97548s, systime: 0.23698s.
616time (fn x => (EVAL x; ())) ``QSORT3 $<= ^l``;
617> runtime: 1m23s, gctime: 6.614s, systime: 2.108s.
618time (fn x => (EVAL x; ())) ``QSORT3 $<= ^l'``;
619> runtime: 55.361s, gctime: 5.010s, systime: 2.373s.
620
621time (fn x => (EVAL x; ())) ``QSORT $<= (COUNT_LIST 500)``;
622> runtime: 10.795s, gctime: 0.80040s, systime: 0.11975s.
623time (fn x => (EVAL x; ())) ``QSORT $<= ^l``;
624> runtime: 33.837s, gctime: 1.495s, systime: 0.33714s.
625time (fn x => (EVAL x; ())) ``QSORT $<= ^l'``;
626> runtime: 21.398s, gctime: 1.040s, systime: 0.22661s.
627
628*)
629