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, 100 insertions, 108 deletions

diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 2356c9cb5..3506b9bab 100755
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -23,196 +23,188 @@
    including Peano's axioms of arithmetic (in Coq, these are in fact provable)
    Case analysis on [nat] and induction on [nat * nat] are provided too *)
 
-Require Notations.
-Require Datatypes.
-Require Logic.
+Require Import Notations.
+Require Import Datatypes.
+Require Import Logic.
 
 Open Scope nat_scope.
 
-Definition eq_S := (f_equal nat nat S).
+Definition eq_S := f_equal S.
 
-Hint eq_S : v62 := Resolve (f_equal nat nat S).
-Hint eq_nat_unary : core := Resolve (f_equal nat).
+Hint Resolve (f_equal S): v62.
+Hint Resolve (f_equal (A:=nat)): core.
 
 (** The predecessor function *)
 
-Definition pred : nat->nat := [n:nat](Cases n of O => O | (S u) => u end).
-Hint eq_pred : v62 := Resolve (f_equal nat nat pred).
+Definition pred (n:nat) : nat := match n with
+                                 | O => 0
+                                 | S u => u
+                                 end.
+Hint Resolve (f_equal pred): v62.
 
-Theorem pred_Sn : (m:nat) m=(pred (S m)).
+Theorem pred_Sn : forall n:nat, n = pred (S n).
 Proof.
-  Auto.
+  auto.
 Qed.
 
-Theorem eq_add_S : (n,m:nat) (S n)=(S m) -> n=m.
+Theorem eq_add_S : forall n m:nat, S n = S m -> n = m.
 Proof.
-  Intros n m H ; Change (pred (S n))=(pred (S m)); Auto.
+  intros n m H; change (pred (S n) = pred (S m)) in |- *; auto.
 Qed.
 
-Hints Immediate eq_add_S : core v62.
+Hint Immediate eq_add_S: core v62.
 
 (** A consequence of the previous axioms *)
 
-Theorem not_eq_S : (n,m:nat) ~(n=m) -> ~((S n)=(S m)).
+Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m.
 Proof.
-  Red; Auto.
+  red in |- *; auto.
 Qed.
-Hints Resolve not_eq_S : core v62.
+Hint Resolve not_eq_S: core v62.
 
-Definition IsSucc : nat->Prop
-  := [n:nat]Cases n of O => False | (S p) => True end.
+Definition IsSucc (n:nat) : Prop :=
+  match n with
+  | O => False
+  | S p => True
+  end.
 
 
-Theorem O_S : (n:nat)~(O=(S n)).
+Theorem O_S : forall n:nat, 0 <> S n.
 Proof.
-  Red;Intros n H.
-  Change (IsSucc O).
-  Rewrite <- (sym_eq nat O (S n));[Exact I | Assumption].
+  red in |- *; intros n H.
+  change (IsSucc 0) in |- *.
+  rewrite <- (sym_eq (x:=0) (y:=(S n))); [ exact I | assumption ].
 Qed.
-Hints Resolve O_S : core v62.
+Hint Resolve O_S: core v62.
 
-Theorem n_Sn : (n:nat) ~(n=(S n)).
+Theorem n_Sn : forall n:nat, n <> S n.
 Proof.
-  NewInduction n ; Auto.
+  induction n; auto.
 Qed.
-Hints Resolve n_Sn : core v62.
+Hint Resolve n_Sn: core v62.
 
 (** Addition *)
 
-Fixpoint plus [n:nat] : nat -> nat := 
-   [m:nat]Cases n of 
-      O   => m 
-  | (S p) => (S (plus p m)) end.
-Hint eq_plus : v62 := Resolve (f_equal2 nat nat nat plus).
-Hint eq_nat_binary : core := Resolve (f_equal2 nat nat).
+Fixpoint plus (n m:nat) {struct n} : nat :=
+  match n with
+  | O => m
+  | S p => S (plus p m)
+  end.
+Hint Resolve (f_equal2 plus): v62.
+Hint Resolve (f_equal2 (A1:=nat) (A2:=nat)): core.
 
