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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(****************************************************************************)
(* *)
(* Naive Set Theory in Coq *)
(* *)
(* INRIA INRIA *)
(* Rocquencourt Sophia-Antipolis *)
(* *)
(* Coq V6.1 *)
(* *)
(* Gilles Kahn *)
(* Gerard Huet *)
(* *)
(* *)
(* *)
(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *)
(* to the Newton Institute for providing an exceptional work environment *)
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
(*i $Id: Finite_sets_facts.v 8642 2006-03-17 10:09:02Z notin $ i*)
Require Export Finite_sets.
Require Export Constructive_sets.
Require Export Classical_Type.
Require Export Classical_sets.
Require Export Powerset.
Require Export Powerset_facts.
Require Export Powerset_Classical_facts.
Require Export Gt.
Require Export Lt.
Section Finite_sets_facts.
Variable U : Type.
Lemma finite_cardinal :
forall X:Ensemble U, Finite U X -> exists n : nat, cardinal U X n.
Proof.
induction 1 as [| A _ [n H]].
exists 0; auto with sets.
exists (S n); auto with sets.
Qed.
Lemma cardinal_finite :
forall (X:Ensemble U) (n:nat), cardinal U X n -> Finite U X.
Proof.
induction 1; auto with sets.
Qed.
Theorem Add_preserves_Finite :
forall (X:Ensemble U) (x:U), Finite U X -> Finite U (Add U X x).
Proof.
intros X x H'.
elim (classic (In U X x)); intro H'0; auto with sets.
rewrite (Non_disjoint_union U X x); auto with sets.
Qed.
Hint Resolve Add_preserves_Finite.
Theorem Singleton_is_finite : forall x:U, Finite U (Singleton U x).
Proof.
intro x; rewrite <- (Empty_set_zero U (Singleton U x)).
change (Finite U (Add U (Empty_set U) x)) in |- *; auto with sets.
Qed.
Hint Resolve Singleton_is_finite.
Theorem Union_preserves_Finite :
forall X Y:Ensemble U, Finite U X -> Finite U Y -> Finite U (Union U X Y).
Proof.
intros X Y H'; elim H'.
rewrite (Empty_set_zero U Y); auto with sets.
intros A H'0 H'1 x H'2 H'3.
rewrite (Union_commutative U (Add U A x) Y).
rewrite <- (Union_add U Y A x).
rewrite (Union_commutative U Y A); auto with sets.
Qed.
Lemma Finite_downward_closed :
forall A:Ensemble U,
Finite U A -> forall X:Ensemble U, Included U X A -> Finite U X.
Proof.
intros A H'; elim H'; auto with sets.
intros X H'0.
rewrite (less_than_empty U X H'0); auto with sets.
intros; elim Included_Add with U X A0 x; auto with sets.
destruct 1 as [A' [H5 H6]].
rewrite H5; auto with sets.
Qed.
Lemma Intersection_preserves_finite :
forall A:Ensemble U,
Finite U A -> forall X:Ensemble U, Finite U (Intersection U X A).
Proof.
intros A H' X; apply Finite_downward_closed with A; auto with sets.
Qed.
Lemma cardinalO_empty :
forall X:Ensemble U, cardinal U X 0 -> X = Empty_set U.
Proof.
intros X H; apply (cardinal_invert U X 0); trivial with sets.
Qed.
Hint Resolve cardinalO_empty.
Lemma inh_card_gt_O :
forall X:Ensemble U, Inhabited U X -> forall n:nat, cardinal U X n -> n > 0.
Proof.
induction 1 as [x H'].
intros n H'0.
elim (gt_O_eq n); auto with sets.
intro H'1; generalize H'; generalize H'0.
rewrite <- H'1; intro H'2.
rewrite (cardinalO_empty X); auto with sets.
intro H'3; elim H'3.
Qed.
Lemma card_soustr_1 :
forall (X:Ensemble U) (n:nat),
cardinal U X n ->
forall x:U, In U X x -> cardinal U (Subtract U X x) (pred n).
Proof.
intros X n H'; elim H'.
intros x H'0; elim H'0.
clear H' n X.
intros X n H' H'0 x H'1 x0 H'2.
elim (classic (In U X x0)).
intro H'4; rewrite (add_soustr_xy U X x x0).
elim (classic (x = x0)).
intro H'5.
absurd (In U X x0); auto with sets.
rewrite <- H'5; auto with sets.
intro H'3; try assumption.
cut (S (pred n) = pred (S n)).
intro H'5; rewrite <- H'5.
apply card_add; auto with sets.
red in |- *; intro H'6; elim H'6.
intros H'7 H'8; try assumption.
elim H'1; auto with sets.
unfold pred at 2 in |- *; symmetry in |- *.
apply S_pred with (m := 0).
change (n > 0) in |- *.
apply inh_card_gt_O with (X := X); auto with sets.
apply Inhabited_intro with (x := x0); auto with sets.
red in |- *; intro H'3.
apply H'1.
elim H'3; auto with sets.
rewrite H'3; auto with sets.
elim (classic (x = x0)).
intro H'3; rewrite <- H'3.
cut (Subtract U (Add U X x) x = X); auto with sets.
intro H'4; rewrite H'4; auto with sets.
intros H'3 H'4; try assumption.
absurd (In U (Add U X x) x0); auto with sets.
red in |- *; intro H'5; try exact H'5.
lapply (Add_inv U X x x0); tauto.
Qed.
Lemma cardinal_is_functional :
forall (X:Ensemble U) (c1:nat),
cardinal U X c1 ->
forall (Y:Ensemble U) (c2:nat), cardinal U Y c2 -> X = Y -> c1 = c2.
Proof.
intros X c1 H'; elim H'.
intros Y c2 H'0; elim H'0; auto with sets.
intros A n H'1 H'2 x H'3 H'5.
elim (not_Empty_Add U A x); auto with sets.
clear H' c1 X.
intros X n H' H'0 x H'1 Y c2 H'2.
elim H'2.
intro H'3.
elim (not_Empty_Add U X x); auto with sets.
clear H'2 c2 Y.
intros X0 c2 H'2 H'3 x0 H'4 H'5.
elim (classic (In U X0 x)).
intro H'6; apply f_equal with nat.
apply H'0 with (Y := Subtract U (Add U X0 x0) x).
elimtype (pred (S c2) = c2); auto with sets.
apply card_soustr_1; auto with sets.
rewrite <- H'5.
apply Sub_Add_new; auto with sets.
elim (classic (x = x0)).
intros H'6 H'7; apply f_equal with nat.
apply H'0 with (Y := X0); auto with sets.
apply Simplify_add with (x := x); auto with sets.
pattern x at 2 in |- *; rewrite H'6; auto with sets.
intros H'6 H'7.
absurd (Add U X x = Add U X0 x0); auto with sets.
clear H'0 H' H'3 n H'5 H'4 H'2 H'1 c2.
red in |- *; intro H'.
lapply (Extension U (Add U X x) (Add U X0 x0)); auto with sets.
clear H'.
intro H'; red in H'.
elim H'; intros H'0 H'1; red in H'0; clear H' H'1.
absurd (In U (Add U X0 x0) x); auto with sets.
lapply (Add_inv U X0 x0 x); [ intuition | apply (H'0 x); apply Add_intro2 ].
Qed.
Lemma cardinal_Empty : forall m:nat, cardinal U (Empty_set U) m -> 0 = m.
Proof.
intros m Cm; generalize (cardinal_invert U (Empty_set U) m Cm).
elim m; auto with sets.
intros; elim H0; intros; elim H1; intros; elim H2; intros.
elim (not_Empty_Add U x x0 H3).
Qed.
Lemma cardinal_unicity :
forall (X:Ensemble U) (n:nat),
cardinal U X n -> forall m:nat, cardinal U X m -> n = m.
Proof.
intros; apply cardinal_is_functional with X X; auto with sets.
Qed.
Lemma card_Add_gen :
forall (A:Ensemble U) (x:U) (n n':nat),
cardinal U A n -> cardinal U (Add U A x) n' -> n' <= S n.
Proof.
intros A x n n' H'.
elim (classic (In U A x)).
intro H'0.
rewrite (Non_disjoint_union U A x H'0).
intro H'1; cut (n = n').
intro E; rewrite E; auto with sets.
apply cardinal_unicity with A; auto with sets.
intros H'0 H'1.
cut (n' = S n).
intro E; rewrite E; auto with sets.
apply cardinal_unicity with (Add U A x); auto with sets.
Qed.
Lemma incl_st_card_lt :
forall (X:Ensemble U) (c1:nat),
cardinal U X c1 ->
forall (Y:Ensemble U) (c2:nat),
cardinal U Y c2 -> Strict_Included U X Y -> c2 > c1.
Proof.
intros X c1 H'; elim H'.
intros Y c2 H'0; elim H'0; auto with sets arith.
intro H'1.
elim (Strict_Included_strict U (Empty_set U)); auto with sets arith.
clear H' c1 X.
intros X n H' H'0 x H'1 Y c2 H'2.
elim H'2.
intro H'3; elim (not_SIncl_empty U (Add U X x)); auto with sets arith.
clear H'2 c2 Y.
intros X0 c2 H'2 H'3 x0 H'4 H'5; elim (classic (In U X0 x)).
intro H'6; apply gt_n_S.
apply H'0 with (Y := Subtract U (Add U X0 x0) x).
elimtype (pred (S c2) = c2); auto with sets arith.
apply card_soustr_1; auto with sets arith.
apply incl_st_add_soustr; auto with sets arith.
elim (classic (x = x0)).
intros H'6 H'7; apply gt_n_S.
apply H'0 with (Y := X0); auto with sets arith.
apply sincl_add_x with (x := x0).
rewrite <- H'6; auto with sets arith.
pattern x0 at 1 in |- *; rewrite <- H'6; trivial with sets arith.
intros H'6 H'7; red in H'5.
elim H'5; intros H'8 H'9; try exact H'8; clear H'5.
red in H'8.
generalize (H'8 x).
intro H'5; lapply H'5; auto with sets arith.
intro H; elim Add_inv with U X0 x0 x; auto with sets arith.
intro; absurd (In U X0 x); auto with sets arith.
intro; absurd (x = x0); auto with sets arith.
Qed.
Lemma incl_card_le :
forall (X Y:Ensemble U) (n m:nat),
cardinal U X n -> cardinal U Y m -> Included U X Y -> n <= m.
Proof.
intros; elim Included_Strict_Included with U X Y; auto with sets arith; intro.
cut (m > n); auto with sets arith.
apply incl_st_card_lt with (X := X) (Y := Y); auto with sets arith.
generalize H0; rewrite <- H2; intro.
cut (n = m).
intro E; rewrite E; auto with sets arith.
apply cardinal_unicity with X; auto with sets arith.
Qed.
Lemma G_aux :
forall P:Ensemble U -> Prop,
(forall X:Ensemble U,
Finite U X ->
(forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
P (Empty_set U).
Proof.
intros P H'; try assumption.
apply H'; auto with sets.
clear H'; auto with sets.
intros Y H'; try assumption.
red in H'.
elim H'; intros H'0 H'1; try exact H'1; clear H'.
lapply (less_than_empty U Y); [ intro H'3; try exact H'3 | assumption ].
elim H'1; auto with sets.
Qed.
Hint Unfold not.
Lemma Generalized_induction_on_finite_sets :
forall P:Ensemble U -> Prop,
(forall X:Ensemble U,
Finite U X ->
(forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
forall X:Ensemble U, Finite U X -> P X.
Proof.
intros P H'0 X H'1.
generalize P H'0; clear H'0 P.
elim H'1.
intros P H'0.
apply G_aux; auto with sets.
clear H'1 X.
intros A H' H'0 x H'1 P H'3.
cut (forall Y:Ensemble U, Included U Y (Add U A x) -> P Y); auto with sets.
generalize H'1.
apply H'0.
intros X K H'5 L Y H'6; apply H'3; auto with sets.
apply Finite_downward_closed with (A := Add U X x); auto with sets.
intros Y0 H'7.
elim (Strict_inclusion_is_transitive_with_inclusion U Y0 Y (Add U X x));
auto with sets.
intros H'2 H'4.
elim (Included_Add U Y0 X x);
[ intro H'14
| intro H'14; elim H'14; intros A' E; elim E; intros H'15 H'16; clear E H'14
| idtac ]; auto with sets.
elim (Included_Strict_Included U Y0 X); auto with sets.
intro H'9; apply H'5 with (Y := Y0); auto with sets.
intro H'9; rewrite H'9.
apply H'3; auto with sets.
intros Y1 H'8; elim H'8.
intros H'10 H'11; apply H'5 with (Y := Y1); auto with sets.
elim (Included_Strict_Included U A' X); auto with sets.
intro H'8; apply H'5 with (Y := A'); auto with sets.
rewrite <- H'15; auto with sets.
intro H'8.
elim H'7.
intros H'9 H'10; apply H'10 || elim H'10; try assumption.
generalize H'6.
rewrite <- H'8.
rewrite <- H'15; auto with sets.
Qed.
End Finite_sets_facts.
|
