diff options
Diffstat (limited to 'theories/Sets/Powerset_Classical_facts.v')
| -rw-r--r-- | theories/Sets/Powerset_Classical_facts.v | 578 |
1 files changed, 287 insertions, 291 deletions
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v index 210017d4..47857705 100644 --- a/theories/Sets/Powerset_Classical_facts.v +++ b/theories/Sets/Powerset_Classical_facts.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id: Powerset_Classical_facts.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Powerset_Classical_facts.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Export Ensembles. Require Export Constructive_sets. @@ -39,298 +39,294 @@ Require Export Classical_sets. Section Sets_as_an_algebra. -Variable U : Type. + 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 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. + + 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. + + 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. -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. + + 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. + + 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 using add_soustr_1 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 using add_soustr_2 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 using add_soustr_xy, add_soustr_1, add_soustr_2 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 using incl_soustr_add_l 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 using incl_soustr_in, add_soustr_xy, add_soustr_1, add_soustr_2 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. -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. + 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). + Proof. + 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. + Proof. + 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. @@ -339,4 +335,4 @@ 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 +Hint Resolve add_soustr_xy: sets v62. |