Permutation/morelist.ml

   1 (* ========================================================================= *)
   2 (*  More definitions and theorems and tactics about lists.                   *)
   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 parse_as_infix ("::",(23,"right"));;
  12 override_interface("::",`CONS`);;
  13
  14 (* ------------------------------------------------------------------------- *)
  15 (*  Some handy tactics.                                                      *)
  16 (* ------------------------------------------------------------------------- *)
  17
  18 let ASSERT_TAC tm = SUBGOAL_THEN tm ASSUME_TAC;;
  19
  20 let SUFFICE_TAC thl tm =
  21   SUBGOAL_THEN tm (fun th -> MESON_TAC (th :: thl));;
  22
  23 let LIST_CASES_TAC =
  24   let th = prove (`!P. P [] /\ (!h t. P (h :: t)) ==> !l. P l`,
  25                   GEN_TAC THEN STRIP_TAC THEN
  26                   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [])
  27   in
  28   MATCH_MP_TAC th THEN CONJ_TAC THENL
  29   [ALL_TAC; GEN_TAC THEN GEN_TAC];;
  30
  31 (* ------------------------------------------------------------------------- *)
  32 (*  Occasionally useful stuff.                                               *)
  33 (* ------------------------------------------------------------------------- *)
  34
  35 let NULL_EQ_NIL = prove
  36   (`!l. NULL l <=> l = []`,
  37    LIST_CASES_TAC THEN REWRITE_TAC [NULL; NOT_CONS_NIL]);;
  38
  39 let NULL_LENGTH = prove
  40   (`!l. NULL l <=> LENGTH l = 0`,
  41    LIST_CASES_TAC THEN REWRITE_TAC [NULL; LENGTH; NOT_SUC]);;
  42
  43 let LENGTH_FILTER_LE = prove
  44   (`!f l:A list. LENGTH (FILTER f l) <= LENGTH l`,
  45    GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC [FILTER; LENGTH; LE_0] THEN
  46    COND_CASES_TAC THEN
  47    ASM_SIMP_TAC [LENGTH; LE_SUC; ARITH_RULE `n<=m ==> n<= SUC m`]);;
  48
  49 (* ------------------------------------------------------------------------- *)
  50 (*  Well-founded induction on lists.                                         *)
  51 (* ------------------------------------------------------------------------- *)
  52
  53 let list_WF = prove
  54   (`!P. (!l. (!l'. LENGTH l' < LENGTH l ==> P l') ==> P l)
  55         ==> (!l:A list. P l)`,
  56    MP_TAC (ISPEC `LENGTH:A list->num` WF_MEASURE) THEN
  57    REWRITE_TAC [WF_IND; MEASURE]);;
  58
  59 (* ------------------------------------------------------------------------- *)
  60 (*  Delete one element from a list.                                          *)
  61 (* ------------------------------------------------------------------------- *)
  62
  63 let DELETE1 = define
  64   `(!x. DELETE1 x [] = []) /\
  65    (!x h t. DELETE1 x (h :: t) = if x = h then t
  66                                           else h :: DELETE1 x t)`;;
  67
  68 let DELETE1_ID = prove
  69   (`!x l. ~MEM x l ==> DELETE1 x l = l`,
  70    GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC [MEM; DELETE1] THEN
  71    COND_CASES_TAC THEN ASM_REWRITE_TAC [NOT_CONS_NIL; CONS_11]);;
  72
  73 let DELETE1_APPEND = prove
  74   (`!x l1 l2. DELETE1 x (APPEND l1 l2) =
  75               if MEM x l1 then APPEND (DELETE1 x l1) l2
  76                           else APPEND l1 (DELETE1 x l2)`,
  77    GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC [APPEND; DELETE1; MEM] THEN
  78    GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[MEM; APPEND] THEN
  79    COND_CASES_TAC THEN ASM_REWRITE_TAC[]);;
  80
  81 let FILTER_DELETE1 = prove
  82   (`!P x l. FILTER P (DELETE1 x l) =
  83             if P x then DELETE1 x (FILTER P l) else FILTER P l`,
  84    GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN
  85    REPEAT (REWRITE_TAC [DELETE1; FILTER] THEN COND_CASES_TAC) THEN
  86    ASM_MESON_TAC []);;
  87
  88 let LENGTH_DELETE1 = prove
  89   (`!l x:A. LENGTH (DELETE1 x l) =
  90             if MEM x l then PRE (LENGTH l) else LENGTH l`,
  91    LIST_INDUCT_TAC THEN REWRITE_TAC [MEM; LENGTH; DELETE1] THEN GEN_TAC THEN
  92    COND_CASES_TAC THEN ASM_REWRITE_TAC[PRE; LENGTH] THEN COND_CASES_TAC THEN
  93    REWRITE_TAC [ARITH_RULE `SUC (PRE n)=n <=> ~(n=0)`; LENGTH_EQ_NIL] THEN
  94    ASM_MESON_TAC [MEM]);;
  95
  96 let MEM_DELETE1_MEM_IMP = prove
  97   (`!h t x. MEM x (DELETE1 h t) ==> MEM x t`,
  98    GEN_TAC THEN LIST_INDUCT_TAC THEN GEN_TAC THEN
  99    REWRITE_TAC [MEM; DELETE1] THEN COND_CASES_TAC THEN
 100    REWRITE_TAC [MEM] THEN STRIP_TAC THEN ASM_SIMP_TAC []);;
 101
 102 let NOT_MEM_DELETE1 = prove
 103   (`!t h x. ~MEM x t ==> ~MEM x (DELETE1 h t)`,
 104    LIST_INDUCT_TAC THEN GEN_TAC THEN GEN_TAC THEN
 105    REWRITE_TAC [MEM; DELETE1] THEN
 106    COND_CASES_TAC THEN REWRITE_TAC [MEM; DE_MORGAN_THM] THEN
 107    STRIP_TAC THEN ASM_SIMP_TAC []);;
 108
 109 let MEM_DELETE1 = prove
 110   (`!l x y:A. MEM x l /\ ~(x = y) ==> MEM x (DELETE1 y l)`,
 111    LIST_INDUCT_TAC THEN REWRITE_TAC [MEM; DELETE1] THEN
 112    GEN_TAC THEN GEN_TAC THEN COND_CASES_TAC THENL
 113    [EXPAND_TAC "h" THEN MESON_TAC [];
 114     REWRITE_TAC [MEM] THEN ASM_MESON_TAC []]);;
 115
 116 let ALL_DELETE1_ALL_IMP = prove
 117   (`!P x l. P x /\ ALL P (DELETE1 x l) ==> ALL P l`,
 118    GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN
 119    REWRITE_TAC [ALL; DELETE1] THEN
 120    COND_CASES_TAC THEN ASM_SIMP_TAC [ALL]);;
 121
 122 (* ------------------------------------------------------------------------- *)
 123 (*  Counting occurrences of a given element in a list.                       *)
 124 (* ------------------------------------------------------------------------- *)
 125
 126 let COUNT = define
 127   `(!x. COUNT x [] = 0) /\
 128    (!x h t. COUNT x (CONS h t) = if x=h then SUC (COUNT x t) else COUNT x t)`;;
 129
 130 let COUNT_LENGTH_FILTER = prove
 131   (`!x l. COUNT x l = LENGTH (FILTER ((=) x) l)`,
 132    GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC [COUNT; FILTER; LENGTH] THEN
 133    COND_CASES_TAC THEN ASM_REWRITE_TAC [LENGTH]);;
 134
 135 let COUNT_FILTER = prove
 136   (`!P x l. COUNT x (FILTER P l) =
 137             if P x then COUNT x l else 0`,
 138    GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN
 139    REPEAT (ASM_REWRITE_TAC [COUNT; FILTER] THEN COND_CASES_TAC) THEN
 140    ASM_MESON_TAC []);;
 141
 142 let COUNT_APPEND = prove
 143   (`!x l1 l2. COUNT x (APPEND l1 l2) = COUNT x l1 + COUNT x l2`,
 144     REWRITE_TAC [COUNT_LENGTH_FILTER; LENGTH_APPEND; FILTER_APPEND]);;
 145
 146 let COUNT_LE_LENGTH = prove
 147   (`!x l. COUNT x l <= LENGTH l`,
 148    GEN_TAC THEN LIST_INDUCT_TAC THEN
 149    ASM_REWRITE_TAC [COUNT; LENGTH; LE_REFL] THEN COND_CASES_TAC THEN
 150    ASM_SIMP_TAC [LE_SUC; ARITH_RULE `n<=m ==> n <= SUC m`]);;
 151
 152 let COUNT_ZERO = prove
 153   (`!x l. COUNT x l = 0 <=> ~MEM x l`,
 154    GEN_TAC THEN REWRITE_TAC [COUNT_LENGTH_FILTER; LENGTH_EQ_NIL] THEN
 155    LIST_INDUCT_TAC THEN REWRITE_TAC [FILTER; MEM] THEN COND_CASES_TAC THEN
 156    ASM_REWRITE_TAC [NOT_CONS_NIL]);;
 157
 158 let MEM_COUNT = prove
 159   (`!x l. MEM x l <=> ~(COUNT x l = 0)`,
 160    MESON_TAC [COUNT_ZERO]);;
 161
 162 let COUNT_DELETE1 = prove
 163   (`!y x l. COUNT y (DELETE1 (x:A) l) =
 164             if y=x /\ MEM x l then PRE (COUNT y l) else COUNT y l`,
 165    REWRITE_TAC [COUNT_LENGTH_FILTER; FILTER_DELETE1] THEN REPEAT GEN_TAC THEN
 166    COND_CASES_TAC THEN ASM_REWRITE_TAC[MEM_FILTER; LENGTH_DELETE1]);;
 167
 168 (* ------------------------------------------------------------------------- *)
 169 (*  Duplicates in a list.                                                    *)
 170 (* ------------------------------------------------------------------------- *)
 171
 172 let LIST_UNIQ_RULES, LIST_UNIQ_INDUCT, LIST_UNIQ_CASES =
 173   new_inductive_definition
 174   `LIST_UNIQ [] /\
 175    (!x xs. LIST_UNIQ xs /\ ~MEM x xs ==> LIST_UNIQ (x :: xs))`;;
 176
 177 let LIST_UNIQ = prove
 178   (`LIST_UNIQ [] /\
 179    (!x. LIST_UNIQ [x]) /\
 180    (!x xs. LIST_UNIQ (x :: xs) <=> ~MEM x xs /\ LIST_UNIQ xs)`,
 181    SIMP_TAC [LIST_UNIQ_RULES; MEM] THEN
 182    REPEAT GEN_TAC THEN EQ_TAC THENL
 183    [ONCE_REWRITE_TAC [ISPEC `h :: t` LIST_UNIQ_CASES] THEN
 184     REWRITE_TAC [CONS_11; NOT_CONS_NIL] THEN
 185     DISCH_THEN (CHOOSE_THEN CHOOSE_TAC) THEN ASM_REWRITE_TAC [];
 186     SIMP_TAC [LIST_UNIQ_RULES]]);;
 187
 188 (* !!! forse e' meglio con IMP? *)
 189 (* Magari LIST_UNIQ_COUNT + COUNT_LIST_UNIQ *)
 190 let LIST_UNIQ_COUNT = prove
 191   (`!l. LIST_UNIQ l <=> (!x:A. COUNT x l = if MEM x l then 1 else 0)`,
 192    let IFF_EXPAND = MESON [] `(p <=> q) <=> (p ==> q) /\ (q ==> p)` in
 193    REWRITE_TAC [IFF_EXPAND; FORALL_AND_THM] THEN CONJ_TAC THENL
 194    [MATCH_MP_TAC LIST_UNIQ_INDUCT THEN REWRITE_TAC [COUNT; MEM] THEN
 195     REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[ONE];
 196     LIST_INDUCT_TAC THEN REWRITE_TAC [LIST_UNIQ; COUNT; MEM] THEN
 197     DISCH_TAC THEN FIRST_ASSUM (MP_TAC o SPEC `h:A`) THEN
 198     SIMP_TAC [MEM_COUNT; ONE; SUC_INJ] THEN DISCH_TAC THEN
 199     FIRST_X_ASSUM MATCH_MP_TAC THEN GEN_TAC THEN
 200     FIRST_ASSUM (MP_TAC o SPEC `x:A`) THEN
 201     REWRITE_TAC [MEM_COUNT] THEN ARITH_TAC]);;
 202
 203 let LIST_UNIQ_DELETE1 = prove
 204   (`!l x. LIST_UNIQ l ==> LIST_UNIQ (DELETE1 x l)`,
 205    LIST_INDUCT_TAC THEN GEN_TAC THEN
 206    REWRITE_TAC [LIST_UNIQ; DELETE1] THEN STRIP_TAC THEN
 207    COND_CASES_TAC THEN ASM_SIMP_TAC [LIST_UNIQ; NOT_MEM_DELETE1]);;
 208
 209 let DELETE1_LIST_UNIQ = prove
 210   (`!l x:A. ~MEM x (DELETE1 x l) /\ LIST_UNIQ (DELETE1 x l)
 211             ==> LIST_UNIQ l`,
 212    LIST_INDUCT_TAC THEN REWRITE_TAC [LIST_UNIQ; DELETE1; MEM] THEN
 213    GEN_TAC THEN COND_CASES_TAC THEN
 214    ASM_REWRITE_TAC [MEM; LIST_UNIQ] THEN STRIP_TAC THEN CONJ_TAC THENL
 215    [ASM_MESON_TAC [MEM_DELETE1];
 216     FIRST_X_ASSUM MATCH_MP_TAC THEN EXISTS_TAC `x:A` THEN
 217     ASM_REWRITE_TAC []]);;
 218
 219 let LIST_UNIQ_APPEND = prove
 220  (`!l m. LIST_UNIQ (APPEND l m) <=>
 221          LIST_UNIQ l /\ LIST_UNIQ m /\
 222          !x. ~(MEM x l /\ MEM x m)`,
 223   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[APPEND; LIST_UNIQ; MEM; MEM_APPEND] THEN
 224   MESON_TAC[]);;
 225
 226 (* ------------------------------------------------------------------------- *)
 227 (*  Lists and finite sets.                                                   *)
 228 (* ------------------------------------------------------------------------- *)
 229
 230 let CARD_LENGTH = prove
 231   (`!l:A list. CARD (set_of_list l) <= LENGTH l`,
 232    LIST_INDUCT_TAC THEN
 233    SIMP_TAC [set_of_list; CARD_CLAUSES; LENGTH;
 234              FINITE_SET_OF_LIST; ARITH] THEN
 235    COND_CASES_TAC THENL
 236    [MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `LENGTH (t:A list)`
 237     THEN ASM_REWRITE_TAC [] THEN ARITH_TAC;
 238     ASM_REWRITE_TAC [LE_SUC]]);;
 239
 240 let LIST_UNIQ_CARD_LENGTH = prove
 241   (`!l:A list. LIST_UNIQ l <=> CARD (set_of_list l) = LENGTH l`,
 242    LIST_INDUCT_TAC THEN SIMP_TAC [LIST_UNIQ; set_of_list; FINITE_SET_OF_LIST;
 243                                   LENGTH; CARD_CLAUSES; IN_SET_OF_LIST] THEN
 244    FIRST_X_ASSUM SUBST1_TAC THEN COND_CASES_TAC THEN
 245    ASM_REWRITE_TAC[SUC_INJ] THEN MP_TAC (SPEC `t:A list` CARD_LENGTH) THEN
 246    ARITH_TAC);;
 247
 248 let LIST_UNIQ_LIST_OF_SET = prove
 249  (`!s. FINITE s ==> LIST_UNIQ(list_of_set s)`,
 250   SIMP_TAC[LIST_UNIQ_CARD_LENGTH; SET_OF_LIST_OF_SET; LENGTH_LIST_OF_SET]);;