← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/Sets/Finite_sets_facts.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/Sets/Finite_sets_facts.v
 
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
(************************************************************************)
 
8
(****************************************************************************)
 
9
(*                                                                          *)
 
10
(*                         Naive Set Theory in Coq                          *)
 
11
(*                                                                          *)
 
12
(*                     INRIA                        INRIA                   *)
 
13
(*              Rocquencourt                        Sophia-Antipolis        *)
 
14
(*                                                                          *)
 
15
(*                                 Coq V6.1                                 *)
 
16
(*                                                                          *)
 
17
(*                               Gilles Kahn                                *)
 
18
(*                               Gerard Huet                                *)
 
19
(*                                                                          *)
 
20
(*                                                                          *)
 
21
(*                                                                          *)
 
22
(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks  *)
 
23
(* to the Newton Institute for providing an exceptional work environment    *)
 
24
(* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 
25
(****************************************************************************)
 
26
 
 
27
(*i $Id: Finite_sets_facts.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
28
 
 
29
Require Export Finite_sets.
 
30
Require Export Constructive_sets.
 
31
Require Export Classical_Type.
 
32
Require Export Classical_sets.
 
33
Require Export Powerset.
 
34
Require Export Powerset_facts.
 
35
Require Export Powerset_Classical_facts.
 
36
Require Export Gt.
 
37
Require Export Lt.
 
38
 
 
39
Section Finite_sets_facts.
 
40
  Variable U : Type.
 
41
 
 
42
  Lemma finite_cardinal :
 
43
    forall X:Ensemble U, Finite U X ->  exists n : nat, cardinal U X n.
 
44
  Proof.
 
45
    induction 1 as [| A _ [n H]].
 
46
    exists 0; auto with sets.
 
47
    exists (S n); auto with sets.
 
48
  Qed.
 
49
 
 
50
  Lemma cardinal_finite :
 
51
    forall (X:Ensemble U) (n:nat), cardinal U X n -> Finite U X.
 
52
  Proof.
 
53
    induction 1; auto with sets.
 
54
  Qed.
 
55
 
 
56
  Theorem Add_preserves_Finite :
 
57
    forall (X:Ensemble U) (x:U), Finite U X -> Finite U (Add U X x).
 
58
  Proof.
 
59
    intros X x H'.
 
60
    elim (classic (In U X x)); intro H'0; auto with sets.
 
61
    rewrite (Non_disjoint_union U X x); auto with sets.
 
62
  Qed.
 
63
 
 
64
  Theorem Singleton_is_finite : forall x:U, Finite U (Singleton U x).
 
65
  Proof.
 
66
    intro x; rewrite <- (Empty_set_zero U (Singleton U x)).
 
67
    change (Finite U (Add U (Empty_set U) x)) in |- *; auto with sets.
 
68
  Qed.
 
69
 
 
70
  Theorem Union_preserves_Finite :
 
71
    forall X Y:Ensemble U, Finite U X -> Finite U Y -> Finite U (Union U X Y).
 
72
  Proof.
 
73
    intros X Y H; induction H as [|A Fin_A Hind x].
 
74
    rewrite (Empty_set_zero U Y). trivial.
 
75
    intros. 
 
76
    rewrite (Union_commutative U (Add U A x) Y).
 
77
    rewrite <- (Union_add U Y A x).
 
78
    rewrite (Union_commutative U Y A).
 
79
    apply Add_preserves_Finite.
 
80
    apply Hind. assumption.
 
81
  Qed.
 
82
 
 
83
  Lemma Finite_downward_closed :
 
84
    forall A:Ensemble U,
 
85
      Finite U A -> forall X:Ensemble U, Included U X A -> Finite U X.
 
86
  Proof.
 
87
    intros A H'; elim H'; auto with sets.
 
88
    intros X H'0.
 
89
    rewrite (less_than_empty U X H'0); auto with sets.
 
90
    intros; elim Included_Add with U X A0 x; auto with sets.
 
91
    destruct 1 as [A' [H5 H6]].
 
92
    rewrite H5; auto with sets.
 
93
  Qed.
 
94
 
 
95
  Lemma Intersection_preserves_finite :
 
96
    forall A:Ensemble U,
 
97
      Finite U A -> forall X:Ensemble U, Finite U (Intersection U X A).
 
98
  Proof.
 
99
    intros A H' X; apply Finite_downward_closed with A; auto with sets.
 
100
  Qed.
 
101
  
 
102
  Lemma cardinalO_empty :
 
103
    forall X:Ensemble U, cardinal U X 0 -> X = Empty_set U.
 
104
  Proof.
 
105
    intros X H; apply (cardinal_invert U X 0); trivial with sets.
 
106
  Qed.
 
107
 
 
108
  Lemma inh_card_gt_O :
 
109
    forall X:Ensemble U, Inhabited U X -> forall n:nat, cardinal U X n -> n > 0.
 
110
  Proof.
 
111
    induction 1 as [x H'].
 
112
    intros n H'0.
 
113
    elim (gt_O_eq n); auto with sets.
 
114
    intro H'1; generalize H'; generalize H'0.
 
115
    rewrite <- H'1; intro H'2.
 
116
    rewrite (cardinalO_empty X); auto with sets.
 
117
    intro H'3; elim H'3.
 
118
  Qed.
 
119
 
 
120
  Lemma card_soustr_1 :
 
121
    forall (X:Ensemble U) (n:nat),
 
122
      cardinal U X n ->
 
123
      forall x:U, In U X x -> cardinal U (Subtract U X x) (pred n).
 
124
  Proof.
 
125
    intros X n H'; elim H'.
 
126
    intros x H'0; elim H'0.
 
127
    clear H' n X.
 
128
    intros X n H' H'0 x H'1 x0 H'2.
 
129
    elim (classic (In U X x0)).
 
130
    intro H'4; rewrite (add_soustr_xy U X x x0).
 
131
    elim (classic (x = x0)).
 
132
    intro H'5.
 
133
    absurd (In U X x0); auto with sets.
 
134
    rewrite <- H'5; auto with sets.
 
135
    intro H'3; try assumption.
 
136
    cut (S (pred n) = pred (S n)).
 
137
    intro H'5; rewrite <- H'5.
 
138
    apply card_add; auto with sets.
 
139
    red in |- *; intro H'6; elim H'6.
 
140
    intros H'7 H'8; try assumption.
 
141
    elim H'1; auto with sets.
 
142
    unfold pred at 2 in |- *; symmetry  in |- *.
 
143
    apply S_pred with (m := 0).
 
144
    change (n > 0) in |- *.
 
145
    apply inh_card_gt_O with (X := X); auto with sets.
 
146
    apply Inhabited_intro with (x := x0); auto with sets.
 
147
    red in |- *; intro H'3.
 
148
    apply H'1.
 
149
    elim H'3; auto with sets.
 
150
    rewrite H'3; auto with sets.
 
151
    elim (classic (x = x0)).
 
152
    intro H'3; rewrite <- H'3.
 
153
    cut (Subtract U (Add U X x) x = X); auto with sets.
 
154
    intro H'4; rewrite H'4; auto with sets.
 
155
    intros H'3 H'4; try assumption.
 
156
    absurd (In U (Add U X x) x0); auto with sets.
 
157
    red in |- *; intro H'5; try exact H'5.
 
158
    lapply (Add_inv U X x x0); tauto.
 
159
  Qed.
 
160
 
 
161
  Lemma cardinal_is_functional :
 
162
    forall (X:Ensemble U) (c1:nat),
 
163
      cardinal U X c1 ->
 
164
      forall (Y:Ensemble U) (c2:nat), cardinal U Y c2 -> X = Y -> c1 = c2.
 
165
  Proof.
 
166
    intros X c1 H'; elim H'.
 
167
    intros Y c2 H'0; elim H'0; auto with sets.
 
168
    intros A n H'1 H'2 x H'3 H'5.
 
169
    elim (not_Empty_Add U A x); auto with sets.
 
170
    clear H' c1 X.
 
171
    intros X n H' H'0 x H'1 Y c2 H'2.
 
172
    elim H'2.
 
173
    intro H'3.
 
174
    elim (not_Empty_Add U X x); auto with sets.
 
175
    clear H'2 c2 Y.
 
176
    intros X0 c2 H'2 H'3 x0 H'4 H'5.
 
177
    elim (classic (In U X0 x)).
 
178
    intro H'6; apply f_equal with nat.
 
179
    apply H'0 with (Y := Subtract U (Add U X0 x0) x).
 
180
    elimtype (pred (S c2) = c2); auto with sets.
 
181
    apply card_soustr_1; auto with sets.
 
182
    rewrite <- H'5.
 
183
    apply Sub_Add_new; auto with sets.
 
184
    elim (classic (x = x0)).
 
185
    intros H'6 H'7; apply f_equal with nat.
 
186
    apply H'0 with (Y := X0); auto with sets.
 
187
    apply Simplify_add with (x := x); auto with sets.
 
188
    pattern x at 2 in |- *; rewrite H'6; auto with sets.
 
189
    intros H'6 H'7.
 
190
    absurd (Add U X x = Add U X0 x0); auto with sets.
 
191
    clear H'0 H' H'3 n H'5 H'4 H'2 H'1 c2.
 
192
    red in |- *; intro H'.
 
193
    lapply (Extension U (Add U X x) (Add U X0 x0)); auto with sets.
 
194
    clear H'.
 
195
    intro H'; red in H'.
 
196
    elim H'; intros H'0 H'1; red in H'0; clear H' H'1.
 
197
    absurd (In U (Add U X0 x0) x); auto with sets.
 
198
    lapply (Add_inv U X0 x0 x); [ intuition | apply (H'0 x); apply Add_intro2 ].
 
199
  Qed.
 
200
 
 
201
  Lemma cardinal_Empty : forall m:nat, cardinal U (Empty_set U) m -> 0 = m.
 
202
  Proof.
 
203
    intros m Cm; generalize (cardinal_invert U (Empty_set U) m Cm).
 
204
    elim m; auto with sets.
 
205
    intros; elim H0; intros; elim H1; intros; elim H2; intros.
 
206
    elim (not_Empty_Add U x x0 H3).
 
207
  Qed.
 
208
 
 
209
  Lemma cardinal_unicity :
 
210
    forall (X:Ensemble U) (n:nat),
 
211
      cardinal U X n -> forall m:nat, cardinal U X m -> n = m.
 
212
  Proof.
 
213
    intros; apply cardinal_is_functional with X X; auto with sets.
 
214
  Qed.
 
215
  
 
216
  Lemma card_Add_gen :
 
217
    forall (A:Ensemble U) (x:U) (n n':nat),
 
218
      cardinal U A n -> cardinal U (Add U A x) n' -> n' <= S n.
 
219
  Proof.
 
220
    intros A x n n' H'.
 
221
    elim (classic (In U A x)).
 
222
    intro H'0.
 
223
    rewrite (Non_disjoint_union U A x H'0).
 
224
    intro H'1; cut (n = n').
 
225
    intro E; rewrite E; auto with sets.
 
226
    apply cardinal_unicity with A; auto with sets.
 
227
    intros H'0 H'1.
 
228
    cut (n' = S n).
 
229
    intro E; rewrite E; auto with sets.
 
230
    apply cardinal_unicity with (Add U A x); auto with sets.
 
231
  Qed.
 
232
 
 
233
  Lemma incl_st_card_lt :
 
234
    forall (X:Ensemble U) (c1:nat),
 
235
      cardinal U X c1 ->
 
236
      forall (Y:Ensemble U) (c2:nat),
 
237
        cardinal U Y c2 -> Strict_Included U X Y -> c2 > c1.
 
238
  Proof.
 
239
    intros X c1 H'; elim H'.
 
240
    intros Y c2 H'0; elim H'0; auto with sets arith.
 
241
    intro H'1.
 
242
    elim (Strict_Included_strict U (Empty_set U)); auto with sets arith.
 
243
    clear H' c1 X.
 
244
    intros X n H' H'0 x H'1 Y c2 H'2.
 
245
    elim H'2.
 
246
    intro H'3; elim (not_SIncl_empty U (Add U X x)); auto with sets arith.
 
247
    clear H'2 c2 Y.
 
248
    intros X0 c2 H'2 H'3 x0 H'4 H'5; elim (classic (In U X0 x)).
 
249
    intro H'6; apply gt_n_S.
 
250
    apply H'0 with (Y := Subtract U (Add U X0 x0) x).
 
251
    elimtype (pred (S c2) = c2); auto with sets arith.
 
252
    apply card_soustr_1; auto with sets arith.
 
253
    apply incl_st_add_soustr; auto with sets arith.
 
254
    elim (classic (x = x0)).
 
255
    intros H'6 H'7; apply gt_n_S.
 
256
    apply H'0 with (Y := X0); auto with sets arith.
 
257
    apply sincl_add_x with (x := x0).
 
258
    rewrite <- H'6; auto with sets arith.
 
259
    pattern x0 at 1 in |- *; rewrite <- H'6; trivial with sets arith.
 
260
    intros H'6 H'7; red in H'5.
 
261
    elim H'5; intros H'8 H'9; try exact H'8; clear H'5.
 
262
    red in H'8.
 
263
    generalize (H'8 x).
 
264
    intro H'5; lapply H'5; auto with sets arith.
 
265
    intro H; elim Add_inv with U X0 x0 x; auto with sets arith.
 
266
    intro; absurd (In U X0 x); auto with sets arith.
 
267
    intro; absurd (x = x0); auto with sets arith.
 
268
  Qed.
 
269
 
 
270
  Lemma incl_card_le :
 
271
    forall (X Y:Ensemble U) (n m:nat),
 
272
      cardinal U X n -> cardinal U Y m -> Included U X Y -> n <= m.
 
273
  Proof.
 
274
    intros; elim Included_Strict_Included with U X Y; auto with sets arith; intro.
 
275
    cut (m > n); auto with sets arith.
 
276
    apply incl_st_card_lt with (X := X) (Y := Y); auto with sets arith.
 
277
    generalize H0; rewrite <- H2; intro.
 
278
    cut (n = m).
 
279
    intro E; rewrite E; auto with sets arith.
 
280
    apply cardinal_unicity with X; auto with sets arith.
 
281
  Qed.
 
282
  
 
283
  Lemma G_aux :
 
284
    forall P:Ensemble U -> Prop,
 
285
      (forall X:Ensemble U,
 
286
        Finite U X ->
 
287
        (forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
 
288
      P (Empty_set U).
 
289
  Proof.
 
290
    intros P H'; try assumption.
 
291
    apply H'; auto with sets.
 
292
    clear H'; auto with sets.
 
293
    intros Y H'; try assumption.
 
294
    red in H'.
 
295
    elim H'; intros H'0 H'1; try exact H'1; clear H'.
 
296
    lapply (less_than_empty U Y); [ intro H'3; try exact H'3 | assumption ].
 
297
    elim H'1; auto with sets.
 
298
  Qed.
 
299
 
 
300
  Lemma Generalized_induction_on_finite_sets :
 
301
    forall P:Ensemble U -> Prop,
 
302
      (forall X:Ensemble U,
 
303
        Finite U X ->
 
304
        (forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
 
305
      forall X:Ensemble U, Finite U X -> P X.
 
306
  Proof.
 
307
    intros P H'0 X H'1.
 
308
    generalize P H'0; clear H'0 P.
 
309
    elim H'1.
 
310
    intros P H'0.
 
311
    apply G_aux; auto with sets.
 
312
    clear H'1 X.
 
313
    intros A H' H'0 x H'1 P H'3.
 
314
    cut (forall Y:Ensemble U, Included U Y (Add U A x) -> P Y); auto with sets.
 
315
    generalize H'1.
 
316
    apply H'0.
 
317
    intros X K H'5 L Y H'6; apply H'3; auto with sets.
 
318
    apply Finite_downward_closed with (A := Add U X x); auto with sets.
 
319
    intros Y0 H'7.
 
320
    elim (Strict_inclusion_is_transitive_with_inclusion U Y0 Y (Add U X x));
 
321
      auto with sets.
 
322
    intros H'2 H'4.
 
323
    elim (Included_Add U Y0 X x);
 
324
      [ intro H'14
 
325
        | intro H'14; elim H'14; intros A' E; elim E; intros H'15 H'16; clear E H'14
 
326
        | idtac ]; auto with sets.
 
327
    elim (Included_Strict_Included U Y0 X); auto with sets.
 
328
    intro H'9; apply H'5 with (Y := Y0); auto with sets.
 
329
    intro H'9; rewrite H'9.
 
330
    apply H'3; auto with sets.
 
331
    intros Y1 H'8; elim H'8.
 
332
    intros H'10 H'11; apply H'5 with (Y := Y1); auto with sets.
 
333
    elim (Included_Strict_Included U A' X); auto with sets.
 
334
    intro H'8; apply H'5 with (Y := A'); auto with sets.
 
335
    rewrite <- H'15; auto with sets.
 
336
    intro H'8.
 
337
    elim H'7.
 
338
    intros H'9 H'10; apply H'10 || elim H'10; try assumption.
 
339
    generalize H'6.
 
340
    rewrite <- H'8.
 
341
    rewrite <- H'15; auto with sets.
 
342
  Qed.
 
343
 
 
344
End Finite_sets_facts.