diff options
Diffstat (limited to 'theories/Sets/Powerset_facts.v')
| -rw-r--r-- | theories/Sets/Powerset_facts.v | 436 |
1 files changed, 214 insertions, 222 deletions
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v index 47ef2ea7..edb6a215 100644 --- a/theories/Sets/Powerset_facts.v +++ b/theories/Sets/Powerset_facts.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id: Powerset_facts.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Powerset_facts.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Export Ensembles. Require Export Constructive_sets. @@ -35,231 +35,223 @@ Require Export Cpo. Require Export Powerset. Section Sets_as_an_algebra. -Variable U : Type. -Hint Unfold not. + Variable U : Type. -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:Ensemble U, Union U (Empty_set U) X = X. + Proof. + auto 6 with sets. + Qed. + + Theorem Empty_set_zero' : forall x:U, Add U (Empty_set U) x = Singleton U x. + Proof. + unfold Add at 1 in |- *; auto using Empty_set_zero with sets. + Qed. + + Lemma less_than_empty : + forall X:Ensemble U, Included U X (Empty_set U) -> X = Empty_set U. + Proof. + auto with sets. + Qed. + + 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. + + 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 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'. + 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 using Union_associative with sets. + Qed. + + Theorem Non_disjoint_union : + forall (X:Ensemble U) (x:U), In U X x -> Add U X x = X. + Proof. + 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. + + 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. -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. + 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. -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. + 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. End Sets_as_an_algebra. |