Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 139 insertions, 147 deletions

diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
index 3e1837078..c587744a3 100755
--- a/theories/Sets/Powerset_facts.v
+++ b/theories/Sets/Powerset_facts.v
@@ -35,242 +35,234 @@ Require Export Cpo.
 Require Export Powerset.
 
 Section Sets_as_an_algebra.
-Variable U: Type.
-Hints Unfold not.
+Variable U : Type.
+Hint Unfold not.
 
-Theorem Empty_set_zero :
-  (X: (Ensemble U)) (Union U (Empty_set U) X) == X.
+Theorem Empty_set_zero : forall X:Ensemble U, Union U (Empty_set U) X = X.
 Proof.
-Auto 6 with sets.
+auto 6 with sets.
 Qed.
-Hints Resolve Empty_set_zero.
+Hint Resolve Empty_set_zero.
 
-Theorem Empty_set_zero' :
-  (x: U) (Add U (Empty_set U) x) == (Singleton U x).
+Theorem Empty_set_zero' : forall x:U, Add U (Empty_set U) x = Singleton U x.
 Proof.
-Unfold 1 Add; Auto with sets.
+unfold Add at 1 in |- *; auto with sets.
 Qed.
-Hints Resolve Empty_set_zero'.
+Hint Resolve Empty_set_zero'.
 
 Lemma less_than_empty :
-  (X: (Ensemble U)) (Included U X (Empty_set U)) -> X == (Empty_set U).
+ forall X:Ensemble U, Included U X (Empty_set U) -> X = Empty_set U.
 Proof.
-Auto with sets.
+auto with sets.
 Qed.
-Hints Resolve less_than_empty.
+Hint Resolve less_than_empty.
 
-Theorem Union_commutative :
-  (A,B: (Ensemble U)) (Union U A B) == (Union U B A).
+Theorem Union_commutative : forall A B:Ensemble U, Union U A B = Union U B A.
 Proof.
-Auto with sets.
+auto with sets.
 Qed.
 
 Theorem Union_associative :
-  (A, B, C: (Ensemble U))
-  (Union U (Union U A B) C) == (Union U A (Union U B C)).
+ forall A B C:Ensemble U, Union U (Union U A B) C = Union U A (Union U B C).
 Proof.
-Auto 9 with sets.
+auto 9 with sets.
 Qed.
-Hints Resolve Union_associative.
+Hint Resolve Union_associative.
 
-Theorem Union_idempotent : (A: (Ensemble U)) (Union U A A) == A.
+Theorem Union_idempotent : forall A:Ensemble U, Union U A A = A.
 Proof.
-Auto 7 with sets.
+auto 7 with sets.
 Qed.
 
 Lemma Union_absorbs :
-  (A, B: (Ensemble U)) (Included U B A) -> (Union U A B) == A.
+ forall A B:Ensemble U, Included U B A -> Union U A B = A.
 Proof.
-Auto 7 with sets.
+auto 7 with sets.
 Qed.
 
-Theorem Couple_as_union:
-  (x, y: U) (Union U (Singleton U x) (Singleton U y)) == (Couple U x y).
+Theorem Couple_as_union :
+ forall x y:U, Union U (Singleton U x) (Singleton U y) = Couple U x y.
 Proof.
-Intros x y; Apply Extensionality_Ensembles; Split; Red.
-Intros x0 H'; Elim H'; (Intros x1 H'0; Elim H'0; Auto with sets).
-Intros x0 H'; Elim H'; Auto with sets.
+intros x y; apply Extensionality_Ensembles; split; red in |- *.
+intros x0 H'; elim H'; (intros x1 H'0; elim H'0; auto with sets).
+intros x0 H'; elim H'; auto with sets.
 Qed.
 
 Theorem Triple_as_union :
-  (x, y, z: U)
-  (Union U (Union U (Singleton U x) (Singleton U y)) (Singleton U z)) ==
-  (Triple U x y z).
+ forall x y z:U,
+   Union U (Union U (Singleton U x) (Singleton U y)) (Singleton U z) =
+   Triple U x y z.
 Proof.
