diff options
Diffstat (limited to 'theories7/Sets/Powerset_facts.v')
-rwxr-xr-x | theories7/Sets/Powerset_facts.v | 276 |
1 files changed, 0 insertions, 276 deletions
diff --git a/theories7/Sets/Powerset_facts.v b/theories7/Sets/Powerset_facts.v deleted file mode 100755 index fbe7d93e..00000000 --- a/theories7/Sets/Powerset_facts.v +++ /dev/null @@ -1,276 +0,0 @@ -(************************************************************************) -(* 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.1.2.1 2004/07/16 19:31:39 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. -Hints Unfold not. - -Theorem Empty_set_zero : - (X: (Ensemble U)) (Union U (Empty_set U) X) == X. -Proof. -Auto 6 with sets. -Qed. -Hints Resolve Empty_set_zero. - -Theorem Empty_set_zero' : - (x: U) (Add U (Empty_set U) x) == (Singleton U x). -Proof. -Unfold 1 Add; Auto with sets. -Qed. -Hints Resolve Empty_set_zero'. - -Lemma less_than_empty : - (X: (Ensemble U)) (Included U X (Empty_set U)) -> X == (Empty_set U). -Proof. -Auto with sets. -Qed. -Hints Resolve less_than_empty. - -Theorem Union_commutative : - (A,B: (Ensemble U)) (Union U A B) == (Union U B A). -Proof. -Auto with sets. -Qed. - -Theorem Union_associative : - (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. -Hints Resolve Union_associative. - -Theorem Union_idempotent : (A: (Ensemble U)) (Union U A A) == A. -Proof. -Auto 7 with sets. -Qed. - -Lemma Union_absorbs : - (A, B: (Ensemble U)) (Included U B A) -> (Union U A B) == A. -Proof. -Auto 7 with sets. -Qed. - -Theorem Couple_as_union: - (x, y: U) (Union U (Singleton U x) (Singleton U y)) == (Couple U x y). -Proof. -Intros x y; Apply Extensionality_Ensembles; Split; Red. -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 : - (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. -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 : (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 : - (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 : - (A,B: (Ensemble U)) (Intersection U A B) == (Intersection U B A). -Proof. -Intros A B. -Apply Extensionality_Ensembles. -Split; Red; Intros x H'; Elim H'; Auto with sets. -Qed. - -Theorem Distributivity : - (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; 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' : - (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; 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 : - (A, B: (Ensemble U)) (x: U) - (Add U (Union U A B) x) == (Union U A (Add U B x)). -Proof. -Unfold Add; Auto with sets. -Qed. -Hints Resolve Union_add. - -Theorem Non_disjoint_union : - (X: (Ensemble U)) (x: U) (In U X x) -> (Add U X x) == X. -Intros X x H'; Unfold Add. -Apply Extensionality_Ensembles; Red. -Split; Red; 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' : - (X: (Ensemble U)) (x: U) ~ (In U X x) -> (Subtract U X x) == X. -Proof. -Intros X x H'; Unfold Subtract. -Apply Extensionality_Ensembles. -Split; Red; Auto with sets. -Intros x0 H'0; Elim H'0; Auto with sets. -Intros x0 H'0; Apply Setminus_intro; Auto with sets. -Red; 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 : (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. -Hints Resolve singlx. - -Lemma incl_add : - (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; 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. -Hints Resolve incl_add. - -Lemma incl_add_x : - (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. -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 : - (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. -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' : - (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 : - (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 4 Add. -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 : - (U: Type) - (A: (Ensemble U)) - (x, y: (Ensemble U)) - (Strict_Included U x y) -> - ~ (EXT 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. -Hints Resolve setcover_intro. - -End Sets_as_an_algebra. - -Hints Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add - singlx incl_add : sets v62. - - |