← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/Sets/Powerset_Classical_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/Powerset_Classical_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: Powerset_Classical_facts.v 10855 2008-04-27 11:16:15Z msozeau $ i*)
 
28
 
 
29
Require Export Ensembles.
 
30
Require Export Constructive_sets.
 
31
Require Export Relations_1.
 
32
Require Export Relations_1_facts.
 
33
Require Export Partial_Order.
 
34
Require Export Cpo.
 
35
Require Export Powerset.
 
36
Require Export Powerset_facts.
 
37
Require Export Classical_Type.
 
38
Require Export Classical_sets.
 
39
 
 
40
Section Sets_as_an_algebra.
 
41
 
 
42
  Variable U : Type.
 
43
  
 
44
  Lemma sincl_add_x :
 
45
    forall (A B:Ensemble U) (x:U),
 
46
      ~ In U A x ->
 
47
      Strict_Included U (Add U A x) (Add U B x) -> Strict_Included U A B.
 
48
  Proof.
 
49
    intros A B x H' H'0; red in |- *.
 
50
    lapply (Strict_Included_inv U (Add U A x) (Add U B x)); auto with sets.
 
51
    clear H'0; intro H'0; split.
 
52
    apply incl_add_x with (x := x); tauto.
 
53
    elim H'0; intros H'1 H'2; elim H'2; clear H'0 H'2.
 
54
    intros x0 H'0.
 
55
    red in |- *; intro H'2.
 
56
    elim H'0; clear H'0.
 
57
    rewrite <- H'2; auto with sets.
 
58
  Qed.
 
59
 
 
60
  Lemma incl_soustr_in :
 
61
    forall (X:Ensemble U) (x:U), In U X x -> Included U (Subtract U X x) X.
 
62
  Proof.
 
63
    intros X x H'; red in |- *.
 
64
    intros x0 H'0; elim H'0; auto with sets.
 
65
  Qed.
 
66
  
 
67
  Lemma incl_soustr :
 
68
    forall (X Y:Ensemble U) (x:U),
 
69
      Included U X Y -> Included U (Subtract U X x) (Subtract U Y x).
 
70
  Proof.
 
71
    intros X Y x H'; red in |- *.
 
72
    intros x0 H'0; elim H'0.
 
73
    intros H'1 H'2.
 
74
    apply Subtract_intro; auto with sets.
 
75
  Qed.
 
76
  
 
77
  Lemma incl_soustr_add_l :
 
78
    forall (X:Ensemble U) (x:U), Included U (Subtract U (Add U X x) x) X.
 
79
  Proof.
 
80
    intros X x; red in |- *.
 
81
    intros x0 H'; elim H'; auto with sets.
 
82
    intro H'0; elim H'0; auto with sets.
 
83
    intros t H'1 H'2; elim H'2; auto with sets.
 
84
  Qed.
 
85
 
 
86
  Lemma incl_soustr_add_r :
 
87
    forall (X:Ensemble U) (x:U),
 
88
      ~ In U X x -> Included U X (Subtract U (Add U X x) x).
 
89
  Proof.
 
90
    intros X x H'; red in |- *.
 
91
    intros x0 H'0; try assumption.
 
92
    apply Subtract_intro; auto with sets.
 
93
    red in |- *; intro H'1; apply H'; rewrite H'1; auto with sets.
 
94
  Qed.
 
95
  Hint Resolve incl_soustr_add_r: sets v62.
 
96
  
 
97
  Lemma add_soustr_2 :
 
98
    forall (X:Ensemble U) (x:U),
 
99
      In U X x -> Included U X (Add U (Subtract U X x) x).
 
100
  Proof.
 
101
    intros X x H'; red in |- *.
 
102
    intros x0 H'0; try assumption.
 
103
    elim (classic (x = x0)); intro K; auto with sets.
 
104
    elim K; auto with sets.
 
105
  Qed.
 
106
  
 
107
  Lemma add_soustr_1 :
 
108
    forall (X:Ensemble U) (x:U),
 
