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, 214 insertions, 219 deletions

diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index 88ad1851b..0017a464b 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -12,299 +12,294 @@
     and we prove the decidability and the exclusion of those predicates.
     The main results about parity are proved in the module Div2. *)
 
-V7only [Import nat_scope.].
 Open Local Scope nat_scope.
 
-Implicit Variables Type m,n:nat.
+Implicit Types m n : nat.
 
-Inductive even : nat->Prop :=
-    even_O : (even O)
-  | even_S : (n:nat)(odd n)->(even (S n))
-with odd : nat->Prop :=
-    odd_S : (n:nat)(even n)->(odd (S n)).
+Inductive even : nat -> Prop :=
+  | even_O : even 0
+  | even_S : forall n, odd n -> even (S n)
+with odd : nat -> Prop :=
+    odd_S : forall n, even n -> odd (S n).
 
-Hint constr_even : arith := Constructors even.
-Hint constr_odd : arith := Constructors odd.
+Hint Constructors even: arith.
+Hint Constructors odd: arith.
 
-Lemma even_or_odd : (n:nat) (even n)\/(odd n).
+Lemma even_or_odd : forall n, even n \/ odd n.
 Proof.
-NewInduction n.
-Auto with arith.
-Elim IHn; Auto with arith.
+induction n.
+auto with arith.
+elim IHn; auto with arith.
 Qed.
 
-Lemma even_odd_dec : (n:nat) { (even n) }+{ (odd n) }.
+Lemma even_odd_dec : forall n, {even n} + {odd n}.
 Proof.
-NewInduction n.
-Auto with arith.
-Elim IHn; Auto with arith.
+induction n.
+auto with arith.
+elim IHn; auto with arith.
 Qed.
 
-Lemma not_even_and_odd : (n:nat) (even n) -> (odd n) -> False.
+Lemma not_even_and_odd : forall n, even n -> odd n -> False.
 Proof.
-NewInduction n.
-Intros. Inversion H0.
-Intros. Inversion H. Inversion H0. Auto with arith.
+induction n.
+intros. inversion H0.
+intros. inversion H. inversion H0. auto with arith.
 Qed.
 
-Lemma even_plus_aux:
-  (n,m:nat)
-   (iff (odd (plus n m)) (odd n) /\ (even m) \/ (even n) /\ (odd m)) /\
-   (iff (even (plus n m)) (even n) /\ (even m) \/ (odd n) /\ (odd m)).
+Lemma even_plus_aux :
+ forall n m,
+   (odd (n + m) <-> odd n /\ even m \/ even n /\ odd m) /\
+   (even (n + m) <-> even n /\ even m \/ odd n /\ odd m).
 Proof.
