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, 89 insertions, 82 deletions

diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 9bbbe0e46..19c564eb9 100755
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -16,115 +16,123 @@ Section Streams.
 
 Variable A : Set.
 
-CoInductive Set Stream   := Cons : A->Stream->Stream.
+CoInductive Stream : Set :=
+    Cons : A -> Stream -> Stream.
 
 
-Definition hd  := 
-  [x:Stream] Cases x of (Cons a _) => a end.
+Definition hd (x:Stream) := match x with
+                            | Cons a _ => a
+                            end.
 
-Definition tl  := 
-  [x:Stream] Cases x of (Cons _ s) => s end.
+Definition tl (x:Stream) := match x with
+                            | Cons _ s => s
+                            end.
 
 
-Fixpoint Str_nth_tl [n:nat] : Stream->Stream := 
-  [s:Stream] Cases n of
-	          O    => s
-		|(S m) => (Str_nth_tl m (tl s))
-	    end.
+Fixpoint Str_nth_tl (n:nat) (s:Stream) {struct n} : Stream :=
+  match n with
+  | O => s
+  | S m => Str_nth_tl m (tl s)
+  end.
 
-Definition Str_nth : nat->Stream->A := [n:nat][s:Stream](hd (Str_nth_tl n s)).
+Definition Str_nth (n:nat) (s:Stream) : A := hd (Str_nth_tl n s).
 
 
-Lemma unfold_Stream :(x:Stream)x=(Cases x of (Cons a s) => (Cons a s) end). 
+Lemma unfold_Stream :
+ forall x:Stream, x = match x with
+                      | Cons a s => Cons a s
+                      end. 
 Proof.
-  Intro x.
-  Case x.
-  Trivial.
+  intro x.
+  case x.
+  trivial.
 Qed.
 
-Lemma tl_nth_tl : (n:nat)(s:Stream)(tl (Str_nth_tl n s))=(Str_nth_tl n (tl s)).
+Lemma tl_nth_tl :
+ forall (n:nat) (s:Stream), tl (Str_nth_tl n s) = Str_nth_tl n (tl s).
 Proof.
-  Induction n; Simpl; Auto.
+  simple induction n; simpl in |- *; auto.
 Qed.
-Hints Resolve tl_nth_tl : datatypes v62.
-
-Lemma Str_nth_tl_plus 
-: (n,m:nat)(s:Stream)(Str_nth_tl n (Str_nth_tl m s))=(Str_nth_tl (plus n m) s).
-Induction n; Simpl; Intros; Auto with datatypes.
-Rewrite <- H.
-Rewrite tl_nth_tl; Trivial with datatypes.
+Hint Resolve tl_nth_tl: datatypes v62.
+
+Lemma Str_nth_tl_plus :
+ forall (n m:nat) (s:Stream),
+   Str_nth_tl n (Str_nth_tl m s) = Str_nth_tl (n + m) s.
+simple induction n; simpl in |- *; intros; auto with datatypes.
+rewrite <- H.
+rewrite tl_nth_tl; trivial with datatypes.
 Qed.
 
-Lemma Str_nth_plus 
-  : (n,m:nat)(s:Stream)(Str_nth n (Str_nth_tl m s))=(Str_nth (plus n m) s).
-Intros; Unfold Str_nth; Rewrite Str_nth_tl_plus; Trivial with datatypes.
+Lemma Str_nth_plus :
+ forall (n m:nat) (s:Stream), Str_nth n (Str_nth_tl m s) = Str_nth (n + m) s.
+intros; unfold Str_nth in |- *; rewrite Str_nth_tl_plus;
+ trivial with datatypes.
 Qed.
 
 (** Extensional Equality between two streams  *)
 
-CoInductive EqSt  : Stream->Stream->Prop := 
-	    eqst : (s1,s2:Stream)
-		   ((hd s1)=(hd s2))->
-		   (EqSt (tl s1) (tl s2))
-                    ->(EqSt s1 s2).
+CoInductive EqSt : Stream -> Stream -> Prop :=
+    eqst :
+      forall s1 s2:Stream,
+        hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2.
 
 (** A coinduction principle *)
 
-Tactic Definition CoInduction proof := 
-  Cofix proof; Intros; Constructor;
-    [Clear proof | Try (Apply proof;Clear proof)].
+Ltac coinduction proof :=
+  cofix proof; intros; constructor;
+   [ clear proof | try (apply proof; clear proof) ].
 
 
 (** Extensional equality is an equivalence relation *)
 
-Theorem  EqSt_reflex : (s:Stream)(EqSt s s).
-CoInduction EqSt_reflex.
-Reflexivity.
+Theorem EqSt_reflex : forall s:Stream, EqSt s s.
+coinduction EqSt_reflex.
+reflexivity.
 Qed.
 
-Theorem sym_EqSt : 
- (s1:Stream)(s2:Stream)(EqSt s1 s2)->(EqSt s2 s1).
-(CoInduction Eq_sym).
-Case H;Intros;Symmetry;Assumption.
-Case H;Intros;Assumption.
+Theorem sym_EqSt : forall s1 s2:Stream, EqSt s1 s2 -> EqSt s2 s1.
+coinduction Eq_sym.
+case H; intros; symmetry  in |- *; assumption.
+case H; intros; assumption.
 Qed.
 
 
