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, 93 insertions, 101 deletions

diff --git a/contrib/correctness/ArrayPermut.v b/contrib/correctness/ArrayPermut.v
index 55259b943d..4223a05471 100644
--- a/contrib/correctness/ArrayPermut.v
+++ b/contrib/correctness/ArrayPermut.v
@@ -15,11 +15,11 @@
 (*                        Definition and properties                         *)
 (****************************************************************************)
 
-Require ProgInt.
-Require Arrays.
+Require Import ProgInt.
+Require Import Arrays.
 Require Export Exchange.
 
-Require Omega.
+Require Import Omega.
 
 Set Implicit Arguments.
 
@@ -27,18 +27,16 @@ Set Implicit Arguments.
  * transpositions i.e. exchange of two elements.
  *)
 
-Inductive permut [n:Z; A:Set] : (array n A)->(array n A)->Prop :=
-    exchange_is_permut : 
-      (t,t':(array n A))(i,j:Z)(exchange t t' i j) -> (permut t t')
-  | permut_refl : 
-      (t:(array n A))(permut t t)
-  | permut_sym : 
-      (t,t':(array n A))(permut t t') -> (permut t' t)
-  | permut_trans : 
-      (t,t',t'':(array n A))
-      (permut t t') -> (permut t' t'') -> (permut t t'').
+Inductive permut (n:Z) (A:Set) : array n A -> array n A -> Prop :=
+  | exchange_is_permut :
+      forall (t t':array n A) (i j:Z), exchange t t' i j -> permut t t'
+  | permut_refl : forall t:array n A, permut t t
+  | permut_sym : forall t t':array n A, permut t t' -> permut t' t
+  | permut_trans :
+      forall t t' t'':array n A, permut t t' -> permut t' t'' -> permut t t''.
 
-Hints Resolve exchange_is_permut permut_refl permut_sym permut_trans : v62 datatypes.
+Hint Resolve exchange_is_permut permut_refl permut_sym permut_trans: v62
+  datatypes.
 
 (* We also define the permutation on a segment of an array, "sub_permut",
  * the other parts of the array being unchanged
@@ -47,137 +45,131 @@ Hints Resolve exchange_is_permut permut_refl permut_sym permut_trans : v62 datat
  * transpositions on the given segment.
  *)
 
-Inductive sub_permut [n:Z; A:Set; g,d:Z] : (array n A)->(array n A)->Prop :=
-    exchange_is_sub_permut : 
-      (t,t':(array n A))(i,j:Z)`g <= i <= d` -> `g <= j <= d`
-      -> (exchange t t' i j) -> (sub_permut g d t t')
-  | sub_permut_refl : 
-      (t:(array n A))(sub_permut g d t t)
-  | sub_permut_sym : 
-      (t,t':(array n A))(sub_permut g d t t') -> (sub_permut g d t' t)
-  | sub_permut_trans : 
-      (t,t',t'':(array n A))
-      (sub_permut g d t t') -> (sub_permut g d t' t'') 
-      -> (sub_permut g d t t'').
-
-Hints Resolve exchange_is_sub_permut sub_permut_refl sub_permut_sym sub_permut_trans
-  : v62 datatypes.
+Inductive sub_permut (n:Z) (A:Set) (g d:Z) :
+array n A -> array n A -> Prop :=
+  | exchange_is_sub_permut :
+      forall (t t':array n A) (i j:Z),
+        (g <= i <= d)%Z ->
+        (g <= j <= d)%Z -> exchange t t' i j -> sub_permut g d t t'
+  | sub_permut_refl : forall t:array n A, sub_permut g d t t
+  | sub_permut_sym :
+      forall t t':array n A, sub_permut g d t t' -> sub_permut g d t' t
+  | sub_permut_trans :
+      forall t t' t'':array n A,
+        sub_permut g d t t' -> sub_permut g d t' t'' -> sub_permut g d t t''.
+
+Hint Resolve exchange_is_sub_permut sub_permut_refl sub_permut_sym
+  sub_permut_trans: v62 datatypes.
 
 (* To express that some parts of arrays are equal we introduce the
  * property "array_id" which says that a segment is the same on two
  * arrays.
  *)
 
-Definition array_id := [n:Z][A:Set][t,t':(array n A)][g,d:Z]
-  (i:Z) `g <= i <= d` -> #t[i] = #t'[i].
+Definition array_id (n:Z) (A:Set) (t t':array n A) 
+  (g d:Z) := forall i:Z, (g <= i <= d)%Z -> #t [i] = #t' [i].
 
 (* array_id is an equivalence relation *)
 
-Lemma array_id_refl : 
-  (n:Z)(A:Set)(t:(array n A))(g,d:Z)
-  (array_id t t g d).
+Lemma array_id_refl :
+ forall (n:Z) (A:Set) (t:array n A) (g d:Z), array_id t t g d.
 Proof.
-Unfold array_id.
-Auto with datatypes.
-Save.
+unfold array_id in |- *.
+auto with datatypes.
+Qed.
 
-Hints Resolve array_id_refl : v62 datatypes.
+Hint Resolve array_id_refl: v62 datatypes.
 
 Lemma array_id_sym :
-  (n:Z)(A:Set)(t,t':(array n A))(g,d:Z)
-  (array_id t t' g d)
-  -> (array_id t' t g d).
+ forall (n:Z) (A:Set) (t t':array n A) (g d:Z),
+   array_id t t' g d -> array_id t' t g d.
 Proof.
-Unfold array_id. Intros.
-Symmetry; Auto with datatypes.
-Save.
+unfold array_id in |- *. intros.
+symmetry  in |- *; auto with datatypes.
+Qed.
 
-Hints Resolve  array_id_sym : v62 datatypes.
+Hint Resolve array_id_sym: v62 datatypes.
 
 Lemma array_id_trans :
-  (n:Z)(A:Set)(t,t',t'':(array n A))(g,d:Z)
-  (array_id t t' g d)
-  -> (array_id t' t'' g d)
-    -> (array_id t t'' g d).
+ forall (n:Z) (A:Set) (t t' t'':array n A) (g d:Z),
+   array_id t t' g d -> array_id t' t'' g d -> array_id t t'' g d.
 Proof.
-Unfold array_id. Intros.
-Apply trans_eq with y:=#t'[i]; Auto with datatypes.
-Save.
+unfold array_id in |- *. intros.
+apply trans_eq with (y := #t' [i]); auto with datatypes.
+Qed.
 
-Hints Resolve array_id_trans: v62 datatypes.
+Hint Resolve array_id_trans: v62 datatypes.
 
 (* Outside the segment [g,d] the elements are equal *)
 
 Lemma sub_permut_id :
-  (n:Z)(A:Set)(t,t':(array n A))(g,d:Z)
-  (sub_permut g d t t') ->
-  (array_id t t' `0` `g-1`) /\ (array_id t t' `d+1` `n-1`).
+ forall (n:Z) (A:Set) (t t':array n A) (g d:Z),
+   sub_permut g d t t' ->
+   array_id t t' 0 (g - 1) /\ array_id t t' (d + 1) (n - 1).
 Proof.
-Intros n A t t' g d. Induction 1; Intros.
-Elim H2; Intros.
-Unfold array_id; Split; Intros.
-Apply H7; Omega.
-Apply H7; Omega.
-Auto with datatypes.
-Decompose [and] H1; Auto with datatypes.
-Decompose [and] H1; Decompose [and] H3; EAuto with datatypes.
-Save.
-
-Hints Resolve sub_permut_id.
+intros n A t t' g d. simple induction 1; intros.
+elim H2; intros.
+unfold array_id in |- *; split; intros.
+apply H7; omega.
+apply H7; omega.
+auto with datatypes.
+decompose [and] H1; auto with datatypes.
+decompose [and] H1; decompose [and] H3; eauto with datatypes.
+Qed.
+
+Hint Resolve sub_permut_id.
 
 Lemma sub_permut_eq :
-  (n:Z)(A:Set)(t,t':(array n A))(g,d:Z)
-  (sub_permut g d t t') ->
-  (i:Z) (`0<=i<g` \/ `d<i<n`) -> #t[i]=#t'[i].
+ forall (n:Z) (A:Set) (t t':array n A) (g d:Z),
+   sub_permut g d t t' ->
+   forall i:Z, (0 <= i < g)%Z \/ (d < i < n)%Z -> #t [i] = #t' [i].
 Proof.
-Intros n A t t' g d Htt' i Hi.
-Elim (sub_permut_id Htt'). Unfold array_id. 
-Intros.
-Elim Hi; [ Intro; Apply H; Omega | Intro; Apply H0; Omega ].
-Save.
+intros n A t t' g d Htt' i Hi.
+elim (sub_permut_id Htt'). unfold array_id in |- *. 
+intros.
+elim Hi; [ intro; apply H; omega | intro; apply H0; omega ].
+Qed.
 
 (* sub_permut is a particular case of permutation *)
 
 Lemma sub_permut_is_permut :
-  (n:Z)(A:Set)(t,t':(array n A))(g,d:Z)
-  (sub_permut g d t t') ->
-  (permut t t').
+ forall (n:Z) (A:Set) (t t':array n A) (g d:Z),
+   sub_permut g d t t' -> permut t t'.
 Proof.
-Intros n A t t' g d. Induction 1; Intros; EAuto with datatypes.
-Save.
+intros n A t t' g d. simple induction 1; intros; eauto with datatypes.
+Qed.
 
-Hints Resolve sub_permut_is_permut.
+Hint Resolve sub_permut_is_permut.
 
 (* If we have a sub-permutation on an empty segment, then we have a 
  * sub-permutation on any segment.
  *)
 
 Lemma sub_permut_void :
-  (N:Z)(A:Set)(t,t':(array N A))
-  (g,g',d,d':Z) `d < g`
-   -> (sub_permut g d t t') -> (sub_permut g' d' t t').
+ forall (N:Z) (A:Set) (t t':array N A) (g g' d d':Z),
+   (d < g)%Z -> sub_permut g d t t' -> sub_permut g' d' t t'.
 Proof.
-Intros N A t t' g g' d d' Hdg.
-(Induction 1; Intros).
-(Absurd `g <= d`; Omega).
-Auto with datatypes.
-Auto with datatypes.
-EAuto with datatypes.
-Save.
+intros N A t t' g g' d d' Hdg.
+simple induction 1; intros.
+absurd (g <= d)%Z; omega.
+auto with datatypes.
+auto with datatypes.
+eauto with datatypes.
+Qed.
 
 (* A sub-permutation on a segment may be extended to any segment that
  * contains the first one.
  *)
 
 Lemma sub_permut_extension :
-  (N:Z)(A:Set)(t,t':(array N A))
-  (g,g',d,d':Z) `g' <= g` -> `d <= d'`
-   -> (sub_permut g d t t') -> (sub_permut g' d' t t').
+ forall (N:Z) (A:Set) (t t':array N A) (g g' d d':Z),
+   (g' <= g)%Z -> (d <= d')%Z -> sub_permut g d t t' -> sub_permut g' d' t t'.
 Proof.
-Intros N A t t' g g' d d' Hgg' Hdd'.
-(Induction 1; Intros).
-Apply exchange_is_sub_permut with i:=i j:=j; [ Omega | Omega | Assumption ].
-Auto with datatypes.
-Auto with datatypes.
-EAuto with datatypes.
-Save.
+intros N A t t' g g' d d' Hgg' Hdd'.
+simple induction 1; intros.
+apply exchange_is_sub_permut with (i := i) (j := j);
+ [ omega | omega | assumption ].
+auto with datatypes.
+auto with datatypes.
+eauto with datatypes.
+Qed.
\ No newline at end of file