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, 72 insertions, 63 deletions

diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index 3702387a7..bfb42b7b9 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -8,104 +8,113 @@
 
 (*i $Id$ i*)
 
-Require Relations.
-Require PolyList.
-Require Multiset.
+Require Import Relations.
+Require Import List.
+Require Import Multiset.
 
 Set Implicit Arguments.
 
 Section defs.
 
 Variable A : Set.
-Variable leA : (relation A).
-Variable eqA : (relation A).
+Variable leA : relation A.
+Variable eqA : relation A.
 
-Local gtA := [x,y:A]~(leA x y).
+Let gtA (x y:A) := ~ leA x y.
 
-Hypothesis leA_dec : (x,y:A){(leA x y)}+{~(leA x y)}.
-Hypothesis eqA_dec : (x,y:A){(eqA x y)}+{~(eqA x y)}.
-Hypothesis leA_refl : (x,y:A) (eqA x y) -> (leA x y).
-Hypothesis leA_trans : (x,y,z:A) (leA x y) -> (leA y z) -> (leA x z).
-Hypothesis leA_antisym : (x,y:A)(leA x y) -> (leA y x) -> (eqA x y).
+Hypothesis leA_dec : forall x y:A, {leA x y} + {~ leA x y}.
+Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y.
+Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z.
+Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y.
 
-Hints Resolve leA_refl : default.
-Hints Immediate eqA_dec leA_dec leA_antisym : default.
+Hint Resolve leA_refl: default.
+Hint Immediate eqA_dec leA_dec leA_antisym: default.
 
-Local emptyBag := (EmptyBag A).
-Local singletonBag := (SingletonBag eqA_dec).
+Let emptyBag := EmptyBag A.
+Let singletonBag := SingletonBag _ eqA_dec.
 
 (** contents of a list *)
 
-Fixpoint list_contents [l:(list A)] : (multiset A) :=
- Cases l of
-   nil        => emptyBag
- | (cons a l) => (munion (singletonBag a) (list_contents l))
- end.
+Fixpoint list_contents (l:list A) : multiset A :=
+  match l with
+  | nil => emptyBag
+  | a :: l => munion (singletonBag a) (list_contents l)
+  end.
 
-Lemma list_contents_app : (l,m:(list A))
-  (meq (list_contents (app l m)) (munion (list_contents l) (list_contents m))).
+Lemma list_contents_app :
+ forall l m:list A,
+   meq (list_contents (l ++ m)) (munion (list_contents l) (list_contents m)).
 Proof.
-Induction l; Simpl; Auto with datatypes.
-Intros.
-Apply meq_trans with  
- (munion (singletonBag a) (munion (list_contents l0) (list_contents m))); Auto with datatypes.
+simple induction l; simpl in |- *; auto with datatypes.
+intros.
+apply meq_trans with
+ (munion (singletonBag a) (munion (list_contents l0) (list_contents m)));
+ auto with datatypes.
 Qed.
-Hints Resolve list_contents_app.
+Hint Resolve list_contents_app.
 
-Definition permutation := [l,m:(list A)](meq (list_contents l) (list_contents m)).
+Definition permutation (l m:list A) :=
+  meq (list_contents l) (list_contents m).
 
-Lemma permut_refl : (l:(list A))(permutation l l).
+Lemma permut_refl : forall l:list A, permutation l l.
 Proof.
-Unfold permutation; Auto with datatypes.
+unfold permutation in |- *; auto with datatypes.
 Qed.
-Hints Resolve permut_refl.
+Hint Resolve permut_refl.
 
-Lemma permut_tran : (l,m,n:(list A))
-   (permutation l m) -> (permutation m n) -> (permutation l n).
+Lemma permut_tran :
+ forall l m n:list A, permutation l m -> permutation m n -> permutation l n.
 Proof.
-Unfold permutation; Intros.
-Apply meq_trans with (list_contents m); Auto with datatypes.
+unfold permutation in |- *; intros.
+apply meq_trans with (list_contents m); auto with datatypes.
 Qed.
 
-Lemma permut_right : (l,m:(list A))
-   (permutation l m) -> (a:A)(permutation (cons a l) (cons a m)).
+Lemma permut_right :
+ forall l m:list A,
+   permutation l m -> forall a:A, permutation (a :: l) (a :: m).
 Proof.
-Unfold permutation; Simpl; Auto with datatypes.
+unfold permutation in |- *; simpl in |- *; auto with datatypes.
 Qed.
-Hints Resolve permut_right.
+Hint Resolve permut_right.
 
-Lemma permut_app : (l,l',m,m':(list A))
-   (permutation l l') -> (permutation m m') ->
-   (permutation (app l m) (app l' m')).
+Lemma permut_app :
+ forall l l' m m':list A,
+   permutation l l' -> permutation m m' -> permutation (l ++ m) (l' ++ m').
 Proof.
-Unfold permutation; Intros.
-Apply meq_trans with (munion (list_contents l) (list_contents m)); Auto with datatypes.
-Apply meq_trans with (munion (list_contents l') (list_contents m')); Auto with datatypes.
-Apply meq_trans with (munion (list_contents l') (list_contents m)); Auto with datatypes.
+unfold permutation in |- *; intros.
+apply meq_trans with (munion (list_contents l) (list_contents m));
+ auto with datatypes.
+apply meq_trans with (munion (list_contents l') (list_contents m'));
+ auto with datatypes.
+apply meq_trans with (munion (list_contents l') (list_contents m));
+ auto with datatypes.
 Qed.
-Hints Resolve permut_app.
+Hint Resolve permut_app.
 
-Lemma permut_cons : (l,m:(list A))(permutation l m) ->
-    (a:A)(permutation (cons a l) (cons a m)).
+Lemma permut_cons :
+ forall l m:list A,
+   permutation l m -> forall a:A, permutation (a :: l) (a :: m).
 Proof.
-Intros l m H a.
-Change (permutation (app (cons a (nil A)) l) (app (cons a (nil A)) m)).
-Apply permut_app; Auto with datatypes.
+intros l m H a.
+change (permutation ((a :: nil) ++ l) ((a :: nil) ++ m)) in |- *.
+apply permut_app; auto with datatypes.
 Qed.
-Hints Resolve permut_cons.
+Hint Resolve permut_cons.
 
-Lemma permut_middle : (l,m:(list A))
-   (a:A)(permutation (cons a (app l m)) (app l (cons a m))).
+Lemma permut_middle :
+ forall (l m:list A) (a:A), permutation (a :: l ++ m) (l ++ a :: m).
 Proof.
-Unfold permutation.
-Induction l; Simpl; Auto with datatypes.
-Intros.
-Apply meq_trans with (munion (singletonBag a)
-          (munion (singletonBag a0) (list_contents (app l0 m)))); Auto with datatypes.
-Apply munion_perm_left; Auto with datatypes.
+unfold permutation in |- *.
+simple induction l; simpl in |- *; auto with datatypes.
+intros.
+apply meq_trans with
+ (munion (singletonBag a)
+    (munion (singletonBag a0) (list_contents (l0 ++ m))));
+ auto with datatypes.
+apply munion_perm_left; auto with datatypes.
 Qed.
-Hints Resolve permut_middle.
+Hint Resolve permut_middle.
 
 End defs.
 Unset Implicit Arguments.
-