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, 92 deletions

diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 9ab8fc820..911b0b386 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -8,153 +8,155 @@
 
 (*i $Id$ i*)
 
-Require Lt.
-Require Plus.
-Require Compare_dec.
-Require Even.
+Require Import Lt.
+Require Import Plus.
+Require Import Compare_dec.
+Require Import Even.
 
-V7only [Import nat_scope.].
 Open Local Scope nat_scope.
 
-Implicit Variables Type n:nat.
+Implicit Type n : nat.
 
 (** Here we define [n/2] and prove some of its properties *)
 
-Fixpoint div2 [n:nat] : nat :=
-  Cases n of
-    O => O
-  | (S O) => O
-  | (S (S n')) => (S (div2 n'))
+Fixpoint div2 n : nat :=
+  match n with
+  | O => 0
+  | S O => 0
+  | S (S n') => S (div2 n')
   end.
 
 (** Since [div2] is recursively defined on [0], [1] and [(S (S n))], it is
     useful to prove the corresponding induction principle *)
 
-Lemma ind_0_1_SS : (P:nat->Prop)
-  (P O) -> (P (S O)) -> ((n:nat)(P n)->(P (S (S n)))) -> (n:nat)(P n).
+Lemma ind_0_1_SS :
+ forall P:nat -> Prop,
+   P 0 -> P 1 -> (forall n, P n -> P (S (S n))) -> forall n, P n.
 Proof.
-Intros.
-Cut (n:nat)(P n)/\(P (S n)).
-Intros. Elim (H2 n). Auto with arith.
+intros.
+cut (forall n, P n /\ P (S n)).
+intros. elim (H2 n). auto with arith.
 
-NewInduction n0. Auto with arith.
-Intros. Elim IHn0; Auto with arith.
+induction n0. auto with arith.
+intros. elim IHn0; auto with arith.
 Qed.
 
 (** [0 <n  =>  n/2 < n] *)
 
-Lemma lt_div2 : (n:nat) (lt O n) -> (lt (div2 n) n).
+Lemma lt_div2 : forall n, 0 < n -> div2 n < n.
 Proof.
-Intro n. Pattern n. Apply ind_0_1_SS.
-Intro. Inversion H.
-Auto with arith.
-Intros. Simpl.
-Case (zerop n0).
-Intro. Rewrite e. Auto with arith.
-Auto with arith.
+intro n. pattern n in |- *. apply ind_0_1_SS.
+intro. inversion H.
+auto with arith.
+intros. simpl in |- *.
+case (zerop n0).
+intro. rewrite e. auto with arith.
+auto with arith.
 Qed.
 
-Hints Resolve lt_div2 : arith.
+Hint Resolve lt_div2: arith.
 
 (** Properties related to the parity *)
 
-Lemma even_odd_div2 : (n:nat) 
-  ((even n)<->(div2 n)=(div2 (S n))) /\ ((odd n)<->(S (div2 n))=(div2 (S n))).
+Lemma even_odd_div2 :
+ forall n,
+   (even n <-> div2 n = div2 (S n)) /\ (odd n <-> S (div2 n) = div2 (S n)).
 Proof.
-Intro n. Pattern n. Apply ind_0_1_SS.
+intro n. pattern n in |- *. apply ind_0_1_SS.
 (* n  = 0 *)
-Split. Split; Auto with arith. 
-Split. Intro H. Inversion H.
-Intro H.  Absurd (S (div2 O))=(div2 (S O)); Auto with arith.
+split. split; auto with arith. 
+split. intro H. inversion H.
+intro H.  absurd (S (div2 0) = div2 1); auto with arith.
 (* n = 1 *)