109
      In U X x -> Included U (Add U (Subtract U X x) x) X.
 
110
  Proof.
 
111
    intros X x H'; red in |- *.
 
112
    intros x0 H'0; elim H'0; auto with sets.
 
113
    intros y H'1; elim H'1; auto with sets.
 
114
    intros t H'1; try assumption.
 
115
    rewrite <- (Singleton_inv U x t); auto with sets.
 
116
  Qed.
 
117
  
 
118
  Lemma add_soustr_xy :
 
119
    forall (X:Ensemble U) (x y:U),
 
120
      x <> y -> Subtract U (Add U X x) y = Add U (Subtract U X y) x.
 
121
  Proof.
 
122
    intros X x y H'; apply Extensionality_Ensembles.
 
123
    split; red in |- *.
 
124
    intros x0 H'0; elim H'0; auto with sets.
 
125
    intro H'1; elim H'1.
 
126
    intros u H'2 H'3; try assumption.
 
127
    apply Add_intro1.
 
128
    apply Subtract_intro; auto with sets.
 
129
    intros t H'2 H'3; try assumption.
 
130
    elim (Singleton_inv U x t); auto with sets.
 
131
    intros u H'2; try assumption.
 
132
    elim (Add_inv U (Subtract U X y) x u); auto with sets.
 
133
    intro H'0; elim H'0; auto with sets.
 
134
    intro H'0; rewrite <- H'0; auto with sets.
 
135
  Qed.
 
136
  
 
137
  Lemma incl_st_add_soustr :
 
138
    forall (X Y:Ensemble U) (x:U),
 
139
      ~ In U X x ->
 
140
      Strict_Included U (Add U X x) Y -> Strict_Included U X (Subtract U Y x).
 
141
  Proof.
 
142
    intros X Y x H' H'0; apply sincl_add_x with (x := x); auto using add_soustr_1 with sets.
 
143
    split.
 
144
    elim H'0.
 
145
    intros H'1 H'2.
 
146
    generalize (Inclusion_is_transitive U).
 
147
    intro H'4; red in H'4.
 
148
    apply H'4 with (y := Y); auto using add_soustr_2 with sets.
 
149
    red in H'0.
 
150
    elim H'0; intros H'1 H'2; try exact H'1; clear H'0. (* PB *)
 
151
    red in |- *; intro H'0; apply H'2.
 
152
    rewrite H'0; auto 8 using add_soustr_xy, add_soustr_1, add_soustr_2 with sets.
 
153
  Qed.
 
154
  
 
155
  Lemma Sub_Add_new :
 
156
    forall (X:Ensemble U) (x:U), ~ In U X x -> X = Subtract U (Add U X x) x.
 
157
  Proof.
 
158
    auto using incl_soustr_add_l with sets.
 
159
  Qed.
 
160
  
 
161
  Lemma Simplify_add :
 
162
    forall (X X0:Ensemble U) (x:U),
 
163
      ~ In U X x -> ~ In U X0 x -> Add U X x = Add U X0 x -> X = X0.
 
164
  Proof.
 
165
    intros X X0 x H' H'0 H'1; try assumption.
 
166
    rewrite (Sub_Add_new X x); auto with sets.
 
167
    rewrite (Sub_Add_new X0 x); auto with sets.
 
168
    rewrite H'1; auto with sets.
 
169
  Qed.
 
170
  
 
171
  Lemma Included_Add :
 
172
    forall (X A:Ensemble U) (x:U),
 
173
      Included U X (Add U A x) ->
 