-Intros n; Elim n; Simpl; Auto with arith.
-Intros m; Split; Auto.
-Split.
-Intros H; Right; Split; Auto with arith.
-Intros H'; Case H'; Auto with arith.
-Intros H'0; Elim H'0; Intros H'1 H'2; Inversion H'1.
-Intros H; Elim H; Auto.
-Split; Auto with arith.
-Intros H'; Elim H'; Auto with arith.
-Intros H; Elim H; Auto.
-Intros H'0; Elim H'0; Intros H'1 H'2; Inversion H'1.
-Intros n0 H' m; Elim (H' m); Intros H'1 H'2; Elim H'1; Intros E1 E2; Elim H'2;
- Intros E3 E4; Clear H'1 H'2.
-Split; Split.
-Intros H'0; Case E3.
-Inversion H'0; Auto.
-Intros H; Elim H; Intros H0 H1; Clear H; Auto with arith.
-Intros H; Elim H; Intros H0 H1; Clear H; Auto with arith.
-Intros H'0; Case H'0; Intros C0; Case C0; Intros C1 C2.
-Apply odd_S.
-Apply E4; Left; Split; Auto with arith.
-Inversion C1; Auto.
-Apply odd_S.
-Apply E4; Right; Split; Auto with arith.
-Inversion C1; Auto.
-Intros H'0.
-Case E1.
-Inversion H'0; Auto.
-Intros H; Elim H; Intros H0 H1; Clear H; Auto with arith.
-Intros H; Elim H; Intros H0 H1; Clear H; Auto with arith.
-Intros H'0; Case H'0; Intros C0; Case C0; Intros C1 C2.
-Apply even_S.
-Apply E2; Left; Split; Auto with arith.
-Inversion C1; Auto.
-Apply even_S.
-Apply E2; Right; Split; Auto with arith.
-Inversion C1; Auto.
+intros n; elim n; simpl in |- *; auto with arith.
+intros m; split; auto.
+split.
+intros H; right; split; auto with arith.
+intros H'; case H'; auto with arith.
+intros H'0; elim H'0; intros H'1 H'2; inversion H'1.
+intros H; elim H; auto.
+split; auto with arith.
+intros H'; elim H'; auto with arith.
+intros H; elim H; auto.
+intros H'0; elim H'0; intros H'1 H'2; inversion H'1.
+intros n0 H' m; elim (H' m); intros H'1 H'2; elim H'1; intros E1 E2; elim H'2;
+ intros E3 E4; clear H'1 H'2.
+split; split.
+intros H'0; case E3.
+inversion H'0; auto.
+intros H; elim H; intros H0 H1; clear H; auto with arith.
+intros H; elim H; intros H0 H1; clear H; auto with arith.
+intros H'0; case H'0; intros C0; case C0; intros C1 C2.
+apply odd_S.
+apply E4; left; split; auto with arith.
+inversion C1; auto.
+apply odd_S.
+apply E4; right; split; auto with arith.
+inversion C1; auto.
+intros H'0.
+case E1.
+inversion H'0; auto.
+intros H; elim H; intros H0 H1; clear H; auto with arith.
+intros H; elim H; intros H0 H1; clear H; auto with arith.
+intros H'0; case H'0; intros C0; case C0; intros C1 C2.
+apply even_S.
+apply E2; left; split; auto with arith.
+inversion C1; auto.
+apply even_S.
+apply E2; right; split; auto with arith.
+inversion C1; auto.
 Qed.
  
-Lemma even_even_plus : (n,m:nat) (even n) -> (even m) -> (even (plus n m)).
+Lemma even_even_plus : forall n m, even n -> even m -> even (n + m).
 Proof.
-Intros n m; Case (even_plus_aux n m).
-Intros H H0; Case H0; Auto.
+intros n m; case (even_plus_aux n m).
+intros H H0; case H0; auto.
 Qed.
  
-Lemma odd_even_plus : (n,m:nat) (odd n) -> (odd m) -> (even (plus n m)).
+Lemma odd_even_plus : forall n m, odd n -> odd m -> even (n + m).
 Proof.
-Intros n m; Case (even_plus_aux n m).
-Intros H H0; Case H0; Auto.
+intros n m; case (even_plus_aux n m).
+intros H H0; case H0; auto.
 Qed.
  
-Lemma even_plus_even_inv_r :
-  (n,m:nat) (even (plus n m)) -> (even n) -> (even m).
+Lemma even_plus_even_inv_r : forall n m, even (n + m) -> even n -> even m.
 Proof.
-Intros n m H; Case (even_plus_aux n m).
-Intros H' H'0; Elim H'0.
-Intros H'1; Case H'1; Auto.
-Intros H0; Elim H0; Auto.
-Intros H0 H1 H2; Case (not_even_and_odd n); Auto.
-Case H0; Auto.
+intros n m H; case (even_plus_aux n m).
+intros H' H'0; elim H'0.
+intros H'1; case H'1; auto.
+intros H0; elim H0; auto.
+intros H0 H1 H2; case (not_even_and_odd n); auto.
+case H0; auto.
 Qed.
  
