diff options
Diffstat (limited to 'theories7/Sets/Powerset_Classical_facts.v')
| -rwxr-xr-x | theories7/Sets/Powerset_Classical_facts.v | 338 |
1 files changed, 338 insertions, 0 deletions
diff --git a/theories7/Sets/Powerset_Classical_facts.v b/theories7/Sets/Powerset_Classical_facts.v new file mode 100755 index 00000000..1a51c562 --- /dev/null +++ b/theories7/Sets/Powerset_Classical_facts.v @@ -0,0 +1,338 @@ +(************************************************************************) +(* 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_Classical_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. +Require Export Powerset_facts. +Require Export Classical_Type. +Require Export Classical_sets. + +Section Sets_as_an_algebra. + +Variable U: Type. + +Lemma sincl_add_x: + (A, B: (Ensemble U)) + (x: U) ~ (In U A x) -> (Strict_Included U (Add U A x) (Add U B x)) -> + (Strict_Included U A B). +Proof. +Intros A B x H' H'0; Red. +LApply (Strict_Included_inv U (Add U A x) (Add U B x)); Auto with sets. +Clear H'0; Intro H'0; Split. +Apply incl_add_x with x := x; Tauto. +Elim H'0; Intros H'1 H'2; Elim H'2; Clear H'0 H'2. +Intros x0 H'0. +Red; Intro H'2. +Elim H'0; Clear H'0. +Rewrite <- H'2; Auto with sets. +Qed. + +Lemma incl_soustr_in: + (X: (Ensemble U)) (x: U) (In U X x) -> (Included U (Subtract U X x) X). +Proof. +Intros X x H'; Red. +Intros x0 H'0; Elim H'0; Auto with sets. +Qed. +Hints Resolve incl_soustr_in : sets v62. + +Lemma incl_soustr: + (X, Y: (Ensemble U)) (x: U) (Included U X Y) -> + (Included U (Subtract U X x) (Subtract U Y x)). +Proof. +Intros X Y x H'; Red. +Intros x0 H'0; Elim H'0. +Intros H'1 H'2. +Apply Subtract_intro; Auto with sets. +Qed. +Hints Resolve incl_soustr : sets v62. + + +Lemma incl_soustr_add_l: + (X: (Ensemble U)) (x: U) (Included U (Subtract U (Add U X x) x) X). +Proof. +Intros X x; Red. +Intros x0 H'; Elim H'; Auto with sets. +Intro H'0; Elim H'0; Auto with sets. +Intros t H'1 H'2; Elim H'2; Auto with sets. +Qed. +Hints Resolve incl_soustr_add_l : sets v62. + +Lemma incl_soustr_add_r: + (X: (Ensemble U)) (x: U) ~ (In U X x) -> + (Included U X (Subtract U (Add U X x) x)). +Proof. +Intros X x H'; Red. +Intros x0 H'0; Try Assumption. +Apply Subtract_intro; Auto with sets. +Red; Intro H'1; Apply H'; Rewrite H'1; Auto with sets. +Qed. +Hints Resolve incl_soustr_add_r : sets v62. + +Lemma add_soustr_2: + (X: (Ensemble U)) (x: U) (In U X x) -> + (Included U X (Add U (Subtract U X x) x)). +Proof. +Intros X x H'; Red. +Intros x0 H'0; Try Assumption. +Elim (classic x == x0); Intro K; Auto with sets. +Elim K; Auto with sets. +Qed. + +Lemma add_soustr_1: + (X: (Ensemble U)) (x: U) (In U X x) -> + (Included U (Add U (Subtract U X x) x) X). +Proof. +Intros X x H'; Red. +Intros x0 H'0; Elim H'0; Auto with sets. +Intros y H'1; Elim H'1; Auto with sets. +Intros t H'1; Try Assumption. +Rewrite <- (Singleton_inv U x t); Auto with sets. +Qed. +Hints Resolve add_soustr_1 add_soustr_2 : sets v62. + +Lemma add_soustr_xy: + (X: (Ensemble U)) (x, y: U) ~ x == y -> + (Subtract U (Add U X x) y) == (Add U (Subtract U X y) x). +Proof. +Intros X x y H'; Apply Extensionality_Ensembles. +Split; Red. +Intros x0 H'0; Elim H'0; Auto with sets. +Intro H'1; Elim H'1. +Intros u H'2 H'3; Try Assumption. +Apply Add_intro1. +Apply Subtract_intro; Auto with sets. +Intros t H'2 H'3; Try Assumption. +Elim (Singleton_inv U x t); Auto with sets. +Intros u H'2; Try Assumption. +Elim (Add_inv U (Subtract U X y) x u); Auto with sets. +Intro H'0; Elim H'0; Auto with sets. +Intro H'0; Rewrite <- H'0; Auto with sets. +Qed. +Hints Resolve add_soustr_xy : sets v62. + +Lemma incl_st_add_soustr: + (X, Y: (Ensemble U)) (x: U) ~ (In U X x) -> + (Strict_Included U (Add U X x) Y) -> + (Strict_Included U X (Subtract U Y x)). +Proof. +Intros X Y x H' H'0; Apply sincl_add_x with x := x; Auto with sets. +Split. +Elim H'0. +Intros H'1 H'2. +Generalize (Inclusion_is_transitive U). +Intro H'4; Red in H'4. +Apply H'4 with y := Y; Auto with sets. +Red in H'0. +Elim H'0; Intros H'1 H'2; Try Exact H'1; Clear H'0. (* PB *) +Red; Intro H'0; Apply H'2. +Rewrite H'0; Auto 8 with sets. +Qed. + +Lemma Sub_Add_new: + (X: (Ensemble U)) (x: U) ~ (In U X x) -> X == (Subtract U (Add U X x) x). +Proof. +Auto with sets. +Qed. + +Lemma Simplify_add: + (X, X0 : (Ensemble U)) (x: U) + ~ (In U X x) -> ~ (In U X0 x) -> (Add U X x) == (Add U X0 x) -> X == X0. +Proof. +Intros X X0 x H' H'0 H'1; Try Assumption. +Rewrite (Sub_Add_new X x); Auto with sets. +Rewrite (Sub_Add_new X0 x); Auto with sets. +Rewrite H'1; Auto with sets. +Qed. + +Lemma Included_Add: + (X, A: (Ensemble U)) (x: U) (Included U X (Add U A x)) -> + (Included U X A) \/ + (EXT A' | X == (Add U A' x) /\ (Included U A' A)). +Proof. +Intros X A x H'0; Try Assumption. +Elim (classic (In U X x)). +Intro H'1; Right; Try Assumption. +Exists (Subtract U X x). +Split; Auto with sets. +Red in H'0. +Red. +Intros x0 H'2; Try Assumption. +LApply (Subtract_inv U X x x0); Auto with sets. +Intro H'3; Elim H'3; Intros K K'; Clear H'3. +LApply (H'0 x0); Auto with sets. +Intro H'3; Try Assumption. +LApply (Add_inv U A x x0); Auto with sets. +Intro H'4; Elim H'4; + [Intro H'5; Try Exact H'5; Clear H'4 | Intro H'5; Clear H'4]. +Elim K'; Auto with sets. +Intro H'1; Left; Try Assumption. +Red in H'0. +Red. +Intros x0 H'2; Try Assumption. +LApply (H'0 x0); Auto with sets. +Intro H'3; Try Assumption. +LApply (Add_inv U A x x0); Auto with sets. +Intro H'4; Elim H'4; + [Intro H'5; Try Exact H'5; Clear H'4 | Intro H'5; Clear H'4]. +Absurd (In U X x0); Auto with sets. +Rewrite <- H'5; Auto with sets. +Qed. + +Lemma setcover_inv: + (A: (Ensemble U)) + (x, y: (Ensemble U)) (covers (Ensemble U) (Power_set_PO U A) y x) -> + (Strict_Included U x y) /\ + ((z: (Ensemble U)) (Included U x z) -> (Included U z y) -> x == z \/ z == y). +Proof. +Intros A x y H'; Elim H'. +Unfold Strict_Rel_of; Simpl. +Intros H'0 H'1; Split; [Auto with sets | Idtac]. +Intros z H'2 H'3; Try Assumption. +Elim (classic x == z); Auto with sets. +Intro H'4; Right; Try Assumption. +Elim (classic z == y); Auto with sets. +Intro H'5; Try Assumption. +Elim H'1. +Exists z; Auto with sets. +Qed. + +Theorem Add_covers: + (A: (Ensemble U)) (a: (Ensemble U)) (Included U a A) -> + (x: U) (In U A x) -> ~ (In U a x) -> + (covers (Ensemble U) (Power_set_PO U A) (Add U a x) a). +Proof. +Intros A a H' x H'0 H'1; Try Assumption. +Apply setcover_intro; Auto with sets. +Red. +Split; [Idtac | Red; Intro H'2; Try Exact H'2]; Auto with sets. +Apply H'1. +Rewrite H'2; Auto with sets. +Red; Intro H'2; Elim H'2; Clear H'2. +Intros z H'2; Elim H'2; Intros H'3 H'4; Try Exact H'3; Clear H'2. +LApply (Strict_Included_inv U a z); Auto with sets; Clear H'3. +Intro H'2; Elim H'2; Intros H'3 H'5; Elim H'5; Clear H'2 H'5. +Intros x0 H'2; Elim H'2. +Intros H'5 H'6; Try Assumption. +Generalize H'4; Intro K. +Red in H'4. +Elim H'4; Intros H'8 H'9; Red in H'8; Clear H'4. +LApply (H'8 x0); Auto with sets. +Intro H'7; Try Assumption. +Elim (Add_inv U a x x0); Auto with sets. +Intro H'15. +Cut (Included U (Add U a x) z). +Intro H'10; Try Assumption. +Red in K. +Elim K; Intros H'11 H'12; Apply H'12; Clear K; Auto with sets. +Rewrite H'15. +Red. +Intros x1 H'10; Elim H'10; Auto with sets. +Intros x2 H'11; Elim H'11; Auto with sets. +Qed. + +Theorem covers_Add: + (A: (Ensemble U)) + (a, a': (Ensemble U)) + (Included U a A) -> + (Included U a' A) -> (covers (Ensemble U) (Power_set_PO U A) a' a) -> + (EXT x | a' == (Add U a x) /\ ((In U A x) /\ ~ (In U a x))). +Proof. +Intros A a a' H' H'0 H'1; Try Assumption. +Elim (setcover_inv A a a'); Auto with sets. +Intros H'6 H'7. +Clear H'1. +Elim (Strict_Included_inv U a a'); Auto with sets. +Intros H'5 H'8; Elim H'8. +Intros x H'1; Elim H'1. +Intros H'2 H'3; Try Assumption. +Exists x. +Split; [Try Assumption | Idtac]. +Clear H'8 H'1. +Elim (H'7 (Add U a x)); Auto with sets. +Intro H'1. +Absurd a ==(Add U a x); Auto with sets. +Red; Intro H'8; Try Exact H'8. +Apply H'3. +Rewrite H'8; Auto with sets. +Auto with sets. +Red. +Intros x0 H'1; Elim H'1; Auto with sets. +Intros x1 H'8; Elim H'8; Auto with sets. +Split; [Idtac | Try Assumption]. +Red in H'0; Auto with sets. +Qed. + +Theorem covers_is_Add: + (A: (Ensemble U)) + (a, a': (Ensemble U)) (Included U a A) -> (Included U a' A) -> + (iff + (covers (Ensemble U) (Power_set_PO U A) a' a) + (EXT x | a' == (Add U a x) /\ ((In U A x) /\ ~ (In U a x)))). +Proof. +Intros A a a' H' H'0; Split; Intro K. +Apply covers_Add with A := A; Auto with sets. +Elim K. +Intros x H'1; Elim H'1; Intros H'2 H'3; Rewrite H'2; Clear H'1. +Apply Add_covers; Intuition. +Qed. + +Theorem Singleton_atomic: + (x:U) (A:(Ensemble U)) (In U A x) -> + (covers (Ensemble U) (Power_set_PO U A) (Singleton U x) (Empty_set U)). +Intros x A H'. +Rewrite <- (Empty_set_zero' U x). +Apply Add_covers; Auto with sets. +Qed. + +Lemma less_than_singleton: + (X:(Ensemble U)) (x:U) (Strict_Included U X (Singleton U x)) -> + X ==(Empty_set U). +Intros X x H'; Try Assumption. +Red in H'. +LApply (Singleton_atomic x (Full_set U)); + [Intro H'2; Try Exact H'2 | Apply Full_intro]. +Elim H'; Intros H'0 H'1; Try Exact H'1; Clear H'. +Elim (setcover_inv (Full_set U) (Empty_set U) (Singleton U x)); + [Intros H'6 H'7; Try Exact H'7 | Idtac]; Auto with sets. +Elim (H'7 X); [Intro H'5; Try Exact H'5 | Intro H'5 | Idtac | Idtac]; Auto with sets. +Elim H'1; Auto with sets. +Qed. + +End Sets_as_an_algebra. + +Hints Resolve incl_soustr_in : sets v62. +Hints Resolve incl_soustr : sets v62. +Hints Resolve incl_soustr_add_l : sets v62. +Hints Resolve incl_soustr_add_r : sets v62. +Hints Resolve add_soustr_1 add_soustr_2 : sets v62. +Hints Resolve add_soustr_xy : sets v62. |