diff options
Diffstat (limited to 'theories/Sets/Powerset_Classical_facts.v')
-rwxr-xr-x | theories/Sets/Powerset_Classical_facts.v | 486 |
1 files changed, 245 insertions, 241 deletions
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v index 6b3443b7d..988bbd25a 100755 --- a/theories/Sets/Powerset_Classical_facts.v +++ b/theories/Sets/Powerset_Classical_facts.v @@ -39,300 +39,304 @@ Require Export Classical_sets. Section Sets_as_an_algebra. -Variable U: Type. +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). +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. -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. +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: - (X: (Ensemble U)) (x: U) (In U X x) -> (Included U (Subtract U X x) X). +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. -Intros x0 H'0; Elim H'0; Auto with sets. +intros X x H'; red in |- *. +intros x0 H'0; elim H'0; auto with sets. Qed. -Hints Resolve incl_soustr_in : sets v62. +Hint 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)). +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. -Intros x0 H'0; Elim H'0. -Intros H'1 H'2. -Apply Subtract_intro; Auto with sets. +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. -Hints Resolve incl_soustr : sets v62. +Hint 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). +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. -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. +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. -Hints Resolve incl_soustr_add_l : sets v62. +Hint 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)). +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. -Intros x0 H'0; Try Assumption. -Apply Subtract_intro; Auto with sets. -Red; Intro H'1; Apply H'; Rewrite H'1; Auto with sets. +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. -Hints Resolve incl_soustr_add_r : sets v62. +Hint 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)). +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. -Intros x0 H'0; Try Assumption. -Elim (classic x == x0); Intro K; Auto with sets. -Elim K; Auto with sets. +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: - (X: (Ensemble U)) (x: U) (In U X x) -> - (Included U (Add U (Subtract U X x) x) X). +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. -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. +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. -Hints Resolve add_soustr_1 add_soustr_2 : sets v62. +Hint 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). +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. -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. +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. -Hints Resolve add_soustr_xy : sets v62. +Hint 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)). +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; Intro H'0; Apply H'2. -Rewrite H'0; Auto 8 with sets. +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: - (X: (Ensemble U)) (x: U) ~ (In U X x) -> X == (Subtract U (Add U X x) x). +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. +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. +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. +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)). +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. -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. +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: - (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). +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; 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. +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: - (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). +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. -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. +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: - (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))). +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; 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. +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: - (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)))). +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. +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. +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: - (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. +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. -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. +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 |