-Intros x y z; Apply Extensionality_Ensembles; Split; Red.
-Intros x0 H'; Elim H'.
-Intros x1 H'0; Elim H'0; (Intros x2 H'1; Elim H'1; Auto with sets).
-Intros x1 H'0; Elim H'0; Auto with sets.
-Intros x0 H'; Elim H'; Auto with sets.
+intros x y z; apply Extensionality_Ensembles; split; red in |- *.
+intros x0 H'; elim H'.
+intros x1 H'0; elim H'0; (intros x2 H'1; elim H'1; auto with sets).
+intros x1 H'0; elim H'0; auto with sets.
+intros x0 H'; elim H'; auto with sets.
 Qed.
 
-Theorem Triple_as_Couple : (x, y: U) (Couple U x y) == (Triple U x x y).
+Theorem Triple_as_Couple : forall x y:U, Couple U x y = Triple U x x y.
 Proof.
-Intros x y.
-Rewrite <- (Couple_as_union x y).
-Rewrite <- (Union_idempotent (Singleton U x)).
-Apply Triple_as_union.
+intros x y.
+rewrite <- (Couple_as_union x y).
+rewrite <- (Union_idempotent (Singleton U x)).
+apply Triple_as_union.
 Qed.
 
 Theorem Triple_as_Couple_Singleton :
-  (x, y, z: U) (Triple U x y z) == (Union U (Couple U x y) (Singleton U z)).
+ forall x y z:U, Triple U x y z = Union U (Couple U x y) (Singleton U z).
 Proof.
-Intros x y z.
-Rewrite <- (Triple_as_union x y z).
-Rewrite <- (Couple_as_union x y); Auto with sets.
+intros x y z.
+rewrite <- (Triple_as_union x y z).
+rewrite <- (Couple_as_union x y); auto with sets.
 Qed.
 
 Theorem Intersection_commutative :
-  (A,B: (Ensemble U)) (Intersection U A B) == (Intersection U B A).
+ forall A B:Ensemble U, Intersection U A B = Intersection U B A.
 Proof.
-Intros A B.
-Apply Extensionality_Ensembles.
-Split; Red; Intros x H'; Elim H'; Auto with sets.
+intros A B.
+apply Extensionality_Ensembles.
+split; red in |- *; intros x H'; elim H'; auto with sets.
 Qed.
 
 Theorem Distributivity :
-  (A, B, C: (Ensemble U))
-     (Intersection U A (Union U B C)) ==
-     (Union U (Intersection U A B) (Intersection U A C)).
+ forall A B C:Ensemble U,
+   Intersection U A (Union U B C) =
+   Union U (Intersection U A B) (Intersection U A C).
 Proof.
-Intros A B C.
-Apply Extensionality_Ensembles.
-Split; Red; Intros x H'.
-Elim H'.
-Intros x0 H'0 H'1; Generalize H'0.
-Elim H'1; Auto with sets.
-Elim H'; Intros x0 H'0; Elim H'0; Auto with sets.
+intros A B C.
+apply Extensionality_Ensembles.
+split; red in |- *; intros x H'.
+elim H'.
+intros x0 H'0 H'1; generalize H'0.
+elim H'1; auto with sets.
+elim H'; intros x0 H'0; elim H'0; auto with sets.
 Qed.
 
 Theorem Distributivity' :
-  (A, B, C: (Ensemble U))
-     (Union U A (Intersection U B C)) ==
-     (Intersection U (Union U A B) (Union U A C)).
+ forall A B C:Ensemble U,
+   Union U A (Intersection U B C) =
+   Intersection U (Union U A B) (Union U A C).
 Proof.
-Intros A B C.
-Apply Extensionality_Ensembles.
-Split; Red; Intros x H'.
-Elim H'; Auto with sets.
-Intros x0 H'0; Elim H'0; Auto with sets.
-Elim H'.
-Intros x0 H'0; Elim H'0; Auto with sets.
-Intros x1 H'1 H'2; Try Exact H'2.
-Generalize H'1.
-Elim H'2; Auto with sets.
+intros A B C.
+apply Extensionality_Ensembles.
+split; red in |- *; intros x H'.
+elim H'; auto with sets.
+intros x0 H'0; elim H'0; auto with sets.
+elim H'.
+intros x0 H'0; elim H'0; auto with sets.
+intros x1 H'1 H'2; try exact H'2.
+generalize H'1.
+elim H'2; auto with sets.
 Qed.
 
 Theorem Union_add :