-Theorem trans_EqSt : 
- (s1,s2,s3:Stream)(EqSt s1 s2)->(EqSt s2 s3)->(EqSt s1 s3).
-(CoInduction Eq_trans).
-Transitivity (hd s2).
-Case H; Intros; Assumption.
-Case H0; Intros; Assumption.
-Apply (Eq_trans (tl s1) (tl s2) (tl s3)).
-Case H;  Trivial with datatypes.
-Case H0; Trivial with datatypes.
+Theorem trans_EqSt :
+ forall s1 s2 s3:Stream, EqSt s1 s2 -> EqSt s2 s3 -> EqSt s1 s3.
+coinduction Eq_trans.
+transitivity (hd s2).
+case H; intros; assumption.
+case H0; intros; assumption.
+apply (Eq_trans (tl s1) (tl s2) (tl s3)).
+case H; trivial with datatypes.
+case H0; trivial with datatypes.
 Qed.
 
 (** The definition given is equivalent to require the elements at each
     position to be equal *)
 
 Theorem eqst_ntheq :
-  (n:nat)(s1,s2:Stream)(EqSt s1 s2)->(Str_nth n s1)=(Str_nth n s2).
-Unfold Str_nth; Induction n.
-Intros s1 s2 H; Case H; Trivial with datatypes.
-Intros m hypind.
-Simpl.
-Intros s1 s2 H.
-Apply hypind.
-Case H; Trivial with datatypes.
+ forall (n:nat) (s1 s2:Stream), EqSt s1 s2 -> Str_nth n s1 = Str_nth n s2.
+unfold Str_nth in |- *; simple induction n.
+intros s1 s2 H; case H; trivial with datatypes.
+intros m hypind.
+simpl in |- *.
+intros s1 s2 H.
+apply hypind.
+case H; trivial with datatypes.
 Qed.
 
-Theorem ntheq_eqst : 
-  (s1,s2:Stream)((n:nat)(Str_nth n s1)=(Str_nth n s2))->(EqSt s1 s2).
-(CoInduction Equiv2).
-Apply (H O).
-Intros n; Apply (H (S n)).
+Theorem ntheq_eqst :
+ forall s1 s2:Stream,
+   (forall n:nat, Str_nth n s1 = Str_nth n s2) -> EqSt s1 s2.
+coinduction Equiv2.
+apply (H 0).
+intros n; apply (H (S n)).
 Qed.
 
 Section Stream_Properties.
 
-Variable P : Stream->Prop.
+Variable P : Stream -> Prop.
 
 (*i
 Inductive Exists : Stream -> Prop :=
@@ -132,21 +140,21 @@ Inductive Exists : Stream -> Prop :=
   | Further : forall x:Stream, ~ P x -> Exists (tl x) -> Exists x.
 i*)
 
-Inductive   Exists :  Stream -> Prop :=
-   Here    : (x:Stream)(P x) ->(Exists x) |
-   Further : (x:Stream)(Exists (tl x))->(Exists x).
+Inductive Exists : Stream -> Prop :=
+  | Here : forall x:Stream, P x -> Exists x
+  | Further : forall x:Stream, Exists (tl x) -> Exists x.
 
-CoInductive ForAll : Stream  -> Prop :=
-    forall : (x:Stream)(P x)->(ForAll (tl x))->(ForAll x).
+CoInductive ForAll : Stream -> Prop :=
+    HereAndFurther : forall x:Stream, P x -> ForAll (tl x) -> ForAll x.
 
 
 Section Co_Induction_ForAll.
-Variable   Inv        :  Stream -> Prop.
-Hypothesis InvThenP   : (x:Stream)(Inv x)->(P x).
-Hypothesis InvIsStable: (x:Stream)(Inv x)->(Inv (tl x)).
+Variable Inv : Stream -> Prop.
+Hypothesis InvThenP : forall x:Stream, Inv x -> P x.
+Hypothesis InvIsStable : forall x:Stream, Inv x -> Inv (tl x).
 
-Theorem ForAll_coind : (x:Stream)(Inv x)->(ForAll x).
-(CoInduction ForAll_coind);Auto.
+Theorem ForAll_coind : forall x:Stream, Inv x -> ForAll x.
+coinduction ForAll_coind; auto.
 Qed.
 End Co_Induction_ForAll.
 
@@ -155,16 +163,15 @@ End Stream_Properties.
 End Streams.
 
 Section Map.
-Variables A,B : Set.
-Variable  f   : A->B.
-CoFixpoint map : (Stream A)->(Stream B) :=
- [s:(Stream A)](Cons (f (hd s)) (map (tl s))).
+Variables A B : Set.
+Variable f : A -> B.
+CoFixpoint map (s:Stream A) : Stream B := Cons (f (hd s)) (map (tl s)).
 End Map.
 
 Section Constant_Stream.
 Variable A : Set.
 Variable a : A.
-CoFixpoint const : (Stream A) := (Cons a const).
+CoFixpoint const  : Stream A := Cons a const.
 End Constant_Stream.
 
-Unset Implicit Arguments.
+Unset Implicit Arguments.
\ No newline at end of file