-Lemma even_plus_even_inv_l :
-  (n,m:nat) (even (plus n m)) -> (even m) -> (even n).
+Lemma even_plus_even_inv_l : forall n m, even (n + m) -> even m -> even n.
 Proof.
-Intros n m H; Case (even_plus_aux n m).
-Intros H' H'0; Elim H'0.
-Intros H'1; Case H'1; Auto.
-Intros H0; Elim H0; Auto.
-Intros H0 H1 H2; Case (not_even_and_odd m); Auto.
-Case H0; Auto.
+intros n m H; case (even_plus_aux n m).
+intros H' H'0; elim H'0.
+intros H'1; case H'1; auto.
+intros H0; elim H0; auto.
+intros H0 H1 H2; case (not_even_and_odd m); auto.
+case H0; auto.
 Qed.
  
-Lemma even_plus_odd_inv_r : (n,m:nat) (even (plus n m)) -> (odd n) -> (odd m).
+Lemma even_plus_odd_inv_r : forall n m, even (n + m) -> odd n -> odd m.
 Proof.
-Intros n m H; Case (even_plus_aux n m).
-Intros H' H'0; Elim H'0.
-Intros H'1; Case H'1; Auto.
-Intros H0 H1 H2; Case (not_even_and_odd n); Auto.
-Case H0; Auto.
-Intros H0; Case H0; Auto.
+intros n m H; case (even_plus_aux n m).
+intros H' H'0; elim H'0.
+intros H'1; case H'1; auto.
+intros H0 H1 H2; case (not_even_and_odd n); auto.
+case H0; auto.
+intros H0; case H0; auto.
 Qed.
  
-Lemma even_plus_odd_inv_l : (n,m:nat) (even (plus n m)) -> (odd m) -> (odd n).
+Lemma even_plus_odd_inv_l : forall n m, even (n + m) -> odd m -> odd n.
 Proof.
-Intros n m H; Case (even_plus_aux n m).
-Intros H' H'0; Elim H'0.
-Intros H'1; Case H'1; Auto.
-Intros H0 H1 H2; Case (not_even_and_odd m); Auto.
-Case H0; Auto.
-Intros H0; Case H0; Auto.
+intros n m H; case (even_plus_aux n m).
+intros H' H'0; elim H'0.
+intros H'1; case H'1; auto.
+intros H0 H1 H2; case (not_even_and_odd m); auto.
+case H0; auto.
+intros H0; case H0; auto.
 Qed.
-Hints Resolve even_even_plus odd_even_plus :arith.
+Hint Resolve even_even_plus odd_even_plus: arith.
  
-Lemma odd_plus_l : (n,m:nat) (odd n) -> (even m) -> (odd (plus n m)).
+Lemma odd_plus_l : forall n m, odd n -> even m -> odd (n + m).
 Proof.
-Intros n m; Case (even_plus_aux n m).
-Intros H; Case H; Auto.
+intros n m; case (even_plus_aux n m).
+intros H; case H; auto.
 Qed.
  
-Lemma odd_plus_r : (n,m:nat) (even n) -> (odd m) -> (odd (plus n m)).
+Lemma odd_plus_r : forall n m, even n -> odd m -> odd (n + m).
 Proof.
-Intros n m; Case (even_plus_aux n m).
-Intros H; Case H; Auto.
+intros n m; case (even_plus_aux n m).
+intros H; case H; auto.
 Qed.
  
-Lemma odd_plus_even_inv_l : (n,m:nat) (odd (plus n m)) -> (odd m) -> (even n).
+Lemma odd_plus_even_inv_l : forall n m, odd (n + m) -> odd m -> even n.
 Proof.