-  (A, B: (Ensemble U)) (x: U)
-    (Add U (Union U A B) x) == (Union U A (Add U B x)).
+ forall (A B:Ensemble U) (x:U), Add U (Union U A B) x = Union U A (Add U B x).
 Proof.
-Unfold Add; Auto with sets.
+unfold Add in |- *; auto with sets.
 Qed.
-Hints Resolve Union_add.
+Hint Resolve Union_add.
 
 Theorem Non_disjoint_union :
-  (X: (Ensemble U)) (x: U) (In U X x) -> (Add U X x) == X.
-Intros X x H'; Unfold Add.
-Apply Extensionality_Ensembles; Red.
-Split; Red; Auto with sets.
-Intros x0 H'0; Elim H'0; Auto with sets.
-Intros t H'1; Elim H'1; Auto with sets.
+ forall (X:Ensemble U) (x:U), In U X x -> Add U X x = X.
+intros X x H'; unfold Add in |- *.
+apply Extensionality_Ensembles; red in |- *.
+split; red in |- *; auto with sets.
+intros x0 H'0; elim H'0; auto with sets.
+intros t H'1; elim H'1; auto with sets.
 Qed.
 
 Theorem Non_disjoint_union' :
-  (X: (Ensemble U)) (x: U) ~ (In U X x) -> (Subtract U X x) == X.
+ forall (X:Ensemble U) (x:U), ~ In U X x -> Subtract U X x = X.
 Proof.
-Intros X x H'; Unfold Subtract.
-Apply Extensionality_Ensembles.
-Split; Red; Auto with sets.
-Intros x0 H'0; Elim H'0; Auto with sets.
-Intros x0 H'0; Apply Setminus_intro; Auto with sets.
-Red; Intro H'1; Elim H'1.
-LApply (Singleton_inv U x x0); Auto with sets.
-Intro H'4; Apply H'; Rewrite H'4; Auto with sets.
+intros X x H'; unfold Subtract in |- *.
+apply Extensionality_Ensembles.
+split; red in |- *; auto with sets.
+intros x0 H'0; elim H'0; auto with sets.
+intros x0 H'0; apply Setminus_intro; auto with sets.
+red in |- *; intro H'1; elim H'1.
+lapply (Singleton_inv U x x0); auto with sets.
+intro H'4; apply H'; rewrite H'4; auto with sets.
 Qed.
 
-Lemma singlx : (x, y: U) (In U (Add U (Empty_set U) x) y) -> x == y.
+Lemma singlx : forall x y:U, In U (Add U (Empty_set U) x) y -> x = y.
 Proof.
