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
(****************************************************************************)
10
(* Naive Set Theory in Coq *)
13
(* Rocquencourt Sophia-Antipolis *)
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
(****************************************************************************)
27
(*i $Id: Powerset.v 8642 2006-03-17 10:09:02Z notin $ i*)
29
Require Export Ensembles.
30
Require Export Relations_1.
31
Require Export Relations_1_facts.
32
Require Export Partial_Order.
35
Section The_power_set_partial_order.
38
Inductive Power_set (A:Ensemble U) : Ensemble (Ensemble U) :=
39
Definition_of_Power_set :
40
forall X:Ensemble U, Included U X A -> In (Ensemble U) (Power_set A) X.
41
Hint Resolve Definition_of_Power_set.
43
Theorem Empty_set_minimal : forall X:Ensemble U, Included U (Empty_set U) X.
47
Hint Resolve Empty_set_minimal.
49
Theorem Power_set_Inhabited :
50
forall X:Ensemble U, Inhabited (Ensemble U) (Power_set X).
52
apply Inhabited_intro with (Empty_set U); auto with sets.
54
Hint Resolve Power_set_Inhabited.
56
Theorem Inclusion_is_an_order : Order (Ensemble U) (Included U).
59
Hint Resolve Inclusion_is_an_order.
61
Theorem Inclusion_is_transitive : Transitive (Ensemble U) (Included U).
62
elim Inclusion_is_an_order; auto with sets.
64
Hint Resolve Inclusion_is_transitive.
66
Definition Power_set_PO : Ensemble U -> PO (Ensemble U).
67
intro A; try assumption.
68
apply Definition_of_PO with (Power_set A) (Included U); auto with sets.
70
Hint Unfold Power_set_PO.
72
Theorem Strict_Rel_is_Strict_Included :
73
same_relation (Ensemble U) (Strict_Included U)
74
(Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U))).
77
Hint Resolve Strict_Rel_Transitive Strict_Rel_is_Strict_Included.
79
Lemma Strict_inclusion_is_transitive_with_inclusion :
80
forall x y z:Ensemble U,
81
Strict_Included U x y -> Included U y z -> Strict_Included U x z.
82
intros x y z H' H'0; try assumption.
83
elim Strict_Rel_is_Strict_Included.
84
unfold contains in |- *.
85
intros H'1 H'2; try assumption.
87
apply Strict_Rel_Transitive_with_Rel with (y := y); auto with sets.
90
Lemma Strict_inclusion_is_transitive_with_inclusion_left :
91
forall x y z:Ensemble U,
92
Included U x y -> Strict_Included U y z -> Strict_Included U x z.
93
intros x y z H' H'0; try assumption.
94
elim Strict_Rel_is_Strict_Included.
95
unfold contains in |- *.
96
intros H'1 H'2; try assumption.
98
apply Strict_Rel_Transitive_with_Rel_left with (y := y); auto with sets.
101
Lemma Strict_inclusion_is_transitive :
102
Transitive (Ensemble U) (Strict_Included U).
103
apply cong_transitive_same_relation with
104
(R := Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U)));
108
Theorem Empty_set_is_Bottom :
109
forall A:Ensemble U, Bottom (Ensemble U) (Power_set_PO A) (Empty_set U).
110
intro A; apply Bottom_definition; simpl in |- *; auto with sets.
112
Hint Resolve Empty_set_is_Bottom.
114
Theorem Union_minimal :
115
forall a b X:Ensemble U,
116
Included U a X -> Included U b X -> Included U (Union U a b) X.
117
intros a b X H' H'0; red in |- *.
118
intros x H'1; elim H'1; auto with sets.
120
Hint Resolve Union_minimal.
122
Theorem Intersection_maximal :
123
forall a b X:Ensemble U,
124
Included U X a -> Included U X b -> Included U X (Intersection U a b).
128
Theorem Union_increases_l : forall a b:Ensemble U, Included U a (Union U a b).
132
Theorem Union_increases_r : forall a b:Ensemble U, Included U b (Union U a b).
136
Theorem Intersection_decreases_l :
137
forall a b:Ensemble U, Included U (Intersection U a b) a.
138
intros a b; red in |- *.
139
intros x H'; elim H'; auto with sets.
142
Theorem Intersection_decreases_r :
143
forall a b:Ensemble U, Included U (Intersection U a b) b.
144
intros a b; red in |- *.
145
intros x H'; elim H'; auto with sets.
147
Hint Resolve Union_increases_l Union_increases_r Intersection_decreases_l
148
Intersection_decreases_r.
150
Theorem Union_is_Lub :
151
forall A a b:Ensemble U,
154
Lub (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b) (Union U a b).
156
apply Lub_definition; simpl in |- *.
157
apply Upper_Bound_definition; simpl in |- *; auto with sets.
158
intros y H'1; elim H'1; auto with sets.
159
intros y H'1; elim H'1; simpl in |- *; auto with sets.
162
Theorem Intersection_is_Glb :
163
forall A a b:Ensemble U,
166
Glb (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b)
167
(Intersection U a b).
169
apply Glb_definition; simpl in |- *.
170
apply Lower_Bound_definition; simpl in |- *; auto with sets.
171
apply Definition_of_Power_set.
172
generalize Inclusion_is_transitive; intro IT; red in IT; apply IT with a;
174
intros y H'1; elim H'1; auto with sets.
175
intros y H'1; elim H'1; simpl in |- *; auto with sets.
178
End The_power_set_partial_order.
180
Hint Resolve Empty_set_minimal: sets v62.
181
Hint Resolve Power_set_Inhabited: sets v62.
182
Hint Resolve Inclusion_is_an_order: sets v62.
183
Hint Resolve Inclusion_is_transitive: sets v62.
184
Hint Resolve Union_minimal: sets v62.
185
Hint Resolve Union_increases_l: sets v62.
186
Hint Resolve Union_increases_r: sets v62.
187
Hint Resolve Intersection_decreases_l: sets v62.
188
Hint Resolve Intersection_decreases_r: sets v62.
189
Hint Resolve Empty_set_is_Bottom: sets v62.
190
Hint Resolve Strict_inclusion_is_transitive: sets v62.
b'\\ No newline at end of file'