1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id$ i*)
(** A Library for finite sets, implemented as lists *)
(** List is loaded, but not exported.
This allow to "hide" the definitions, functions and theorems of List
and to see only the ones of ListSet *)
Require Import List.
Set Implicit Arguments.
Section first_definitions.
Variable A : Type.
Hypothesis Aeq_dec : forall x y:A, {x = y} + {x <> y}.
Definition set := list A.
Definition empty_set : set := nil.
Fixpoint set_add (a:A) (x:set) : set :=
match x with
| nil => a :: nil
| a1 :: x1 =>
match Aeq_dec a a1 with
| left _ => a1 :: x1
| right _ => a1 :: set_add a x1
end
end.
Fixpoint set_mem (a:A) (x:set) : bool :=
match x with
| nil => false
| a1 :: x1 =>
match Aeq_dec a a1 with
| left _ => true
| right _ => set_mem a x1
end
end.
(** If [a] belongs to [x], removes [a] from [x]. If not, does nothing *)
Fixpoint set_remove (a:A) (x:set) : set :=
match x with
| nil => empty_set
| a1 :: x1 =>
match Aeq_dec a a1 with
| left _ => x1
| right _ => a1 :: set_remove a x1
end
end.
Fixpoint set_inter (x:set) : set -> set :=
match x with
| nil => fun y => nil
| a1 :: x1 =>
fun y =>
if set_mem a1 y then a1 :: set_inter x1 y else set_inter x1 y
end.
Fixpoint set_union (x y:set) : set :=
match y with
| nil => x
| a1 :: y1 => set_add a1 (set_union x y1)
end.
(** returns the set of all els of [x] that does not belong to [y] *)
Fixpoint set_diff (x y:set) : set :=
match x with
| nil => nil
| a1 :: x1 =>
if set_mem a1 y then set_diff x1 y else set_add a1 (set_diff x1 y)
end.
Definition set_In : A -> set -> Prop := In (A:=A).
Lemma set_In_dec : forall (a:A) (x:set), {set_In a x} + {~ set_In a x}.
Proof.
unfold set_In in |- *.
(*** Realizer set_mem. Program_all. ***)
simple induction x.
auto.
intros a0 x0 Ha0. case (Aeq_dec a a0); intro eq.
rewrite eq; simpl in |- *; auto with datatypes.
elim Ha0.
auto with datatypes.
right; simpl in |- *; unfold not in |- *; intros [Hc1| Hc2];
auto with datatypes.
Qed.
Lemma set_mem_ind :
forall (B:Type) (P:B -> Prop) (y z:B) (a:A) (x:set),
(set_In a x -> P y) -> P z -> P (if set_mem a x then y else z).
Proof.
simple induction x; simpl in |- *; intros.
assumption.
elim (Aeq_dec a a0); auto with datatypes.
Qed.
Lemma set_mem_ind2 :
forall (B:Type) (P:B -> Prop) (y z:B) (a:A) (x:set),
(set_In a x -> P y) ->
(~ set_In a x -> P z) -> P (if set_mem a x then y else z).
Proof.
simple induction x; simpl in |- *; intros.
apply H0; red in |- *; trivial.
case (Aeq_dec a a0); auto with datatypes.
intro; apply H; intros; auto.
apply H1; red in |- *; intro.
case H3; auto.
Qed.
Lemma set_mem_correct1 :
forall (a:A) (x:set), set_mem a x = true -> set_In a x.
Proof.
simple induction x; simpl in |- *.
discriminate.
intros a0 l; elim (Aeq_dec a a0); auto with datatypes.
Qed.
Lemma set_mem_correct2 :
forall (a:A) (x:set), set_In a x -> set_mem a x = true.
Proof.
simple induction x; simpl in |- *.
intro Ha; elim Ha.
intros a0 l; elim (Aeq_dec a a0); auto with datatypes.
intros H1 H2 [H3| H4].
absurd (a0 = a); auto with datatypes.
auto with datatypes.
Qed.
Lemma set_mem_complete1 :
forall (a:A) (x:set), set_mem a x = false -> ~ set_In a x.
Proof.
simple induction x; simpl in |- *.
tauto.
intros a0 l; elim (Aeq_dec a a0).
intros; discriminate H0.
unfold not in |- *; intros; elim H1; auto with datatypes.
Qed.
Lemma set_mem_complete2 :
forall (a:A) (x:set), ~ set_In a x -> set_mem a x = false.
Proof.
simple induction x; simpl in |- *.
tauto.
intros a0 l; elim (Aeq_dec a a0).
intros; elim H0; auto with datatypes.
tauto.
Qed.
Lemma set_add_intro1 :
forall (a b:A) (x:set), set_In a x -> set_In a (set_add b x).
Proof.
unfold set_In in |- *; simple induction x; simpl in |- *.
auto with datatypes.
intros a0 l H [Ha0a| Hal].
elim (Aeq_dec b a0); left; assumption.
elim (Aeq_dec b a0); right; [ assumption | auto with datatypes ].
Qed.
Lemma set_add_intro2 :
forall (a b:A) (x:set), a = b -> set_In a (set_add b x).
Proof.
unfold set_In in |- *; simple induction x; simpl in |- *.
auto with datatypes.
intros a0 l H Hab.
elim (Aeq_dec b a0);
[ rewrite Hab; intro Hba0; rewrite Hba0; simpl in |- *;
auto with datatypes
| auto with datatypes ].
Qed.
Hint Resolve set_add_intro1 set_add_intro2.
Lemma set_add_intro :
forall (a b:A) (x:set), a = b \/ set_In a x -> set_In a (set_add b x).
Proof.
intros a b x [H1| H2]; auto with datatypes.
Qed.
Lemma set_add_elim :
forall (a b:A) (x:set), set_In a (set_add b x) -> a = b \/ set_In a x.
Proof.
unfold set_In in |- *.
simple induction x.
simpl in |- *; intros [H1| H2]; auto with datatypes.
simpl in |- *; do 3 intro.
elim (Aeq_dec b a0).
simpl in |- *; tauto.
simpl in |- *; intros; elim H0.
trivial with datatypes.
tauto.
tauto.
Qed.
Lemma set_add_elim2 :
forall (a b:A) (x:set), set_In a (set_add b x) -> a <> b -> set_In a x.
intros a b x H; case (set_add_elim _ _ _ H); intros; trivial.
case H1; trivial.
Qed.
Hint Resolve set_add_intro set_add_elim set_add_elim2.
Lemma set_add_not_empty : forall (a:A) (x:set), set_add a x <> empty_set.
Proof.
simple induction x; simpl in |- *.
discriminate.
intros; elim (Aeq_dec a a0); intros; discriminate.
Qed.
Lemma set_union_intro1 :
forall (a:A) (x y:set), set_In a x -> set_In a (set_union x y).
Proof.
simple induction y; simpl in |- *; auto with datatypes.
Qed.
Lemma set_union_intro2 :
forall (a:A) (x y:set), set_In a y -> set_In a (set_union x y).
Proof.
simple induction y; simpl in |- *.
tauto.
intros; elim H0; auto with datatypes.
Qed.
Hint Resolve set_union_intro2 set_union_intro1.
Lemma set_union_intro :
forall (a:A) (x y:set),
set_In a x \/ set_In a y -> set_In a (set_union x y).
Proof.
intros; elim H; auto with datatypes.
Qed.
Lemma set_union_elim :
forall (a:A) (x y:set),
set_In a (set_union x y) -> set_In a x \/ set_In a y.
Proof.
simple induction y; simpl in |- *.
auto with datatypes.
intros.
generalize (set_add_elim _ _ _ H0).
intros [H1| H1].
auto with datatypes.
tauto.
Qed.
Lemma set_union_emptyL :
forall (a:A) (x:set), set_In a (set_union empty_set x) -> set_In a x.
intros a x H; case (set_union_elim _ _ _ H); auto || contradiction.
Qed.
Lemma set_union_emptyR :
forall (a:A) (x:set), set_In a (set_union x empty_set) -> set_In a x.
intros a x H; case (set_union_elim _ _ _ H); auto || contradiction.
Qed.
Lemma set_inter_intro :
forall (a:A) (x y:set),
set_In a x -> set_In a y -> set_In a (set_inter x y).
Proof.
simple induction x.
auto with datatypes.
simpl in |- *; intros a0 l Hrec y [Ha0a| Hal] Hy.
simpl in |- *; rewrite Ha0a.
generalize (set_mem_correct1 a y).
generalize (set_mem_complete1 a y).
elim (set_mem a y); simpl in |- *; intros.
auto with datatypes.
absurd (set_In a y); auto with datatypes.
elim (set_mem a0 y); [ right; auto with datatypes | auto with datatypes ].
Qed.
Lemma set_inter_elim1 :
forall (a:A) (x y:set), set_In a (set_inter x y) -> set_In a x.
Proof.
simple induction x.
auto with datatypes.
simpl in |- *; intros a0 l Hrec y.
generalize (set_mem_correct1 a0 y).
elim (set_mem a0 y); simpl in |- *; intros.
elim H0; eauto with datatypes.
eauto with datatypes.
Qed.
Lemma set_inter_elim2 :
forall (a:A) (x y:set), set_In a (set_inter x y) -> set_In a y.
Proof.
simple induction x.
simpl in |- *; tauto.
simpl in |- *; intros a0 l Hrec y.
generalize (set_mem_correct1 a0 y).
elim (set_mem a0 y); simpl in |- *; intros.
elim H0;
[ intro Hr; rewrite <- Hr; eauto with datatypes | eauto with datatypes ].
eauto with datatypes.
Qed.
Hint Resolve set_inter_elim1 set_inter_elim2.
Lemma set_inter_elim :
forall (a:A) (x y:set),
set_In a (set_inter x y) -> set_In a x /\ set_In a y.
Proof.
eauto with datatypes.
Qed.
Lemma set_diff_intro :
forall (a:A) (x y:set),
set_In a x -> ~ set_In a y -> set_In a (set_diff x y).
Proof.
simple induction x.
simpl in |- *; tauto.
simpl in |- *; intros a0 l Hrec y [Ha0a| Hal] Hay.
rewrite Ha0a; generalize (set_mem_complete2 _ _ Hay).
elim (set_mem a y);
[ intro Habs; discriminate Habs | auto with datatypes ].
elim (set_mem a0 y); auto with datatypes.
Qed.
Lemma set_diff_elim1 :
forall (a:A) (x y:set), set_In a (set_diff x y) -> set_In a x.
Proof.
simple induction x.
simpl in |- *; tauto.
simpl in |- *; intros a0 l Hrec y; elim (set_mem a0 y).
eauto with datatypes.
intro; generalize (set_add_elim _ _ _ H).
intros [H1| H2]; eauto with datatypes.
Qed.
Lemma set_diff_elim2 :
forall (a:A) (x y:set), set_In a (set_diff x y) -> ~ set_In a y.
intros a x y; elim x; simpl in |- *.
intros; contradiction.
intros a0 l Hrec.
apply set_mem_ind2; auto.
intros H1 H2; case (set_add_elim _ _ _ H2); intros; auto.
rewrite H; trivial.
Qed.
Lemma set_diff_trivial : forall (a:A) (x:set), ~ set_In a (set_diff x x).
red in |- *; intros a x H.
apply (set_diff_elim2 _ _ _ H).
apply (set_diff_elim1 _ _ _ H).
Qed.
Hint Resolve set_diff_intro set_diff_trivial.
End first_definitions.
Section other_definitions.
Definition set_prod : forall {A B:Type}, set A -> set B -> set (A * B) :=
list_prod.
(** [B^A], set of applications from [A] to [B] *)
Definition set_power : forall {A B:Type}, set A -> set B -> set (set (A * B)) :=
list_power.
Definition set_fold_left {A B:Type} : (B -> A -> B) -> set A -> B -> B :=
fold_left (A:=B) (B:=A).
Definition set_fold_right {A B:Type} (f:A -> B -> B) (x:set A)
(b:B) : B := fold_right f b x.
Definition set_map {A B:Type} (Aeq_dec : forall x y:B, {x = y} + {x <> y})
(f : A -> B) (x : set A) : set B :=
set_fold_right (fun a => set_add Aeq_dec (f a)) x (empty_set B).
End other_definitions.
Unset Implicit Arguments.
|