-Intro x; Rewrite (Empty_set_zero' x); Auto with sets.
+intro x; rewrite (Empty_set_zero' x); auto with sets.
 Qed.
-Hints Resolve singlx.
+Hint Resolve singlx.
 
 Lemma incl_add :
-  (A, B: (Ensemble U)) (x: U) (Included U A B) ->
-   (Included U (Add U A x) (Add U B x)).
+ forall (A B:Ensemble U) (x:U),
+   Included U A B -> Included U (Add U A x) (Add U B x).
 Proof.
-Intros A B x H'; Red; Auto with sets.
-Intros x0 H'0.
-LApply (Add_inv U A x x0); Auto with sets.
-Intro H'1; Elim H'1;
- [Intro H'2; Clear H'1 | Intro H'2; Rewrite <- H'2; Clear H'1]; Auto with sets.
+intros A B x H'; red in |- *; auto with sets.
+intros x0 H'0.
+lapply (Add_inv U A x x0); auto with sets.
+intro H'1; elim H'1;
+ [ intro H'2; clear H'1 | intro H'2; rewrite <- H'2; clear H'1 ];
+ auto with sets.
 Qed.
-Hints Resolve incl_add.
+Hint Resolve incl_add.
 
 Lemma incl_add_x :
-  (A, B: (Ensemble U))
-  (x: U) ~ (In U A x) -> (Included U (Add U A x) (Add U B x)) ->
-   (Included U A B).
+ forall (A B:Ensemble U) (x:U),
+   ~ In U A x -> Included U (Add U A x) (Add U B x) -> Included U A B.
 Proof.
-Unfold Included.
-Intros A B x H' H'0 x0 H'1.
-LApply (H'0 x0); Auto with sets.
-Intro H'2; LApply (Add_inv U B x x0); Auto with sets.
-Intro H'3; Elim H'3;
- [Intro H'4; Try Exact H'4; Clear H'3 | Intro H'4; Clear H'3].
-Absurd (In U A x0); Auto with sets.
-Rewrite <- H'4; Auto with sets.
+unfold Included in |- *.
+intros A B x H' H'0 x0 H'1.
+lapply (H'0 x0); auto with sets.
+intro H'2; lapply (Add_inv U B x x0); auto with sets.
+intro H'3; elim H'3;
+ [ intro H'4; try exact H'4; clear H'3 | intro H'4; clear H'3 ].
+absurd (In U A x0); auto with sets.
+rewrite <- H'4; auto with sets.
 Qed.
 
 Lemma Add_commutative :
-  (A: (Ensemble U)) (x, y: U) (Add U (Add U A x) y) == (Add U (Add U A y) x).
+ forall (A:Ensemble U) (x y:U), Add U (Add U A x) y = Add U (Add U A y) x.
 Proof.
-Intros A x y.
-Unfold Add.
-Rewrite (Union_associative A (Singleton U x) (Singleton U y)).
-Rewrite (Union_commutative (Singleton U x) (Singleton U y)).
-Rewrite <- (Union_associative A (Singleton U y) (Singleton U x)); Auto with sets.
+intros A x y.
+unfold Add in |- *.
+rewrite (Union_associative A (Singleton U x) (Singleton U y)).
+rewrite (Union_commutative (Singleton U x) (Singleton U y)).
+rewrite <- (Union_associative A (Singleton U y) (Singleton U x));
+ auto with sets.
 Qed.
 
 Lemma Add_commutative' :
-  (A: (Ensemble U)) (x, y, z: U)
-    (Add U (Add U (Add U A x) y) z) == (Add U (Add U (Add U A z) x) y).
+ forall (A:Ensemble U) (x y z:U),
+   Add U (Add U (Add U A x) y) z = Add U (Add U (Add U A z) x) y.
 Proof.
-Intros A x y z.
-Rewrite (Add_commutative (Add U A x) y z).
-Rewrite (Add_commutative A x z); Auto with sets.
+intros A x y z.
+rewrite (Add_commutative (Add U A x) y z).
+rewrite (Add_commutative A x z); auto with sets.
 Qed.
 
 Lemma Add_distributes :
-  (A, B: (Ensemble U)) (x, y: U) (Included U B A) ->
-  (Add U (Add U A x) y) == (Union U (Add U A x) (Add U B y)).
+ forall (A B:Ensemble U) (x y:U),
+   Included U B A -> Add U (Add U A x) y = Union U (Add U A x) (Add U B y).
 Proof.
-Intros A B x y H'; Try Assumption.
-Rewrite <- (Union_add (Add U A x) B y).
-Unfold 4 Add.
-Rewrite (Union_commutative A (Singleton U x)).
-Rewrite Union_associative.
-Rewrite (Union_absorbs A B H').
-Rewrite (Union_commutative (Singleton U x) A).
-Auto with sets.
+intros A B x y H'; try assumption.
+rewrite <- (Union_add (Add U A x) B y).
+unfold Add at 4 in |- *.
+rewrite (Union_commutative A (Singleton U x)).
+rewrite Union_associative.
+rewrite (Union_absorbs A B H').
+rewrite (Union_commutative (Singleton U x) A).
+auto with sets.
 Qed.
 
 Lemma setcover_intro :
-  (U: Type)
-  (A: (Ensemble U))
-  (x, y: (Ensemble U))
-  (Strict_Included U x y) ->
-  ~ (EXT z | (Strict_Included U x z) 
-              /\ (Strict_Included U z y)) ->
-   (covers (Ensemble U) (Power_set_PO U A) y x).
+ forall (U:Type) (A x y:Ensemble U),
+   Strict_Included U x y ->
+   ~ ( exists z : _ | Strict_Included U x z /\ Strict_Included U z y) ->
+   covers (Ensemble U) (Power_set_PO U A) y x.
 Proof.
-Intros; Apply Definition_of_covers; Auto with sets.
+intros; apply Definition_of_covers; auto with sets.
 Qed.
-Hints Resolve setcover_intro.
+Hint Resolve setcover_intro.
 
 End Sets_as_an_algebra.
 
-Hints Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add
-	singlx incl_add : sets v62.
-
+Hint Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add
+  singlx incl_add: sets v62.