diff options
Diffstat (limited to 'theories/Sets/Powerset_facts.v')
| -rwxr-xr-x | theories/Sets/Powerset_facts.v | 268 |
1 files changed, 268 insertions, 0 deletions
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v new file mode 100755 index 00000000..2c71f529 --- /dev/null +++ b/theories/Sets/Powerset_facts.v @@ -0,0 +1,268 @@ +(************************************************************************) +(* 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_facts.v,v 1.8.2.1 2004/07/16 19:31:18 herbelin Exp $ i*) + +Require Export Ensembles. +Require Export Constructive_sets. +Require Export Relations_1. +Require Export Relations_1_facts. +Require Export Partial_Order. +Require Export Cpo. +Require Export Powerset. + +Section Sets_as_an_algebra. +Variable U : Type. +Hint Unfold not. + +Theorem Empty_set_zero : forall X:Ensemble U, Union U (Empty_set U) X = X. +Proof. +auto 6 with sets. +Qed. +Hint Resolve Empty_set_zero. + +Theorem Empty_set_zero' : forall x:U, Add U (Empty_set U) x = Singleton U x. +Proof. +unfold Add at 1 in |- *; auto with sets. +Qed. +Hint Resolve Empty_set_zero'. + +Lemma less_than_empty : + forall X:Ensemble U, Included U X (Empty_set U) -> X = Empty_set U. +Proof. +auto with sets. +Qed. +Hint Resolve less_than_empty. + +Theorem Union_commutative : forall A B:Ensemble U, Union U A B = Union U B A. +Proof. +auto with sets. +Qed. + +Theorem Union_associative : + forall A B C:Ensemble U, Union U (Union U A B) C = Union U A (Union U B C). +Proof. +auto 9 with sets. +Qed. +Hint Resolve Union_associative. + +Theorem Union_idempotent : forall A:Ensemble U, Union U A A = A. +Proof. +auto 7 with sets. +Qed. + +Lemma Union_absorbs : + forall A B:Ensemble U, Included U B A -> Union U A B = A. +Proof. +auto 7 with sets. +Qed. + +Theorem Couple_as_union : + forall x y:U, Union U (Singleton U x) (Singleton U y) = Couple U x y. +Proof. +intros x y; apply Extensionality_Ensembles; split; red in |- *. +intros x0 H'; elim H'; (intros x1 H'0; elim H'0; auto with sets). +intros x0 H'; elim H'; auto with sets. +Qed. + +Theorem Triple_as_union : + forall x y z:U, + Union U (Union U (Singleton U x) (Singleton U y)) (Singleton U z) = + Triple U x y z. +Proof. +intros x y z; apply Extensionality_Ensembles; split; red in |- *. +intros x0 H'; elim H'. +intros x1 H'0; elim H'0; (intros x2 H'1; elim H'1; auto with sets). +intros x1 H'0; elim H'0; auto with sets. +intros x0 H'; elim H'; auto with sets. +Qed. + +Theorem Triple_as_Couple : forall x y:U, Couple U x y = Triple U x x y. +Proof. +intros x y. +rewrite <- (Couple_as_union x y). +rewrite <- (Union_idempotent (Singleton U x)). +apply Triple_as_union. +Qed. + +Theorem Triple_as_Couple_Singleton : + forall x y z:U, Triple U x y z = Union U (Couple U x y) (Singleton U z). +Proof. +intros x y z. +rewrite <- (Triple_as_union x y z). +rewrite <- (Couple_as_union x y); auto with sets. +Qed. + +Theorem Intersection_commutative : + forall A B:Ensemble U, Intersection U A B = Intersection U B A. +Proof. +intros A B. +apply Extensionality_Ensembles. +split; red in |- *; intros x H'; elim H'; auto with sets. +Qed. + +Theorem Distributivity : + forall A B C:Ensemble U, + Intersection U A (Union U B C) = + Union U (Intersection U A B) (Intersection U A C). +Proof. +intros A B C. +apply Extensionality_Ensembles. +split; red in |- *; intros x H'. +elim H'. +intros x0 H'0 H'1; generalize H'0. +elim H'1; auto with sets. +elim H'; intros x0 H'0; elim H'0; auto with sets. +Qed. + +Theorem Distributivity' : + forall A B C:Ensemble U, + Union U A (Intersection U B C) = + Intersection U (Union U A B) (Union U A C). +Proof. +intros A B C. +apply Extensionality_Ensembles. +split; red in |- *; intros x H'. +elim H'; auto with sets. +intros x0 H'0; elim H'0; auto with sets. +elim H'. +intros x0 H'0; elim H'0; auto with sets. +intros x1 H'1 H'2; try exact H'2. +generalize H'1. +elim H'2; auto with sets. +Qed. + +Theorem Union_add : + forall (A B:Ensemble U) (x:U), Add U (Union U A B) x = Union U A (Add U B x). +Proof. +unfold Add in |- *; auto with sets. +Qed. +Hint Resolve Union_add. + +Theorem Non_disjoint_union : + forall (X:Ensemble U) (x:U), In U X x -> Add U X x = X. +intros X x H'; unfold Add in |- *. +apply Extensionality_Ensembles; red in |- *. +split; red in |- *; auto with sets. +intros x0 H'0; elim H'0; auto with sets. +intros t H'1; elim H'1; auto with sets. +Qed. + +Theorem Non_disjoint_union' : + forall (X:Ensemble U) (x:U), ~ In U X x -> Subtract U X x = X. +Proof. +intros X x H'; unfold Subtract in |- *. +apply Extensionality_Ensembles. +split; red in |- *; auto with sets. +intros x0 H'0; elim H'0; auto with sets. +intros x0 H'0; apply Setminus_intro; auto with sets. +red in |- *; intro H'1; elim H'1. +lapply (Singleton_inv U x x0); auto with sets. +intro H'4; apply H'; rewrite H'4; auto with sets. +Qed. + +Lemma singlx : forall x y:U, In U (Add U (Empty_set U) x) y -> x = y. +Proof. +intro x; rewrite (Empty_set_zero' x); auto with sets. +Qed. +Hint Resolve singlx. + +Lemma incl_add : + forall (A B:Ensemble U) (x:U), + Included U A B -> Included U (Add U A x) (Add U B x). +Proof. +intros A B x H'; red in |- *; auto with sets. +intros x0 H'0. +lapply (Add_inv U A x x0); auto with sets. +intro H'1; elim H'1; + [ intro H'2; clear H'1 | intro H'2; rewrite <- H'2; clear H'1 ]; + auto with sets. +Qed. +Hint Resolve incl_add. + +Lemma incl_add_x : + forall (A B:Ensemble U) (x:U), + ~ In U A x -> Included U (Add U A x) (Add U B x) -> Included U A B. +Proof. +unfold Included in |- *. +intros A B x H' H'0 x0 H'1. +lapply (H'0 x0); auto with sets. +intro H'2; lapply (Add_inv U B x x0); auto with sets. +intro H'3; elim H'3; + [ intro H'4; try exact H'4; clear H'3 | intro H'4; clear H'3 ]. +absurd (In U A x0); auto with sets. +rewrite <- H'4; auto with sets. +Qed. + +Lemma Add_commutative : + forall (A:Ensemble U) (x y:U), Add U (Add U A x) y = Add U (Add U A y) x. +Proof. +intros A x y. +unfold Add in |- *. +rewrite (Union_associative A (Singleton U x) (Singleton U y)). +rewrite (Union_commutative (Singleton U x) (Singleton U y)). +rewrite <- (Union_associative A (Singleton U y) (Singleton U x)); + auto with sets. +Qed. + +Lemma Add_commutative' : + forall (A:Ensemble U) (x y z:U), + Add U (Add U (Add U A x) y) z = Add U (Add U (Add U A z) x) y. +Proof. +intros A x y z. +rewrite (Add_commutative (Add U A x) y z). +rewrite (Add_commutative A x z); auto with sets. +Qed. + +Lemma Add_distributes : + forall (A B:Ensemble U) (x y:U), + Included U B A -> Add U (Add U A x) y = Union U (Add U A x) (Add U B y). +Proof. +intros A B x y H'; try assumption. +rewrite <- (Union_add (Add U A x) B y). +unfold Add at 4 in |- *. +rewrite (Union_commutative A (Singleton U x)). +rewrite Union_associative. +rewrite (Union_absorbs A B H'). +rewrite (Union_commutative (Singleton U x) A). +auto with sets. +Qed. + +Lemma setcover_intro : + forall (U:Type) (A x y:Ensemble U), + Strict_Included U x y -> + ~ (exists z : _, Strict_Included U x z /\ Strict_Included U z y) -> + covers (Ensemble U) (Power_set_PO U A) y x. +Proof. +intros; apply Definition_of_covers; auto with sets. +Qed. +Hint Resolve setcover_intro. + +End Sets_as_an_algebra. + +Hint Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add + singlx incl_add: sets v62. + |