diff options
Diffstat (limited to 'theories7/Sets/Powerset.v')
| -rwxr-xr-x | theories7/Sets/Powerset.v | 188 |
1 files changed, 188 insertions, 0 deletions
diff --git a/theories7/Sets/Powerset.v b/theories7/Sets/Powerset.v new file mode 100755 index 00000000..b1fa892c --- /dev/null +++ b/theories7/Sets/Powerset.v @@ -0,0 +1,188 @@ +(************************************************************************) +(* 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: Powerset.v,v 1.1.2.1 2004/07/16 19:31:39 herbelin Exp $ i*) + +Require Export Ensembles. +Require Export Relations_1. +Require Export Relations_1_facts. +Require Export Partial_Order. +Require Export Cpo. + +Section The_power_set_partial_order. +Variable U: Type. + +Inductive Power_set [A:(Ensemble U)]: (Ensemble (Ensemble U)) := + Definition_of_Power_set: + (X: (Ensemble U)) (Included U X A) -> (In (Ensemble U) (Power_set A) X). +Hints Resolve Definition_of_Power_set. + +Theorem Empty_set_minimal: (X: (Ensemble U)) (Included U (Empty_set U) X). +Intro X; Red. +Intros x H'; Elim H'. +Qed. +Hints Resolve Empty_set_minimal. + +Theorem Power_set_Inhabited: + (X: (Ensemble U)) (Inhabited (Ensemble U) (Power_set X)). +Intro X. +Apply Inhabited_intro with (Empty_set U); Auto with sets. +Qed. +Hints Resolve Power_set_Inhabited. + +Theorem Inclusion_is_an_order: (Order (Ensemble U) (Included U)). +Auto 6 with sets. +Qed. +Hints Resolve Inclusion_is_an_order. + +Theorem Inclusion_is_transitive: (Transitive (Ensemble U) (Included U)). +Elim Inclusion_is_an_order; Auto with sets. +Qed. +Hints Resolve Inclusion_is_transitive. + +Definition Power_set_PO: (Ensemble U) -> (PO (Ensemble U)). +Intro A; Try Assumption. +Apply Definition_of_PO with (Power_set A) (Included U); Auto with sets. +Defined. +Hints Unfold Power_set_PO. + +Theorem Strict_Rel_is_Strict_Included: + (same_relation + (Ensemble U) (Strict_Included U) + (Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U)))). +Auto with sets. +Qed. +Hints Resolve Strict_Rel_Transitive Strict_Rel_is_Strict_Included. + +Lemma Strict_inclusion_is_transitive_with_inclusion: + (x, y, z:(Ensemble U)) (Strict_Included U x y) -> (Included U y z) -> + (Strict_Included U x z). +Intros x y z H' H'0; Try Assumption. +Elim Strict_Rel_is_Strict_Included. +Unfold contains. +Intros H'1 H'2; Try Assumption. +Apply H'1. +Apply Strict_Rel_Transitive_with_Rel with y := y; Auto with sets. +Qed. + +Lemma Strict_inclusion_is_transitive_with_inclusion_left: + (x, y, z:(Ensemble U)) (Included U x y) -> (Strict_Included U y z) -> + (Strict_Included U x z). +Intros x y z H' H'0; Try Assumption. +Elim Strict_Rel_is_Strict_Included. +Unfold contains. +Intros H'1 H'2; Try Assumption. +Apply H'1. +Apply Strict_Rel_Transitive_with_Rel_left with y := y; Auto with sets. +Qed. + +Lemma Strict_inclusion_is_transitive: + (Transitive (Ensemble U) (Strict_Included U)). +Apply cong_transitive_same_relation + with R := (Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U))); Auto with sets. +Qed. + +Theorem Empty_set_is_Bottom: + (A: (Ensemble U)) (Bottom (Ensemble U) (Power_set_PO A) (Empty_set U)). +Intro A; Apply Bottom_definition; Simpl; Auto with sets. +Qed. +Hints Resolve Empty_set_is_Bottom. + +Theorem Union_minimal: + (a, b, X: (Ensemble U)) (Included U a X) -> (Included U b X) -> + (Included U (Union U a b) X). +Intros a b X H' H'0; Red. +Intros x H'1; Elim H'1; Auto with sets. +Qed. +Hints Resolve Union_minimal. + +Theorem Intersection_maximal: + (a, b, X: (Ensemble U)) (Included U X a) -> (Included U X b) -> + (Included U X (Intersection U a b)). +Auto with sets. +Qed. + +Theorem Union_increases_l: (a, b: (Ensemble U)) (Included U a (Union U a b)). +Auto with sets. +Qed. + +Theorem Union_increases_r: (a, b: (Ensemble U)) (Included U b (Union U a b)). +Auto with sets. +Qed. + +Theorem Intersection_decreases_l: + (a, b: (Ensemble U)) (Included U (Intersection U a b) a). +Intros a b; Red. +Intros x H'; Elim H'; Auto with sets. +Qed. + +Theorem Intersection_decreases_r: + (a, b: (Ensemble U)) (Included U (Intersection U a b) b). +Intros a b; Red. +Intros x H'; Elim H'; Auto with sets. +Qed. +Hints Resolve Union_increases_l Union_increases_r Intersection_decreases_l + Intersection_decreases_r. + +Theorem Union_is_Lub: + (A: (Ensemble U)) (a, b: (Ensemble U)) (Included U a A) -> (Included U b A) -> + (Lub (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b) (Union U a b)). +Intros A a b H' H'0. +Apply Lub_definition; Simpl. +Apply Upper_Bound_definition; Simpl; Auto with sets. +Intros y H'1; Elim H'1; Auto with sets. +Intros y H'1; Elim H'1; Simpl; Auto with sets. +Qed. + +Theorem Intersection_is_Glb: + (A: (Ensemble U)) (a, b: (Ensemble U)) (Included U a A) -> (Included U b A) -> + (Glb + (Ensemble U) + (Power_set_PO A) + (Couple (Ensemble U) a b) + (Intersection U a b)). +Intros A a b H' H'0. +Apply Glb_definition; Simpl. +Apply Lower_Bound_definition; Simpl; Auto with sets. +Apply Definition_of_Power_set. +Generalize Inclusion_is_transitive; Intro IT; Red in IT; Apply IT with a; Auto with sets. +Intros y H'1; Elim H'1; Auto with sets. +Intros y H'1; Elim H'1; Simpl; Auto with sets. +Qed. + +End The_power_set_partial_order. + +Hints Resolve Empty_set_minimal : sets v62. +Hints Resolve Power_set_Inhabited : sets v62. +Hints Resolve Inclusion_is_an_order : sets v62. +Hints Resolve Inclusion_is_transitive : sets v62. +Hints Resolve Union_minimal : sets v62. +Hints Resolve Union_increases_l : sets v62. +Hints Resolve Union_increases_r : sets v62. +Hints Resolve Intersection_decreases_l : sets v62. +Hints Resolve Intersection_decreases_r : sets v62. +Hints Resolve Empty_set_is_Bottom : sets v62. +Hints Resolve Strict_inclusion_is_transitive : sets v62. |