Update from HH
[hl193./.git] / 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]);;