Permutation/qsort.ml

   1 (* ========================================================================= *)
   2 (*  Quick sort algorithm.                                                    *)
   3 (*                                                                           *)
   4 (*  Author: Marco Maggesi                                                    *)
   5 (*          University of Florence, Italy                                    *)
   6 (*          http://www.math.unifi.it/~maggesi/                               *)
   7 (*                                                                           *)
   8 (*          (c) Copyright, Marco Maggesi, 2005-2007                          *)
   9 (* ========================================================================= *)
  10
  11 needs "Permutation/permuted.ml";;
  12
  13 (* ------------------------------------------------------------------------- *)
  14 (* Ordered lists.                                                            *)
  15 (* ------------------------------------------------------------------------- *)
  16
  17 let ORDERED_RULES, ORDERED_INDUCT, ORDERED_CASES = new_inductive_definition
  18   `(!le. ORDERED le []) /\
  19    (!le h t. ORDERED le t /\ ALL (le h) t ==> ORDERED le (CONS h t))`;;
  20
  21 let ORDERED_CONS = prove
  22   (`!le (h:A) t. ORDERED le (h :: t) <=> (ORDERED le t /\ ALL (le h) t)`,
  23    SUBGOAL_THEN
  24     `!le (h:A) t. ORDERED le (h :: t) ==> (ORDERED le t /\ ALL (le h) t)`
  25    (fun th -> MESON_TAC [th; ORDERED_RULES]) THEN
  26    REPEAT GEN_TAC THEN
  27    DISCH_THEN (MP_TAC o ONCE_REWRITE_RULE [ORDERED_CASES]) THEN
  28    REWRITE_TAC [NOT_CONS_NIL; CONS_11] THEN MESON_TAC []);;
  29
  30 let ORDERED_APPEND = prove
  31  (`!l1 l2:A list.
  32       ORDERED le (APPEND l1 l2) <=>
  33       ORDERED le l1 /\ ORDERED le l2 /\ ALL (\x. ALL (le x) l2) l1`,
  34   SUBGOAL_THEN
  35     `(!l1 l2:A list.
  36         ORDERED le (APPEND l1 l2)
  37         ==> ORDERED le l1 /\ ORDERED le l2 /\ ALL (\x. ALL (le x) l2) l1) /\
  38      (!l1 l2. ORDERED le l1 /\ ORDERED le l2 /\ ALL (\x. ALL (le x) l2) l1
  39               ==> ORDERED le (APPEND l1 l2))`
  40    (fun th -> MESON_TAC [th]) THEN
  41    CONJ_TAC THEN LIST_INDUCT_TAC THEN
  42    REWRITE_TAC [APPEND; ALL; ORDERED_RULES; ORDERED_CONS] THEN
  43    ASM_SIMP_TAC [ORDERED_CONS; ALL_APPEND] THEN ASM_MESON_TAC [ALL_APPEND]);;
  44
  45 (* ------------------------------------------------------------------------- *)
  46 (*  Quick Sort.                                                              *)
  47 (* ------------------------------------------------------------------------- *)
  48
  49 let QSORT =
  50   let PROVE_RECURSIVE_FUNCTION_EXISTS_TAC : tactic = fun g ->
  51     let th = pure_prove_recursive_function_exists (snd g) in
  52     MATCH_MP_TAC (DISCH_ALL th) g in
  53   new_specification ["QSORT"] (prove
  54   (`?f. (!le. f le [] = [] : A list) /\
  55         (!le h t. f le (CONS h t) =
  56                   APPEND (f le (FILTER (\x. ~le h x) t))
  57                   (CONS h (f le (FILTER (\x. le h x) t))))`,
  58    REWRITE_TAC [GSYM SKOLEM_THM; AND_FORALL_THM] THEN GEN_TAC THEN
  59    PROVE_RECURSIVE_FUNCTION_EXISTS_TAC THEN
  60    EXISTS_TAC `MEASURE (LENGTH:A list -> num)` THEN
  61    REWRITE_TAC [WF_MEASURE; MEASURE; LENGTH; FILTER] THEN
  62    REWRITE_TAC [LT_SUC_LE; LENGTH_FILTER_LE]));;
  63
  64 let COUNT_QSORT = prove
  65   (`!le x l. COUNT x (QSORT le l) = COUNT x l`,
  66    GEN_TAC THEN GEN_TAC THEN MATCH_MP_TAC list_WF THEN LIST_INDUCT_TAC THEN
  67    REWRITE_TAC [QSORT; COUNT; LENGTH; LT_SUC_LE; COUNT_APPEND] THEN
  68    DISCH_TAC THEN ASM_SIMP_TAC [COUNT; LENGTH_FILTER_LE] THEN
  69    REWRITE_TAC [COUNT_FILTER] THEN
  70    REPEAT (ASM_REWRITE_TAC [ADD; ADD_SUC; ADD_0] THEN COND_CASES_TAC) THEN
  71    ASM_MESON_TAC[ADD_SUC]);;
  72
  73 let QSORT_PERMUTED = prove
  74   (`!le (l:A list). QSORT le l PERMUTED l`,
  75    REWRITE_TAC [PERMUTED_COUNT; COUNT_QSORT]);;
  76
  77 let ALL_QSORT = prove
  78   (`!P le l. ALL P (QSORT le l) <=> ALL P l`,
  79    MESON_TAC [QSORT_PERMUTED; PERMUTED_ALL]);;
  80
  81 let LENGTH_QSORT = prove
  82   (`!le l. LENGTH (QSORT le l) =  LENGTH l`,
  83    MESON_TAC [QSORT_PERMUTED; PERMUTED_LENGTH]);;
  84
  85 let MEM_QSORT = prove
  86   (`!le l x. MEM x (QSORT le l) <=> MEM x l`,
  87    MESON_TAC [QSORT_PERMUTED; PERMUTED_MEM]);;
  88
  89 let ORDERED_QSORT = prove
  90  (`!le (l:A list).
  91      (!x y. le x y \/ le y x) /\ (!x y z. le x y \/ le y z ==> le x z)
  92      ==> ORDERED le (QSORT le l)`,
  93    REWRITE_TAC [GSYM RIGHT_IMP_FORALL_THM] THEN GEN_TAC THEN STRIP_TAC THEN
  94    MATCH_MP_TAC list_WF THEN LIST_CASES_TAC THEN
  95    REWRITE_TAC [QSORT; LENGTH; ORDERED_RULES; LT_SUC_LE] THEN DISCH_TAC THEN
  96    REWRITE_TAC [ORDERED_APPEND; ORDERED_CONS; ALL; ALL_QSORT; ALL_T] THEN
  97    ASM_SIMP_TAC [LENGTH_FILTER_LE] THEN REWRITE_TAC [GSYM ALL_MEM] THEN
  98    ASM_MESON_TAC[]);;
  99
 100 (* Example:
 101 REWRITE_CONV [QSORT; ARITH_LE; ARITH_LT; FILTER; APPEND]
 102   `QSORT (<=) [12;3;5;1;23;2;1]`;;
 103 *)