summaryrefslogtreecommitdiff
path: root/theories/Sets/Powerset.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
commitdb38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch)
tree09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /theories/Sets/Powerset.v
parent6e34b272d789455a9be589e27ad3a998cf25496b (diff)
parent499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff)
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'theories/Sets/Powerset.v')
-rw-r--r--theories/Sets/Powerset.v32
1 files changed, 15 insertions, 17 deletions
diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v
index 372473d6..cdbeaf7b 100644
--- a/theories/Sets/Powerset.v
+++ b/theories/Sets/Powerset.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -24,8 +24,6 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Powerset.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export Ensembles.
Require Export Relations_1.
Require Export Relations_1_facts.
@@ -41,7 +39,7 @@ Inductive Power_set (A:Ensemble U) : Ensemble (Ensemble U) :=
Hint Resolve Definition_of_Power_set.
Theorem Empty_set_minimal : forall X:Ensemble U, Included U (Empty_set U) X.
-intro X; red in |- *.
+intro X; red.
intros x H'; elim H'.
Qed.
Hint Resolve Empty_set_minimal.
@@ -81,7 +79,7 @@ Lemma Strict_inclusion_is_transitive_with_inclusion :
Strict_Included U x y -> Included U y z -> Strict_Included U x z.
intros x y z H' H'0; try assumption.
elim Strict_Rel_is_Strict_Included.
-unfold contains in |- *.
+unfold contains.
intros H'1 H'2; try assumption.
apply H'1.
apply Strict_Rel_Transitive_with_Rel with (y := y); auto with sets.
@@ -92,7 +90,7 @@ Lemma Strict_inclusion_is_transitive_with_inclusion_left :
Included U x y -> Strict_Included U y z -> Strict_Included U x z.
intros x y z H' H'0; try assumption.
elim Strict_Rel_is_Strict_Included.
-unfold contains in |- *.
+unfold contains.
intros H'1 H'2; try assumption.
apply H'1.
apply Strict_Rel_Transitive_with_Rel_left with (y := y); auto with sets.
@@ -107,14 +105,14 @@ Qed.
Theorem Empty_set_is_Bottom :
forall A:Ensemble U, Bottom (Ensemble U) (Power_set_PO A) (Empty_set U).
-intro A; apply Bottom_definition; simpl in |- *; auto with sets.
+intro A; apply Bottom_definition; simpl; auto with sets.
Qed.
Hint Resolve Empty_set_is_Bottom.
Theorem Union_minimal :
forall a b X:Ensemble U,
Included U a X -> Included U b X -> Included U (Union U a b) X.
-intros a b X H' H'0; red in |- *.
+intros a b X H' H'0; red.
intros x H'1; elim H'1; auto with sets.
Qed.
Hint Resolve Union_minimal.
@@ -135,13 +133,13 @@ Qed.
Theorem Intersection_decreases_l :
forall a b:Ensemble U, Included U (Intersection U a b) a.
-intros a b; red in |- *.
+intros a b; red.
intros x H'; elim H'; auto with sets.
Qed.
Theorem Intersection_decreases_r :
forall a b:Ensemble U, Included U (Intersection U a b) b.
-intros a b; red in |- *.
+intros a b; red.
intros x H'; elim H'; auto with sets.
Qed.
Hint Resolve Union_increases_l Union_increases_r Intersection_decreases_l
@@ -153,10 +151,10 @@ Theorem Union_is_Lub :
Included U b A ->
Lub (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b) (Union U a b).
intros A a b H' H'0.
-apply Lub_definition; simpl in |- *.
-apply Upper_Bound_definition; simpl in |- *; auto with sets.
+apply Lub_definition; simpl.
+apply Upper_Bound_definition; simpl; auto with sets.
intros y H'1; elim H'1; auto with sets.
-intros y H'1; elim H'1; simpl in |- *; auto with sets.
+intros y H'1; elim H'1; simpl; auto with sets.
Qed.
Theorem Intersection_is_Glb :
@@ -166,13 +164,13 @@ Theorem Intersection_is_Glb :
Glb (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b)
(Intersection U a b).
intros A a b H' H'0.
-apply Glb_definition; simpl in |- *.
-apply Lower_Bound_definition; simpl in |- *; auto with sets.
+apply Glb_definition; simpl.
+apply Lower_Bound_definition; simpl; auto with sets.
apply Definition_of_Power_set.
generalize Inclusion_is_transitive; intro IT; red in IT; apply IT with a;
auto with sets.
intros y H'1; elim H'1; auto with sets.
-intros y H'1; elim H'1; simpl in |- *; auto with sets.
+intros y H'1; elim H'1; simpl; auto with sets.
Qed.
End The_power_set_partial_order.
@@ -187,4 +185,4 @@ Hint Resolve Union_increases_r: sets v62.
Hint Resolve Intersection_decreases_l: sets v62.
Hint Resolve Intersection_decreases_r: sets v62.
Hint Resolve Empty_set_is_Bottom: sets v62.
-Hint Resolve Strict_inclusion_is_transitive: sets v62. \ No newline at end of file
+Hint Resolve Strict_inclusion_is_transitive: sets v62.