-Split. Split. Intro. Inversion H. Inversion H1.
-Intro H.  Absurd (div2 (S O))=(div2 (S (S O))).
-Simpl. Discriminate. Assumption.
-Split; Auto with arith.
+split. split. intro. inversion H. inversion H1.
+intro H.  absurd (div2 1 = div2 2).
+simpl in |- *. discriminate. assumption.
+split; auto with arith.
 (* n = (S (S n')) *)
-Intros. Decompose [and] H. Unfold iff in H0 H1.
-Decompose [and] H0. Decompose [and] H1. Clear H H0 H1.
-Split; Split; Auto with arith.
-Intro H. Inversion H. Inversion H1.
-Change (S (div2 n0))=(S (div2 (S n0))). Auto with arith.
-Intro H. Inversion H. Inversion H1.
-Change (S (S (div2 n0)))=(S (div2 (S n0))). Auto with arith.
+intros. decompose [and] H. unfold iff in H0, H1.
+decompose [and] H0. decompose [and] H1. clear H H0 H1.
+split; split; auto with arith.
+intro H. inversion H. inversion H1.
+change (S (div2 n0) = S (div2 (S n0))) in |- *. auto with arith.
+intro H. inversion H. inversion H1.
+change (S (S (div2 n0)) = S (div2 (S n0))) in |- *. auto with arith.
 Qed.
 
 (** Specializations *)
 
-Lemma even_div2 : (n:nat) (even n) -> (div2 n)=(div2 (S n)).
-Proof [n:nat](proj1 ? ? (proj1 ? ? (even_odd_div2 n))).
+Lemma even_div2 : forall n, even n -> div2 n = div2 (S n).
+Proof fun n => proj1 (proj1 (even_odd_div2 n)).
 
-Lemma div2_even : (n:nat) (div2 n)=(div2 (S n)) -> (even n).
-Proof [n:nat](proj2 ? ? (proj1 ? ? (even_odd_div2 n))).
+Lemma div2_even : forall n, div2 n = div2 (S n) -> even n.
+Proof fun n => proj2 (proj1 (even_odd_div2 n)).
 
-Lemma odd_div2 : (n:nat) (odd n) -> (S (div2 n))=(div2 (S n)).
-Proof [n:nat](proj1 ? ? (proj2 ? ? (even_odd_div2 n))).
+Lemma odd_div2 : forall n, odd n -> S (div2 n) = div2 (S n).
+Proof fun n => proj1 (proj2 (even_odd_div2 n)).
 
-Lemma div2_odd : (n:nat) (S (div2 n))=(div2 (S n)) -> (odd n).
-Proof [n:nat](proj2 ? ? (proj2 ? ? (even_odd_div2 n))).
+Lemma div2_odd : forall n, S (div2 n) = div2 (S n) -> odd n.
+Proof fun n => proj2 (proj2 (even_odd_div2 n)).
 
-Hints Resolve even_div2 div2_even odd_div2 div2_odd : arith.
+Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith.
 
 (** Properties related to the double ([2n]) *)
 
-Definition double := [n:nat](plus n n).
+Definition double n := n + n.
 
-Hints Unfold double : arith.
+Hint Unfold double: arith.
 
-Lemma double_S : (n:nat) (double (S n))=(S (S (double n))).
+Lemma double_S : forall n, double (S n) = S (S (double n)).
 Proof.
-Intro. Unfold double. Simpl. Auto with arith.
+intro. unfold double in |- *. simpl in |- *. auto with arith.
 Qed.
 
-Lemma double_plus : (m,n:nat) (double (plus m n))=(plus (double m) (double n)).
+Lemma double_plus : forall n (m:nat), double (n + m) = double n + double m.
 Proof.
-Intros m n. Unfold double.
-Do 2 Rewrite -> plus_assoc_r. Rewrite -> (plus_permute n).
-Reflexivity.
+intros m n. unfold double in |- *.
+do 2 rewrite plus_assoc_reverse. rewrite (plus_permute n).
+reflexivity.
 Qed.
 
-Hints Resolve double_S : arith.
+Hint Resolve double_S: arith.
 
-Lemma even_odd_double : (n:nat) 
-  ((even n)<->n=(double (div2 n))) /\ ((odd n)<->n=(S (double (div2 n)))).
+Lemma even_odd_double :
+ forall n,
+   (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))).
 Proof.
-Intro n. Pattern n. Apply ind_0_1_SS.
+intro n. pattern n in |- *. apply ind_0_1_SS.
 (* n = 0 *)
-Split; Split; Auto with arith.
-Intro H. Inversion H.
+split; split; auto with arith.
+intro H. inversion H.
 (* n = 1 *)
-Split; Split; Auto with arith.
-Intro H. Inversion H. Inversion H1.
+split; split; auto with arith.
+intro H. inversion H. inversion H1.
 (* n = (S (S n')) *)
-Intros. Decompose [and] H. Unfold iff in H0 H1.
-Decompose [and] H0. Decompose [and] H1. Clear H H0 H1.
-Split; Split.
-Intro H. Inversion H. Inversion H1.
-Simpl. Rewrite (double_S (div2 n0)). Auto with arith.
-Simpl. Rewrite (double_S (div2 n0)). Intro H. Injection H. Auto with arith.
-Intro H. Inversion H. Inversion H1.
-Simpl. Rewrite (double_S (div2 n0)). Auto with arith.
-Simpl. Rewrite (double_S (div2 n0)). Intro H. Injection H. Auto with arith.
+intros. decompose [and] H. unfold iff in H0, H1.
+decompose [and] H0. decompose [and] H1. clear H H0 H1.
+split; split.
+intro H. inversion H. inversion H1.
+simpl in |- *. rewrite (double_S (div2 n0)). auto with arith.
+simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith.
+intro H. inversion H. inversion H1.
+simpl in |- *. rewrite (double_S (div2 n0)). auto with arith.
+simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith.
 Qed.
 
 
 (** Specializations *)
 
-Lemma even_double : (n:nat) (even n) -> n=(double (div2 n)).
-Proof [n:nat](proj1 ? ? (proj1 ? ? (even_odd_double n))).
+Lemma even_double : forall n, even n -> n = double (div2 n).
+Proof fun n => proj1 (proj1 (even_odd_double n)).
 
-Lemma double_even : (n:nat) n=(double (div2 n)) -> (even n).
-Proof [n:nat](proj2 ? ? (proj1 ? ? (even_odd_double n))).
+Lemma double_even : forall n, n = double (div2 n) -> even n.
+Proof fun n => proj2 (proj1 (even_odd_double n)).
 
-Lemma odd_double : (n:nat) (odd n) -> n=(S (double (div2 n))).
-Proof [n:nat](proj1 ? ? (proj2 ? ? (even_odd_double n))).
+Lemma odd_double : forall n, odd n -> n = S (double (div2 n)).
+Proof fun n => proj1 (proj2 (even_odd_double n)).
 
-Lemma double_odd : (n:nat) n=(S (double (div2 n))) -> (odd n).
-Proof [n:nat](proj2 ? ? (proj2 ? ? (even_odd_double n))).
+Lemma double_odd : forall n, n = S (double (div2 n)) -> odd n.
+Proof fun n => proj2 (proj2 (even_odd_double n)).
 
-Hints Resolve even_double double_even odd_double double_odd : arith.
+Hint Resolve even_double double_even odd_double double_odd: arith.
 
 (** Application: 
     - if [n] is even then there is a [p] such that [n = 2p]
@@ -162,13 +164,12 @@ Hints Resolve even_double double_even odd_double double_odd : arith.
 
     (Immediate: it is [n/2]) *)
 
-Lemma even_2n : (n:nat) (even n) -> { p:nat | n=(double p) }.
+Lemma even_2n : forall n, even n -> {p : nat | n = double p}.
 Proof.
-Intros n H. Exists (div2 n). Auto with arith.
+intros n H. exists (div2 n). auto with arith.
 Qed.
 
-Lemma odd_S2n : (n:nat) (odd n) -> { p:nat | n=(S (double p)) }.
+Lemma odd_S2n : forall n, odd n -> {p : nat | n = S (double p)}.
 Proof.
-Intros n H. Exists (div2 n). Auto with arith.
+intros n H. exists (div2 n). auto with arith.
 Qed.
-