-Intros n m H; Case (even_plus_aux n m).
-Intros H' H'0; Elim H'.
-Intros H'1; Case H'1; Auto.
-Intros H0 H1 H2; Case (not_even_and_odd m); Auto.
-Case H0; Auto.
-Intros H0; Case H0; Auto.
+intros n m H; case (even_plus_aux n m).
+intros H' H'0; elim H'.
+intros H'1; case H'1; auto.
+intros H0 H1 H2; case (not_even_and_odd m); auto.
+case H0; auto.
+intros H0; case H0; auto.
 Qed.
  
-Lemma odd_plus_even_inv_r : (n,m:nat) (odd (plus n m)) -> (odd n) -> (even m).
+Lemma odd_plus_even_inv_r : forall n m, odd (n + m) -> odd n -> even m.
 Proof.
-Intros n m H; Case (even_plus_aux n m).
-Intros H' H'0; Elim H'.
-Intros H'1; Case H'1; Auto.
-Intros H0; Case H0; Auto.
-Intros H0 H1 H2; Case (not_even_and_odd n); Auto.
-Case H0; Auto.
+intros n m H; case (even_plus_aux n m).
+intros H' H'0; elim H'.
+intros H'1; case H'1; auto.
+intros H0; case H0; auto.
+intros H0 H1 H2; case (not_even_and_odd n); auto.
+case H0; auto.
 Qed.
  
-Lemma odd_plus_odd_inv_l : (n,m:nat) (odd (plus n m)) -> (even m) -> (odd n).
+Lemma odd_plus_odd_inv_l : forall n m, odd (n + m) -> even m -> odd n.
 Proof.
-Intros n m H; Case (even_plus_aux n m).
-Intros H' H'0; Elim H'.
-Intros H'1; Case H'1; Auto.
-Intros H0; Case H0; Auto.
-Intros H0 H1 H2; Case (not_even_and_odd m); Auto.
-Case H0; Auto.
+intros n m H; case (even_plus_aux n m).
+intros H' H'0; elim H'.
+intros H'1; case H'1; auto.
+intros H0; case H0; auto.
+intros H0 H1 H2; case (not_even_and_odd m); auto.
+case H0; auto.
 Qed.
  
-Lemma odd_plus_odd_inv_r : (n,m:nat) (odd (plus n m)) -> (even n) -> (odd m).
+Lemma odd_plus_odd_inv_r : forall n m, odd (n + m) -> even n -> odd m.
 Proof.
-Intros n m H; Case (even_plus_aux n m).
-Intros H' H'0; Elim H'.
-Intros H'1; Case H'1; Auto.
-Intros H0 H1 H2; Case (not_even_and_odd n); Auto.
-Case H0; Auto.
-Intros H0; Case H0; Auto.
+intros n m H; case (even_plus_aux n m).
+intros H' H'0; elim H'.
+intros H'1; case H'1; auto.
+intros H0 H1 H2; case (not_even_and_odd n); auto.
+case H0; auto.
+intros H0; case H0; auto.
 Qed.
-Hints Resolve odd_plus_l odd_plus_r :arith.
+Hint Resolve odd_plus_l odd_plus_r: arith.
  
 Lemma even_mult_aux :
-  (n,m:nat)
-   (iff (odd (mult n m)) (odd n) /\ (odd m)) /\
-   (iff (even (mult n m)) (even n) \/ (even m)).
+ forall n m,
+   (odd (n * m) <-> odd n /\ odd m) /\ (even (n * m) <-> even n \/ even m).
 Proof.