174
      Included U X A \/ (exists A' : _, X = Add U A' x /\ Included U A' A).
 
175
  Proof.
 
176
    intros X A x H'0; try assumption.
 
177
    elim (classic (In U X x)).
 
178
    intro H'1; right; try assumption.
 
179
    exists (Subtract U X x).
 
180
    split; auto using incl_soustr_in, add_soustr_xy, add_soustr_1, add_soustr_2 with sets.
 
181
    red in H'0.
 
182
    red in |- *.
 
183
    intros x0 H'2; try assumption.
 
184
    lapply (Subtract_inv U X x x0); auto with sets.
 
185
    intro H'3; elim H'3; intros K K'; clear H'3.
 
186
    lapply (H'0 x0); auto with sets.
 
187
    intro H'3; try assumption.
 
188
    lapply (Add_inv U A x x0); auto with sets.
 
189
    intro H'4; elim H'4;
 
190
      [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ].
 
191
    elim K'; auto with sets.
 
192
    intro H'1; left; try assumption.
 
193
    red in H'0.
 
194
    red in |- *.
 
195
    intros x0 H'2; try assumption.
 
196
    lapply (H'0 x0); auto with sets.
 
197
    intro H'3; try assumption.
 
198
    lapply (Add_inv U A x x0); auto with sets.
 
199
    intro H'4; elim H'4;
 
200
      [ intro H'5; try exact H'5; clear H'4 | intro H'5; clear H'4 ].
 
201
    absurd (In U X x0); auto with sets.
 
202
    rewrite <- H'5; auto with sets.
 
203
  Qed.
 
204
  
 
205
  Lemma setcover_inv :
 
206
    forall A x y:Ensemble U,
 
207
      covers (Ensemble U) (Power_set_PO U A) y x ->
 
208
      Strict_Included U x y /\
 
209
      (forall z:Ensemble U, Included U x z -> Included U z y -> x = z \/ z = y).
 
210
  Proof.
 
211
    intros A x y H'; elim H'.
 
212
    unfold Strict_Rel_of in |- *; simpl in |- *.
 
213
    intros H'0 H'1; split; [ auto with sets | idtac ].
 
214
    intros z H'2 H'3; try assumption.
 
215
    elim (classic (x = z)); auto with sets.
 
216
    intro H'4; right; try assumption.
 
217
    elim (classic (z = y)); auto with sets.
 
218
    intro H'5; try assumption.
 
219
    elim H'1.
 
220
    exists z; auto with sets.
 
221
  Qed.
 
222
  
 
223
  Theorem Add_covers :
 
224
    forall A a:Ensemble U,
 
225
      Included U a A ->
 
226
      forall x:U,
 
227
        In U A x ->
 
228
        ~ In U a x -> covers (Ensemble U) (Power_set_PO U A) (Add U a x) a.
 
229
  Proof.
 
230
    intros A a H' x H'0 H'1; try assumption.
 
231
    apply setcover_intro; auto with sets.
 
232
    red in |- *.
 
233
    split; [ idtac | red in |- *; intro H'2; try exact H'2 ]; auto with sets.
 
234
    apply H'1.
 
235
    rewrite H'2; auto with sets.
 
236
    red in |- *; intro H'2; elim H'2; clear H'2.
 
237
    intros z H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2.
 
238
    lapply (Strict_Included_inv U a z); auto with sets; clear H'3.
 
239
    intro H'2; elim H'2; intros H'3 H'5; elim H'5; clear H'2 H'5.
 
240
    intros x0 H'2; elim H'2.
 
241
    intros H'5 H'6; try assumption.
 
242
    generalize H'4; intro K.
 
243
    red in H'4.
 
244
    elim H'4; intros H'8 H'9; red in H'8; clear H'4.
 
245
    lapply (H'8 x0); auto with sets.
 
246
    intro H'7; try assumption.
 
247
    elim (Add_inv U a x x0); auto with sets.
 
248
    intro H'15.
 
249
    cut (Included U (Add U a x) z).
 
250
    intro H'10; try assumption.
 
251
    red in K.
 
252
    elim K; intros H'11 H'12; apply H'12; clear K; auto with sets.
 
253
    rewrite H'15.
 
254
    red in |- *.
 
255
    intros x1 H'10; elim H'10; auto with sets.
 
256
    intros x2 H'11; elim H'11; auto with sets.
 
257
  Qed.
 
258
  
 
259
  Theorem covers_Add :
 
260
    forall A a a':Ensemble U,
 
261
      Included U a A ->
 
262
      Included U a' A ->
 
263
      covers (Ensemble U) (Power_set_PO U A) a' a ->
 
264
      exists x : _, a' = Add U a x /\ In U A x /\ ~ In U a x.
 
265
  Proof.
 
266
    intros A a a' H' H'0 H'1; try assumption.
 
267
    elim (setcover_inv A a a'); auto with sets.
 
268
    intros H'6 H'7.
 
269
    clear H'1.
 
270
    elim (Strict_Included_inv U a a'); auto with sets.
 
271
    intros H'5 H'8; elim H'8.
 
272
    intros x H'1; elim H'1.
 
273
    intros H'2 H'3; try assumption.
 
274
    exists x.
 
275
    split; [ try assumption | idtac ].
 
276
    clear H'8 H'1.
 
277
    elim (H'7 (Add U a x)); auto with sets.
 
278
    intro H'1.
 
279
    absurd (a = Add U a x); auto with sets.
 
280
    red in |- *; intro H'8; try exact H'8.
 
281
    apply H'3.
 
282
    rewrite H'8; auto with sets.
 
283
    auto with sets.
 
284
    red in |- *.
 
285
    intros x0 H'1; elim H'1; auto with sets.
 
286
    intros x1 H'8; elim H'8; auto with sets.
 
287
    split; [ idtac | try assumption ].
 
288
    red in H'0; auto with sets.
 
289
  Qed.
 
290
 
 
291
  Theorem covers_is_Add :
 
292
    forall A a a':Ensemble U,
 
293
      Included U a A ->
 
294
      Included U a' A ->
 
295
      (covers (Ensemble U) (Power_set_PO U A) a' a <->
 
296
        (exists x : _, a' = Add U a x /\ In U A x /\ ~ In U a x)).
 
297
  Proof.
 
298
    intros A a a' H' H'0; split; intro K.
 
299
    apply covers_Add with (A := A); auto with sets.
 
300
    elim K.
 
301
    intros x H'1; elim H'1; intros H'2 H'3; rewrite H'2; clear H'1.
 
302
    apply Add_covers; intuition.
 
303
  Qed.
 
304
  
 
305
  Theorem Singleton_atomic :
 
306
    forall (x:U) (A:Ensemble U),
 
307
      In U A x ->
 
308
      covers (Ensemble U) (Power_set_PO U A) (Singleton U x) (Empty_set U).
 
309
  Proof.
 
310
    intros x A H'.
 
311
    rewrite <- (Empty_set_zero' U x).
 
312
    apply Add_covers; auto with sets.
 
313
  Qed.
 
314
  
 
315
  Lemma less_than_singleton :
 
316
    forall (X:Ensemble U) (x:U),
 
317
      Strict_Included U X (Singleton U x) -> X = Empty_set U.
 
318
  Proof.
 
319
    intros X x H'; try assumption.
 
320
    red in H'.
 
321
    lapply (Singleton_atomic x (Full_set U));
 
322
      [ intro H'2; try exact H'2 | apply Full_intro ].
 
323
    elim H'; intros H'0 H'1; try exact H'1; clear H'.
 
324
    elim (setcover_inv (Full_set U) (Empty_set U) (Singleton U x));
 
325
      [ intros H'6 H'7; try exact H'7 | idtac ]; auto with sets.
 
326
    elim (H'7 X); [ intro H'5; try exact H'5 | intro H'5 | idtac | idtac ];
 
327
      auto with sets.
 
328
    elim H'1; auto with sets.
 
329
  Qed.
 
330
 
 
331
End Sets_as_an_algebra.
 
332
 
 
333
Hint Resolve incl_soustr_in: sets v62.
 
334
Hint Resolve incl_soustr: sets v62.
 
335
Hint Resolve incl_soustr_add_l: sets v62.
 
336
Hint Resolve incl_soustr_add_r: sets v62.
 
337
Hint Resolve add_soustr_1 add_soustr_2: sets v62.
 
338
Hint Resolve add_soustr_xy: sets v62.