1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: ListSet.v 10616 2008-03-04 17:33:35Z letouzey $ i*)
11
(** A Library for finite sets, implemented as lists *)
13
(** List is loaded, but not exported.
14
This allow to "hide" the definitions, functions and theorems of List
15
and to see only the ones of ListSet *)
19
Set Implicit Arguments.
21
Section first_definitions.
24
Hypothesis Aeq_dec : forall x y:A, {x = y} + {x <> y}.
26
Definition set := list A.
28
Definition empty_set : set := nil.
30
Fixpoint set_add (a:A) (x:set) {struct x} : set :=
34
match Aeq_dec a a1 with
36
| right _ => a1 :: set_add a x1
41
Fixpoint set_mem (a:A) (x:set) {struct x} : bool :=
45
match Aeq_dec a a1 with
47
| right _ => set_mem a x1
51
(** If [a] belongs to [x], removes [a] from [x]. If not, does nothing *)
52
Fixpoint set_remove (a:A) (x:set) {struct x} : set :=
56
match Aeq_dec a a1 with
58
| right _ => a1 :: set_remove a x1
62
Fixpoint set_inter (x:set) : set -> set :=
67
if set_mem a1 y then a1 :: set_inter x1 y else set_inter x1 y
70
Fixpoint set_union (x y:set) {struct y} : set :=
73
| a1 :: y1 => set_add a1 (set_union x y1)
76
(** returns the set of all els of [x] that does not belong to [y] *)
77
Fixpoint set_diff (x y:set) {struct x} : set :=
81
if set_mem a1 y then set_diff x1 y else set_add a1 (set_diff x1 y)
85
Definition set_In : A -> set -> Prop := In (A:=A).
87
Lemma set_In_dec : forall (a:A) (x:set), {set_In a x} + {~ set_In a x}.
90
unfold set_In in |- *.
91
(*** Realizer set_mem. Program_all. ***)
94
intros a0 x0 Ha0. case (Aeq_dec a a0); intro eq.
95
rewrite eq; simpl in |- *; auto with datatypes.
98
right; simpl in |- *; unfold not in |- *; intros [Hc1| Hc2];
103
forall (B:Type) (P:B -> Prop) (y z:B) (a:A) (x:set),
104
(set_In a x -> P y) -> P z -> P (if set_mem a x then y else z).
107
simple induction x; simpl in |- *; intros.
109
elim (Aeq_dec a a0); auto with datatypes.
113
forall (B:Type) (P:B -> Prop) (y z:B) (a:A) (x:set),
114
(set_In a x -> P y) ->
115
(~ set_In a x -> P z) -> P (if set_mem a x then y else z).
118
simple induction x; simpl in |- *; intros.
119
apply H0; red in |- *; trivial.
120
case (Aeq_dec a a0); auto with datatypes.
121
intro; apply H; intros; auto.
122
apply H1; red in |- *; intro.
127
Lemma set_mem_correct1 :
128
forall (a:A) (x:set), set_mem a x = true -> set_In a x.
130
simple induction x; simpl in |- *.
132
intros a0 l; elim (Aeq_dec a a0); auto with datatypes.
135
Lemma set_mem_correct2 :
136
forall (a:A) (x:set), set_In a x -> set_mem a x = true.
138
simple induction x; simpl in |- *.
140
intros a0 l; elim (Aeq_dec a a0); auto with datatypes.
141
intros H1 H2 [H3| H4].
142
absurd (a0 = a); auto with datatypes.
146
Lemma set_mem_complete1 :
147
forall (a:A) (x:set), set_mem a x = false -> ~ set_In a x.
149
simple induction x; simpl in |- *.
151
intros a0 l; elim (Aeq_dec a a0).
152
intros; discriminate H0.
153
unfold not in |- *; intros; elim H1; auto with datatypes.
156
Lemma set_mem_complete2 :
157
forall (a:A) (x:set), ~ set_In a x -> set_mem a x = false.
159
simple induction x; simpl in |- *.
161
intros a0 l; elim (Aeq_dec a a0).
162
intros; elim H0; auto with datatypes.
166
Lemma set_add_intro1 :
167
forall (a b:A) (x:set), set_In a x -> set_In a (set_add b x).
170
unfold set_In in |- *; simple induction x; simpl in |- *.
172
intros a0 l H [Ha0a| Hal].
173
elim (Aeq_dec b a0); left; assumption.
174
elim (Aeq_dec b a0); right; [ assumption | auto with datatypes ].
177
Lemma set_add_intro2 :
178
forall (a b:A) (x:set), a = b -> set_In a (set_add b x).
181
unfold set_In in |- *; simple induction x; simpl in |- *.
185
[ rewrite Hab; intro Hba0; rewrite Hba0; simpl in |- *;
187
| auto with datatypes ].
190
Hint Resolve set_add_intro1 set_add_intro2.
192
Lemma set_add_intro :
193
forall (a b:A) (x:set), a = b \/ set_In a x -> set_In a (set_add b x).
196
intros a b x [H1| H2]; auto with datatypes.
200
forall (a b:A) (x:set), set_In a (set_add b x) -> a = b \/ set_In a x.
203
unfold set_In in |- *.
205
simpl in |- *; intros [H1| H2]; auto with datatypes.
206
simpl in |- *; do 3 intro.
208
simpl in |- *; tauto.
209
simpl in |- *; intros; elim H0.
210
trivial with datatypes.
215
Lemma set_add_elim2 :
216
forall (a b:A) (x:set), set_In a (set_add b x) -> a <> b -> set_In a x.
217
intros a b x H; case (set_add_elim _ _ _ H); intros; trivial.
221
Hint Resolve set_add_intro set_add_elim set_add_elim2.
223
Lemma set_add_not_empty : forall (a:A) (x:set), set_add a x <> empty_set.
225
simple induction x; simpl in |- *.
227
intros; elim (Aeq_dec a a0); intros; discriminate.
231
Lemma set_union_intro1 :
232
forall (a:A) (x y:set), set_In a x -> set_In a (set_union x y).
234
simple induction y; simpl in |- *; auto with datatypes.
237
Lemma set_union_intro2 :
238
forall (a:A) (x y:set), set_In a y -> set_In a (set_union x y).
240
simple induction y; simpl in |- *.
242
intros; elim H0; auto with datatypes.
245
Hint Resolve set_union_intro2 set_union_intro1.
247
Lemma set_union_intro :
248
forall (a:A) (x y:set),
249
set_In a x \/ set_In a y -> set_In a (set_union x y).
251
intros; elim H; auto with datatypes.
254
Lemma set_union_elim :
255
forall (a:A) (x y:set),
256
set_In a (set_union x y) -> set_In a x \/ set_In a y.
258
simple induction y; simpl in |- *.
261
generalize (set_add_elim _ _ _ H0).
267
Lemma set_union_emptyL :
268
forall (a:A) (x:set), set_In a (set_union empty_set x) -> set_In a x.
269
intros a x H; case (set_union_elim _ _ _ H); auto || contradiction.
273
Lemma set_union_emptyR :
274
forall (a:A) (x:set), set_In a (set_union x empty_set) -> set_In a x.
275
intros a x H; case (set_union_elim _ _ _ H); auto || contradiction.
279
Lemma set_inter_intro :
280
forall (a:A) (x y:set),
281
set_In a x -> set_In a y -> set_In a (set_inter x y).
285
simpl in |- *; intros a0 l Hrec y [Ha0a| Hal] Hy.
286
simpl in |- *; rewrite Ha0a.
287
generalize (set_mem_correct1 a y).
288
generalize (set_mem_complete1 a y).
289
elim (set_mem a y); simpl in |- *; intros.
291
absurd (set_In a y); auto with datatypes.
292
elim (set_mem a0 y); [ right; auto with datatypes | auto with datatypes ].
295
Lemma set_inter_elim1 :
296
forall (a:A) (x y:set), set_In a (set_inter x y) -> set_In a x.
300
simpl in |- *; intros a0 l Hrec y.
301
generalize (set_mem_correct1 a0 y).
302
elim (set_mem a0 y); simpl in |- *; intros.
303
elim H0; eauto with datatypes.
304
eauto with datatypes.
307
Lemma set_inter_elim2 :
308
forall (a:A) (x y:set), set_In a (set_inter x y) -> set_In a y.
311
simpl in |- *; tauto.
312
simpl in |- *; intros a0 l Hrec y.
313
generalize (set_mem_correct1 a0 y).
314
elim (set_mem a0 y); simpl in |- *; intros.
316
[ intro Hr; rewrite <- Hr; eauto with datatypes | eauto with datatypes ].
317
eauto with datatypes.
320
Hint Resolve set_inter_elim1 set_inter_elim2.
322
Lemma set_inter_elim :
323
forall (a:A) (x y:set),
324
set_In a (set_inter x y) -> set_In a x /\ set_In a y.
326
eauto with datatypes.
329
Lemma set_diff_intro :
330
forall (a:A) (x y:set),
331
set_In a x -> ~ set_In a y -> set_In a (set_diff x y).
334
simpl in |- *; tauto.
335
simpl in |- *; intros a0 l Hrec y [Ha0a| Hal] Hay.
336
rewrite Ha0a; generalize (set_mem_complete2 _ _ Hay).
338
[ intro Habs; discriminate Habs | auto with datatypes ].
339
elim (set_mem a0 y); auto with datatypes.
342
Lemma set_diff_elim1 :
343
forall (a:A) (x y:set), set_In a (set_diff x y) -> set_In a x.
346
simpl in |- *; tauto.
347
simpl in |- *; intros a0 l Hrec y; elim (set_mem a0 y).
348
eauto with datatypes.
349
intro; generalize (set_add_elim _ _ _ H).
350
intros [H1| H2]; eauto with datatypes.
353
Lemma set_diff_elim2 :
354
forall (a:A) (x y:set), set_In a (set_diff x y) -> ~ set_In a y.
355
intros a x y; elim x; simpl in |- *.
356
intros; contradiction.
358
apply set_mem_ind2; auto.
359
intros H1 H2; case (set_add_elim _ _ _ H2); intros; auto.
363
Lemma set_diff_trivial : forall (a:A) (x:set), ~ set_In a (set_diff x x).
364
red in |- *; intros a x H.
365
apply (set_diff_elim2 _ _ _ H).
366
apply (set_diff_elim1 _ _ _ H).
369
Hint Resolve set_diff_intro set_diff_trivial.
372
End first_definitions.
374
Section other_definitions.
376
Variables A B : Type.
378
Definition set_prod : set A -> set B -> set (A * B) :=
379
list_prod (A:=A) (B:=B).
381
(** [B^A], set of applications from [A] to [B] *)
382
Definition set_power : set A -> set B -> set (set (A * B)) :=
383
list_power (A:=A) (B:=B).
385
Definition set_map : (A -> B) -> set A -> set B := map (A:=A) (B:=B).
387
Definition set_fold_left : (B -> A -> B) -> set A -> B -> B :=
388
fold_left (A:=B) (B:=A).
390
Definition set_fold_right (f:A -> B -> B) (x:set A)
391
(b:B) : B := fold_right f b x.
394
End other_definitions.
396
Unset Implicit Arguments.
added
removed
theories/Lists/ListSet.v