-Intros n; Elim n; Simpl; Auto with arith.
-Intros m; Split; Split; Auto with arith.
-Intros H'; Inversion H'.
-Intros H'; Elim H'; Auto.
-Intros n0 H' m; Split; Split; Auto with arith.
-Intros H'0.
-Elim (even_plus_aux m (mult n0 m)); Intros H'3 H'4; Case H'3; Intros H'1 H'2;
- Case H'1; Auto.
-Intros H'5; Elim H'5; Intros H'6 H'7; Auto with arith.
-Split; Auto with arith.
-Case (H' m).
-Intros H'8 H'9; Case H'9.
-Intros H'10; Case H'10; Auto with arith.
-Intros H'11 H'12; Case (not_even_and_odd m); Auto with arith.
-Intros H'5; Elim H'5; Intros H'6 H'7; Case (not_even_and_odd (mult n0 m)); Auto.
-Case (H' m).
-Intros H'8 H'9; Case H'9; Auto.
-Intros H'0; Elim H'0; Intros H'1 H'2; Clear H'0.
-Elim (even_plus_aux m (mult n0 m)); Auto.
-Intros H'0 H'3.
-Elim H'0.
-Intros H'4 H'5; Apply H'5; Auto.
-Left; Split; Auto with arith.
-Case (H' m).
-Intros H'6 H'7; Elim H'7.
-Intros H'8 H'9; Apply H'9.
-Left.
-Inversion H'1; Auto.
-Intros H'0.
-Elim (even_plus_aux m (mult n0 m)); Intros H'3 H'4; Case H'4.
-Intros H'1 H'2.
-Elim H'1; Auto.
-Intros H; Case H; Auto.
-Intros H'5; Elim H'5; Intros H'6 H'7; Auto with arith.
-Left.
-Case (H' m).
-Intros H'8; Elim H'8.
-Intros H'9; Elim H'9; Auto with arith.
-Intros H'0; Elim H'0; Intros H'1.
-Case (even_or_odd m); Intros H'2.
-Apply even_even_plus; Auto.
-Case (H' m).
-Intros H H0; Case H0; Auto.
-Apply odd_even_plus; Auto.
-Inversion H'1; Case (H' m); Auto.
-Intros H1; Case H1; Auto.
-Apply even_even_plus; Auto.
-Case (H' m).
-Intros H H0; Case H0; Auto.
+intros n; elim n; simpl in |- *; auto with arith.
+intros m; split; split; auto with arith.
+intros H'; inversion H'.
+intros H'; elim H'; auto.
+intros n0 H' m; split; split; auto with arith.
+intros H'0.
+elim (even_plus_aux m (n0 * m)); intros H'3 H'4; case H'3; intros H'1 H'2;
+ case H'1; auto.
+intros H'5; elim H'5; intros H'6 H'7; auto with arith.
+split; auto with arith.
+case (H' m).
+intros H'8 H'9; case H'9.
+intros H'10; case H'10; auto with arith.
+intros H'11 H'12; case (not_even_and_odd m); auto with arith.
+intros H'5; elim H'5; intros H'6 H'7; case (not_even_and_odd (n0 * m)); auto.
+case (H' m).
+intros H'8 H'9; case H'9; auto.
+intros H'0; elim H'0; intros H'1 H'2; clear H'0.
+elim (even_plus_aux m (n0 * m)); auto.
+intros H'0 H'3.
+elim H'0.
+intros H'4 H'5; apply H'5; auto.
+left; split; auto with arith.
+case (H' m).
+intros H'6 H'7; elim H'7.
+intros H'8 H'9; apply H'9.
+left.
+inversion H'1; auto.
+intros H'0.
+elim (even_plus_aux m (n0 * m)); intros H'3 H'4; case H'4.
+intros H'1 H'2.
+elim H'1; auto.
+intros H; case H; auto.
+intros H'5; elim H'5; intros H'6 H'7; auto with arith.
+left.
+case (H' m).
+intros H'8; elim H'8.
+intros H'9; elim H'9; auto with arith.
+intros H'0; elim H'0; intros H'1.
+case (even_or_odd m); intros H'2.
+apply even_even_plus; auto.
+case (H' m).
+intros H H0; case H0; auto.
+apply odd_even_plus; auto.
+inversion H'1; case (H' m); auto.
+intros H1; case H1; auto.
+apply even_even_plus; auto.
+case (H' m).
+intros H H0; case H0; auto.
 Qed.
  
-Lemma even_mult_l : (n,m:nat) (even n) -> (even (mult n m)).
+Lemma even_mult_l : forall n m, even n -> even (n * m).
 Proof.
-Intros n m; Case (even_mult_aux n m); Auto.
-Intros H H0; Case H0; Auto.
+intros n m; case (even_mult_aux n m); auto.
+intros H H0; case H0; auto.
 Qed.
  
-Lemma even_mult_r: (n,m:nat) (even m) -> (even (mult n m)).
+Lemma even_mult_r : forall n m, even m -> even (n * m).
 Proof.
-Intros n m; Case (even_mult_aux n m); Auto.
-Intros H H0; Case H0; Auto.
+intros n m; case (even_mult_aux n m); auto.
+intros H H0; case H0; auto.
 Qed.
-Hints Resolve even_mult_l even_mult_r :arith.
+Hint Resolve even_mult_l even_mult_r: arith.
  
-Lemma even_mult_inv_r: (n,m:nat) (even (mult n m)) -> (odd n) -> (even m).
+Lemma even_mult_inv_r : forall n m, even (n * m) -> odd n -> even m.
 Proof.
-Intros n m H' H'0.
-Case (even_mult_aux n m).
-Intros H'1 H'2; Elim H'2.
-Intros H'3; Elim H'3; Auto.
-Intros H; Case (not_even_and_odd n); Auto.
+intros n m H' H'0.
+case (even_mult_aux n m).
+intros H'1 H'2; elim H'2.
+intros H'3; elim H'3; auto.
+intros H; case (not_even_and_odd n); auto.
 Qed.
  
-Lemma even_mult_inv_l : (n,m:nat) (even (mult n m)) -> (odd m) -> (even n).
+Lemma even_mult_inv_l : forall n m, even (n * m) -> odd m -> even n.
 Proof.
-Intros n m H' H'0.
-Case (even_mult_aux n m).
-Intros H'1 H'2; Elim H'2.
-Intros H'3; Elim H'3; Auto.
-Intros H; Case (not_even_and_odd m); Auto.
+intros n m H' H'0.
+case (even_mult_aux n m).
+intros H'1 H'2; elim H'2.
+intros H'3; elim H'3; auto.
+intros H; case (not_even_and_odd m); auto.
 Qed.
  
-Lemma odd_mult : (n,m:nat) (odd n) -> (odd m) -> (odd (mult n m)).
+Lemma odd_mult : forall n m, odd n -> odd m -> odd (n * m).
 Proof.
-Intros n m; Case (even_mult_aux n m); Intros H; Case H; Auto.
+intros n m; case (even_mult_aux n m); intros H; case H; auto.
 Qed.
-Hints Resolve even_mult_l even_mult_r odd_mult :arith.
+Hint Resolve even_mult_l even_mult_r odd_mult: arith.
  
-Lemma odd_mult_inv_l : (n,m:nat) (odd (mult n m)) -> (odd n).
+Lemma odd_mult_inv_l : forall n m, odd (n * m) -> odd n.
 Proof.
-Intros n m H'.
-Case (even_mult_aux n m).
-Intros H'1 H'2; Elim H'1.
-Intros H'3; Elim H'3; Auto.
+intros n m H'.
+case (even_mult_aux n m).
+intros H'1 H'2; elim H'1.
+intros H'3; elim H'3; auto.
 Qed.
  
-Lemma odd_mult_inv_r : (n,m:nat) (odd (mult n m)) -> (odd m).
+Lemma odd_mult_inv_r : forall n m, odd (n * m) -> odd m.
 Proof.
-Intros n m H'.
-Case (even_mult_aux n m).
-Intros H'1 H'2; Elim H'1.
-Intros H'3; Elim H'3; Auto.
+intros n m H'.
+case (even_mult_aux n m).
+intros H'1 H'2; elim H'1.
+intros H'3; elim H'3; auto.
 Qed.
-