-V8Infix "+" plus : nat_scope.
+Infix "+" := plus : nat_scope.
 
-Lemma plus_n_O : (n:nat) n=(plus n O).
+Lemma plus_n_O : forall n:nat, n = n + 0.
 Proof.
-  NewInduction n ; Simpl ; Auto.
+  induction n; simpl in |- *; auto.
 Qed.
-Hints Resolve plus_n_O : core v62.
+Hint Resolve plus_n_O: core v62.
 
-Lemma plus_O_n : (n:nat) (plus O n)=n.
+Lemma plus_O_n : forall n:nat, 0 + n = n.
 Proof.
-  Auto.
+  auto.
 Qed.
 
-Lemma plus_n_Sm : (n,m:nat) (S (plus n m))=(plus n (S m)).
+Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m.
 Proof.
-  Intros n m; NewInduction n; Simpl; Auto.
+  intros n m; induction n; simpl in |- *; auto.
 Qed.
-Hints Resolve plus_n_Sm : core v62.
+Hint Resolve plus_n_Sm: core v62.
 
-Lemma plus_Sn_m : (n,m:nat)(plus (S n) m)=(S (plus n m)).
+Lemma plus_Sn_m : forall n m:nat, S n + m = S (n + m).
 Proof.
-  Auto.
+  auto.
 Qed.
 
 (** Multiplication *)
 
-Fixpoint  mult [n:nat] : nat -> nat := 
-   [m:nat]Cases n of O => O 
-               | (S p) => (plus m (mult p m)) end.
-Hint eq_mult : core v62 := Resolve (f_equal2 nat nat nat mult).
+Fixpoint mult (n m:nat) {struct n} : nat :=
+  match n with
+  | O => 0
+  | S p => m + mult p m
+  end.
+Hint Resolve (f_equal2 mult): core v62.
 
-V8Infix "*" mult : nat_scope.
+Infix "*" := mult : nat_scope.
 
-Lemma mult_n_O : (n:nat) O=(mult n O).
+Lemma mult_n_O : forall n:nat, 0 = n * 0.
 Proof.
-  NewInduction n; Simpl; Auto.
+  induction n; simpl in |- *; auto.
 Qed.
-Hints Resolve mult_n_O : core v62.
+Hint Resolve mult_n_O: core v62.
 
-Lemma mult_n_Sm : (n,m:nat) (plus (mult n m) n)=(mult n (S m)).
+Lemma mult_n_Sm : forall n m:nat, n * m + n = n * S m.
 Proof.
-  Intros; NewInduction n as [|p H]; Simpl; Auto.
-  NewDestruct H; Rewrite <- plus_n_Sm; Apply (f_equal nat nat S).
-  Pattern 1 3 m; Elim m; Simpl; Auto.
+  intros; induction n as [| p H]; simpl in |- *; auto.
+  destruct H; rewrite <- plus_n_Sm; apply (f_equal S).
+  pattern m at 1 3 in |- *; elim m; simpl in |- *; auto.
 Qed.
-Hints Resolve mult_n_Sm : core v62.
+Hint Resolve mult_n_Sm: core v62.
 
 (** Definition of subtraction on [nat] : [m-n] is [0] if [n>=m] *)
 
-Fixpoint minus [n:nat] : nat -> nat := 
-  [m:nat]Cases n m of
-            O    _     =>  O
-         | (S k) O     => (S k)
-         | (S k) (S l) => (minus k l)
-        end. 
+Fixpoint minus (n m:nat) {struct n} : nat :=
+  match n, m with
+  | O, _ => 0
+  | S k, O => S k
+  | S k, S l => minus k l
+  end. 
 
-V8Infix "-" minus : nat_scope.
+Infix "-" := minus : nat_scope.
 
 (** Definition of the usual orders, the basic properties of [le] and [lt] 
     can be found in files Le and Lt *)
 
 (** An inductive definition to define the order *)
 
