diff options
Diffstat (limited to 'theories/Sets/Powerset_Classical_facts.v')
| -rwxr-xr-x | theories/Sets/Powerset_Classical_facts.v | 342 |
1 files changed, 342 insertions, 0 deletions
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v new file mode 100755 index 00000000..05c60def --- /dev/null +++ b/theories/Sets/Powerset_Classical_facts.v @@ -0,0 +1,342 @@ +(************************************************************************) +(* 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.5.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. +Require Export Powerset_facts. +Require Export Classical_Type. +Require Export Classical_sets. + +Section Sets_as_an_algebra. + +Variable U : Type. + +Lemma sincl_add_x : + forall (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 in |- *. +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 in |- *; intro H'2. +elim H'0; clear H'0. +rewrite <- H'2; auto with sets. +Qed. + +Lemma incl_soustr_in : + forall (X:Ensemble U) (x:U), In U X x -> Included U (Subtract U X x) X. +Proof. +intros X x H'; red in |- *. +intros x0 H'0; elim H'0; auto with sets. +Qed. +Hint Resolve incl_soustr_in: sets v62. + +Lemma incl_soustr : + forall (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 in |- *. +intros x0 H'0; elim H'0. +intros H'1 H'2. +apply Subtract_intro; auto with sets. +Qed. +Hint Resolve incl_soustr: sets v62. + + +Lemma incl_soustr_add_l : + forall (X:Ensemble U) (x:U), Included U (Subtract U (Add U X x) x) X. +Proof. +intros X x; red in |- *. +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. +Hint Resolve incl_soustr_add_l: sets v62. + +Lemma incl_soustr_add_r : + forall (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 in |- *. +intros x0 H'0; try assumption. +apply Subtract_intro; auto with sets. +red in |- *; intro H'1; apply H'; rewrite H'1; auto with sets. +Qed. +Hint Resolve incl_soustr_add_r: sets v62. + +Lemma add_soustr_2 : + forall (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 in |- *. +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 : + forall (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 in |- *. +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. +Hint Resolve add_soustr_1 add_soustr_2: sets v62. + +Lemma add_soustr_xy : + forall (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 in |- *. +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. +Hint Resolve add_soustr_xy: sets v62. + +Lemma incl_st_add_soustr : + forall (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 in |- *; intro H'0; apply H'2. +rewrite H'0; auto 8 with sets. +Qed. + +Lemma Sub_Add_new : + forall (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 : + forall (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 : + forall (X A:Ensemble U) (x:U), + Included U X (Add U A x) -> + Included U X A \/ (exists 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 in |- *. +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 in |- *. +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 : + forall A x y:Ensemble U, + covers (Ensemble U) (Power_set_PO U A) y x -> + Strict_Included U x y /\ + (forall 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 in |- *; simpl in |- *. +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 : + forall A a:Ensemble U, + Included U a A -> + forall 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 in |- *. +split; [ idtac | red in |- *; intro H'2; try exact H'2 ]; auto with sets. +apply H'1. +rewrite H'2; auto with sets. +red in |- *; 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 in |- *. +intros x1 H'10; elim H'10; auto with sets. +intros x2 H'11; elim H'11; auto with sets. +Qed. + +Theorem covers_Add : + forall A a a':Ensemble U, + Included U a A -> + Included U a' A -> + covers (Ensemble U) (Power_set_PO U A) a' a -> + exists 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 in |- *; intro H'8; try exact H'8. +apply H'3. +rewrite H'8; auto with sets. +auto with sets. +red in |- *. +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 : + forall A a a':Ensemble U, + Included U a A -> + Included U a' A -> + (covers (Ensemble U) (Power_set_PO U A) a' a <-> + (exists 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 : + forall (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 : + forall (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. + +Hint Resolve incl_soustr_in: sets v62. +Hint Resolve incl_soustr: sets v62. +Hint Resolve incl_soustr_add_l: sets v62. +Hint Resolve incl_soustr_add_r: sets v62. +Hint Resolve add_soustr_1 add_soustr_2: sets v62. +Hint Resolve add_soustr_xy: sets v62.
\ No newline at end of file |