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, 71 insertions, 58 deletions

diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index ee7da4ba67..476ec4a547 100755
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -7,7 +7,6 @@
 (***********************************************************************)
 
 Set Implicit Arguments.
-V7only [Unset Implicit Arguments.].
 
 (*i $Id$ i*)
 
@@ -17,24 +16,24 @@ V7only [Unset Implicit Arguments.].
 
    from a well-founded ordering on a given set *)
 
-Require Notations.
-Require Logic.
-Require Datatypes.
+Require Import Notations.
+Require Import Logic.
+Require Import Datatypes.
 
 (** Well-founded induction principle on Prop *)
 
-Chapter Well_founded.
+Section Well_founded.
 
  Variable A : Set.
  Variable R : A -> A -> Prop.
 
  (** The accessibility predicate is defined to be non-informative *)
 
- Inductive  Acc : A -> Prop 
-    := Acc_intro : (x:A)((y:A)(R y x)->(Acc y))->(Acc x).
+ Inductive Acc : A -> Prop :=
+     Acc_intro : forall x:A, (forall y:A, R y x -> Acc y) -> Acc x.
 
- Lemma Acc_inv : (x:A)(Acc x) -> (y:A)(R y x) -> (Acc y).
-  NewDestruct 1; Trivial.
+ Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y.
+  destruct 1; trivial.
  Defined.
 
   (** the informative elimination :
@@ -42,50 +41,56 @@ Chapter Well_founded.
 
  Section AccRecType.
   Variable P : A -> Type.
-  Variable F : (x:A)((y:A)(R y x)->(Acc y))->((y:A)(R y x)->(P y))->(P x).
+  Variable
+    F :
+      forall x:A,
+        (forall y:A, R y x -> Acc y) -> (forall y:A, R y x -> P y) -> P x.
 
-  Fixpoint Acc_rect [x:A;a:(Acc x)] : (P x)
-     := (F x (Acc_inv x a) ([y:A][h:(R y x)](Acc_rect y (Acc_inv x a y h)))).
+  Fixpoint Acc_rect (x:A) (a:Acc x) {struct a} : P x :=
+    F (Acc_inv a) (fun (y:A) (h:R y x) => Acc_rect (x:=y) (Acc_inv a h)).
 
  End AccRecType.
 
- Definition Acc_rec [P:A->Set] := (Acc_rect P).
+ Definition Acc_rec (P:A -> Set) := Acc_rect P.
 
  (** A simplified version of Acc_rec(t) *)
 
  Section AccIter.
   Variable P : A -> Type. 
-  Variable F : (x:A)((y:A)(R y x)-> (P y))->(P x).
+  Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
 
-  Fixpoint Acc_iter [x:A;a:(Acc x)] : (P x)
-     := (F x ([y:A][h:(R y x)](Acc_iter y (Acc_inv x a y h)))).
+  Fixpoint Acc_iter (x:A) (a:Acc x) {struct a} : P x :=
+    F (fun (y:A) (h:R y x) => Acc_iter (x:=y) (Acc_inv a h)).
 
  End AccIter.
 
  (** A relation is well-founded if every element is accessible *)
 
- Definition well_founded := (a:A)(Acc a).
+ Definition well_founded := forall a:A, Acc a.
 
  (** well-founded induction on Set and Prop *)
 
  Hypothesis Rwf : well_founded.
 
- Theorem well_founded_induction_type : 
-        (P:A->Type)((x:A)((y:A)(R y x)->(P y))->(P x))->(a:A)(P a).
+ Theorem well_founded_induction_type :
+  forall P:A -> Type,
+    (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
  Proof.
-  Intros; Apply (Acc_iter P); Auto.
+  intros; apply (Acc_iter P); auto.
  Defined.
 
  Theorem well_founded_induction :
-        (P:A->Set)((x:A)((y:A)(R y x)->(P y))->(P x))->(a:A)(P a).
+  forall P:A -> Set,
+    (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
  Proof.
-  Exact [P:A->Set](well_founded_induction_type P).
+  exact (fun P:A -> Set => well_founded_induction_type P).
  Defined.
 
- Theorem well_founded_ind : 
-         (P:A->Prop)((x:A)((y:A)(R y x)->(P y))->(P x))->(a:A)(P a).
+ Theorem well_founded_ind :
+  forall P:A -> Prop,
+    (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
  Proof.
-  Exact [P:A->Prop](well_founded_induction_type P).
+  exact (fun P:A -> Prop => well_founded_induction_type P).
  Defined.
 
 (** Building fixpoints  *) 
@@ -93,40 +98,41 @@ Chapter Well_founded.
 Section FixPoint.
 
 Variable P : A -> Set.
-Variable F : (x:A)((y:A)(R y x)->(P y))->(P x).
+Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
 
-Fixpoint Fix_F [x:A;r:(Acc x)] : (P x) := 
-         (F x [y:A][p:(R y x)](Fix_F y (Acc_inv x r y p))).
+Fixpoint Fix_F (x:A) (r:Acc x) {struct r} : P x :=
+  F (fun (y:A) (p:R y x) => Fix_F (x:=y) (Acc_inv r p)).
 
-Definition fix := [x:A](Fix_F x (Rwf x)).
+Definition Fix (x:A) := Fix_F (Rwf x).
 
 (** Proof that [well_founded_induction] satisfies the fixpoint equation. 
     It requires an extra property of the functional *)
 
-Hypothesis F_ext : 
-  (x:A)(f,g:(y:A)(R y x)->(P y))
-  ((y:A)(p:(R y x))((f y p)=(g y p)))->(F x f)=(F x g).
+Hypothesis
+  F_ext :
+    forall (x:A) (f g:forall y:A, R y x -> P y),
+      (forall (y:A) (p:R y x), f y p = g y p) -> F f = F g.
 
 Scheme Acc_inv_dep := Induction for Acc Sort Prop.
 
-Lemma Fix_F_eq
-  : (x:A)(r:(Acc x))
-    (F x [y:A][p:(R y x)](Fix_F y (Acc_inv x r y p)))=(Fix_F x r).
-NewDestruct r using  Acc_inv_dep; Auto.
+Lemma Fix_F_eq :
+ forall (x:A) (r:Acc x),
+   F (fun (y:A) (p:R y x) => Fix_F (Acc_inv r p)) = Fix_F r.
+destruct r using Acc_inv_dep; auto.
 Qed.
 
-Lemma Fix_F_inv : (x:A)(r,s:(Acc x))(Fix_F x r)=(Fix_F x s).
-Intro x; NewInduction (Rwf x); Intros.
-Rewrite <- (Fix_F_eq x r); Rewrite <- (Fix_F_eq x s); Intros.
-Apply F_ext; Auto.
+Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F r = Fix_F s.
+intro x; induction (Rwf x); intros.
+rewrite <- (Fix_F_eq r); rewrite <- (Fix_F_eq s); intros.
+apply F_ext; auto.
 Qed.
 
 
-Lemma Fix_eq : (x:A)(fix x)=(F x [y:A][p:(R y x)](fix y)).
-Intro x; Unfold fix.
-Rewrite <- (Fix_F_eq x).
-Apply F_ext; Intros.
-Apply Fix_F_inv.
+Lemma Fix_eq : forall x:A, Fix x = F (fun (y:A) (p:R y x) => Fix y).
+intro x; unfold Fix in |- *.
+rewrite <- (Fix_F_eq (x:=x)).
+apply F_ext; intros.
+apply Fix_F_inv.
 Qed.
 
 End FixPoint.
@@ -135,24 +141,31 @@ End Well_founded.
 
 (** A recursor over pairs *)
 
-Chapter Well_founded_2.
+Section Well_founded_2.
 
-  Variable A,B : Set.
+  Variables A B : Set.
   Variable R : A * B -> A * B -> Prop.
 
   Variable P : A -> B -> Type. 
-  Variable F : (x:A)(x':B)((y:A)(y':B)(R (y,y') (x,x'))-> (P y y'))->(P x x').
-
-  Fixpoint Acc_iter_2 [x:A;x':B;a:(Acc ? R (x,x'))] : (P x x')
-     := (F x x' ([y:A][y':B][h:(R (y,y') (x,x'))](Acc_iter_2 y y' (Acc_inv ? ? (x,x') a (y,y') h)))).
-
-  Hypothesis Rwf : (well_founded ? R).
-
-  Theorem well_founded_induction_type_2 : 
-     ((x:A)(x':B)((y:A)(y':B)(R (y,y') (x,x'))->(P y y'))->(P x x'))->(a:A)(b:B)(P a b).
+  Variable
+    F :
+      forall (x:A) (x':B),
+        (forall (y:A) (y':B), R (y, y') (x, x') -> P y y') -> P x x'.
+
+  Fixpoint Acc_iter_2 (x:A) (x':B) (a:Acc R (x, x')) {struct a} : 
+   P x x' :=
+    F
+      (fun (y:A) (y':B) (h:R (y, y') (x, x')) =>
+         Acc_iter_2 (x:=y) (x':=y') (Acc_inv a (y, y') h)).
+
+  Hypothesis Rwf : well_founded R.
+
+  Theorem well_founded_induction_type_2 :
+   (forall (x:A) (x':B),
+      (forall (y:A) (y':B), R (y, y') (x, x') -> P y y') -> P x x') ->
+   forall (a:A) (b:B), P a b.
   Proof.
-   Intros; Apply Acc_iter_2; Auto.
+   intros; apply Acc_iter_2; auto.
   Defined.
 
 End Well_founded_2.
-