-Inductive le [n:nat] : nat -> Prop
-    := le_n : (le n n)
-     | le_S : (m:nat)(le n m)->(le n (S m)).
+Inductive le (n:nat) : nat -> Prop :=
+  | le_n : le n n
+  | le_S : forall m:nat, le n m -> le n (S m).
 
-V8Infix "<=" le : nat_scope.
+Infix "<=" := le : nat_scope.
 
-Hint constr_le : core v62 := Constructors le.
+Hint Constructors le: core v62.
 (*i equivalent to : "Hints Resolve le_n le_S : core v62." i*)
 
-Definition lt := [n,m:nat](le (S n) m).
-Hints Unfold lt : core v62.
+Definition lt (n m:nat) := S n <= m.
+Hint Unfold lt: core v62.
 
-V8Infix "<" lt : nat_scope.
+Infix "<" := lt : nat_scope.
 
-Definition ge := [n,m:nat](le m n).
-Hints Unfold ge : core v62.
+Definition ge (n m:nat) := m <= n.
+Hint Unfold ge: core v62.
 
-V8Infix ">=" ge : nat_scope.
+Infix ">=" := ge : nat_scope.
 
-Definition gt := [n,m:nat](lt m n).
-Hints Unfold gt : core v62.
+Definition gt (n m:nat) := m < n.
+Hint Unfold gt: core v62.
 
-V8Infix ">" gt : nat_scope.
+Infix ">" := gt : nat_scope.
 
-V8Notation "x <= y <= z" := (le x y)/\(le y z) : nat_scope.
-V8Notation "x <= y < z"  := (le x y)/\(lt y z) : nat_scope.
-V8Notation "x < y < z"   := (lt x y)/\(lt y z) : nat_scope.
-V8Notation "x < y <= z"  := (lt x y)/\(le y z) : nat_scope.
+Notation "x <= y <= z" := (x <= y /\ y <= z) : nat_scope.
+Notation "x <= y < z" := (x <= y /\ y < z) : nat_scope.
+Notation "x < y < z" := (x < y /\ y < z) : nat_scope.
+Notation "x < y <= z" := (x < y /\ y <= z) : nat_scope.
 
 (** Pattern-Matching on natural numbers *)
 
-Theorem nat_case : (n:nat)(P:nat->Prop)(P O)->((m:nat)(P (S m)))->(P n).
+Theorem nat_case :
+ forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n.
 Proof.
-  NewInduction n ; Auto.
+  induction n; auto.
 Qed.
 
 (** Principle of double induction *)
 
-Theorem nat_double_ind : (R:nat->nat->Prop)
-     ((n:nat)(R O n)) -> ((n:nat)(R (S n) O))
-     -> ((n,m:nat)(R n m)->(R (S n) (S m)))
-     -> (n,m:nat)(R n m).
+Theorem nat_double_ind :
+ forall R:nat -> nat -> Prop,
+   (forall n:nat, R 0 n) ->
+   (forall n:nat, R (S n) 0) ->
+   (forall n m:nat, R n m -> R (S n) (S m)) -> forall n m:nat, R n m.
 Proof.
-  NewInduction n; Auto.
-  NewDestruct m; Auto.
+  induction n; auto.
+  destruct m as [| n0]; auto.
 Qed.
 
 (** Notations *)
-V7only[
-Syntax constr
-  level 0:
-    S [ (S $p) ] -> [$p:"nat_printer":9]
-  | O [ O ]      -> ["(0)"].
-].
-
-V7only [
-(* For parsing/printing based on scopes *)
-Module nat_scope.
-Infix 4 "+" plus : nat_scope.
-Infix 3 "*" mult : nat_scope.
-Infix 4 "-" minus : nat_scope.
-Infix NONA 5 "<=" le : nat_scope.
-Infix NONA 5 "<" lt : nat_scope.
-Infix NONA 5 ">=" ge : nat_scope.
-Infix NONA 5 ">" gt : nat_scope.
-End nat_scope.
-].