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, 78 insertions, 78 deletions

diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index fe53fce90..d9bc4d1b2 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -11,128 +11,128 @@
 (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
 
 Require Export Arith.
-Require BinPos.
-Require BinInt.
-Require Zcompare.
-Require Zorder.
-Require Decidable.
-Require Peano_dec.
+Require Import BinPos.
+Require Import BinInt.
+Require Import Zcompare.
+Require Import Zorder.
+Require Import Decidable.
+Require Import Peano_dec.
 Require Export Compare_dec.
 
 Open Local Scope Z_scope.
 
-Definition neq := [x,y:nat] ~(x=y).
+Definition neq (x y:nat) := x <> y.
 
 (**********************************************************************)
 (** Properties of the injection from nat into Z *)
 
-Theorem inj_S : (y:nat) (inject_nat (S y)) = (Zs (inject_nat y)).
+Theorem inj_S : forall n:nat, Z_of_nat (S n) = Zsucc (Z_of_nat n).
 Proof.
-Intro y; NewInduction y as [|n H]; [
-  Unfold Zs ; Simpl; Trivial with arith
-| Change (POS (add_un (anti_convert n)))=(Zs (inject_nat (S n)));
-  Rewrite add_un_Zs; Trivial with arith].
+intro y; induction y as [| n H];
+ [ unfold Zsucc in |- *; simpl in |- *; trivial with arith
+ | change (Zpos (Psucc (P_of_succ_nat n)) = Zsucc (Z_of_nat (S n))) in |- *;
+    rewrite Zpos_succ_morphism; trivial with arith ].
 Qed.
  
-Theorem inj_plus : 
-  (x,y:nat) (inject_nat (plus x y)) = (Zplus (inject_nat x) (inject_nat y)).
+Theorem inj_plus : forall n m:nat, Z_of_nat (n + m) = Z_of_nat n + Z_of_nat m.
 Proof.
-Intro x; NewInduction x as [|n H]; Intro y; NewDestruct y as [|m]; [
-  Simpl; Trivial with arith
-| Simpl; Trivial with arith
-| Simpl; Rewrite <- plus_n_O; Trivial with arith
-| Change (inject_nat (S (plus n (S m))))=
-                        (Zplus (inject_nat (S n)) (inject_nat (S m)));
-  Rewrite inj_S; Rewrite H; Do 2 Rewrite inj_S; Rewrite Zplus_S_n; Trivial with arith].
+intro x; induction x as [| n H]; intro y; destruct y as [| m];
+ [ simpl in |- *; trivial with arith
+ | simpl in |- *; trivial with arith
+ | simpl in |- *; rewrite <- plus_n_O; trivial with arith
+ | change (Z_of_nat (S (n + S m)) = Z_of_nat (S n) + Z_of_nat (S m)) in |- *;
+    rewrite inj_S; rewrite H; do 2 rewrite inj_S; rewrite Zplus_succ_l;
+    trivial with arith ].
 Qed.
  
-Theorem inj_mult : 
-  (x,y:nat) (inject_nat (mult x y)) = (Zmult (inject_nat x) (inject_nat y)).
+Theorem inj_mult : forall n m:nat, Z_of_nat (n * m) = Z_of_nat n * Z_of_nat m.
 Proof.
-Intro x; NewInduction x as [|n H]; [
-  Simpl; Trivial with arith
-| Intro y; Rewrite -> inj_S; Rewrite <- Zmult_Sm_n;
-    Rewrite <- H;Rewrite <- inj_plus; Simpl; Rewrite plus_sym; Trivial with arith].
+intro x; induction x as [| n H];
+ [ simpl in |- *; trivial with arith
+ | intro y; rewrite inj_S; rewrite <- Zmult_succ_l_reverse; rewrite <- H;
+    rewrite <- inj_plus; simpl in |- *; rewrite plus_comm; 
+    trivial with arith ].
 Qed.
 
-Theorem inj_neq:
-  (x,y:nat) (neq x y) -> (Zne (inject_nat x) (inject_nat y)).
+Theorem inj_neq : forall n m:nat, neq n m -> Zne (Z_of_nat n) (Z_of_nat m).
 Proof.
-Unfold neq Zne not ; Intros x y H1 H2; Apply H1; Generalize H2; 
-Case x; Case y; Intros; [
-  Auto with arith
-| Discriminate H0
-| Discriminate H0
-| Simpl in H0; Injection H0; Do 2 Rewrite <- bij1; Intros E; Rewrite E; Auto with arith].
+unfold neq, Zne, not in |- *; intros x y H1 H2; apply H1; generalize H2;
+ case x; case y; intros;
+ [ auto with arith
+ | discriminate H0
+ | discriminate H0
+ | simpl in H0; injection H0;
+    do 2 rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ; 
+    intros E; rewrite E; auto with arith ].
 Qed. 
 
-Theorem inj_le:
-  (x,y:nat) (le x y) -> (Zle (inject_nat x) (inject_nat y)).
+Theorem inj_le : forall n m:nat, (n <= m)%nat -> Z_of_nat n <= Z_of_nat m.
 Proof.
-Intros x y; Intros H; Elim H; [
-  Unfold Zle ; Elim (Zcompare_EGAL (inject_nat x) (inject_nat x));
-  Intros H1 H2; Rewrite H2; [ Discriminate | Trivial with arith]
-| Intros m H1 H2; Apply Zle_trans with (inject_nat m); 
-    [Assumption | Rewrite inj_S; Apply Zle_n_Sn]].
+intros x y; intros H; elim H;
+ [ unfold Zle in |- *; elim (Zcompare_Eq_iff_eq (Z_of_nat x) (Z_of_nat x));
+    intros H1 H2; rewrite H2; [ discriminate | trivial with arith ]
+ | intros m H1 H2; apply Zle_trans with (Z_of_nat m);
+    [ assumption | rewrite inj_S; apply Zle_succ ] ].
 Qed.
 
-Theorem inj_lt: (x,y:nat) (lt x y) -> (Zlt (inject_nat x) (inject_nat y)).
+Theorem inj_lt : forall n m:nat, (n < m)%nat -> Z_of_nat n < Z_of_nat m.
 Proof.
-Intros x y H; Apply Zgt_lt; Apply Zle_S_gt; Rewrite <- inj_S; Apply inj_le;
-Exact H.
+intros x y H; apply Zgt_lt; apply Zlt_succ_gt; rewrite <- inj_S; apply inj_le;
+ exact H.
 Qed.
 
-Theorem inj_gt: (x,y:nat) (gt x y) -> (Zgt (inject_nat x) (inject_nat y)).
+Theorem inj_gt : forall n m:nat, (n > m)%nat -> Z_of_nat n > Z_of_nat m.
 Proof.
-Intros x y H; Apply Zlt_gt; Apply inj_lt; Exact H.
+intros x y H; apply Zlt_gt; apply inj_lt; exact H.
 Qed.
 
-Theorem inj_ge: (x,y:nat) (ge x y) -> (Zge (inject_nat x) (inject_nat y)).
+Theorem inj_ge : forall n m:nat, (n >= m)%nat -> Z_of_nat n >= Z_of_nat m.
 Proof.
-Intros x y H; Apply Zle_ge; Apply inj_le; Apply H.
+intros x y H; apply Zle_ge; apply inj_le; apply H.
 Qed.
 
-Theorem inj_eq: (x,y:nat) x=y -> (inject_nat x) = (inject_nat y).
+Theorem inj_eq : forall n m:nat, n = m -> Z_of_nat n = Z_of_nat m.
 Proof.
-Intros x y H; Rewrite H; Trivial with arith.
+intros x y H; rewrite H; trivial with arith.
 Qed.
 
-Theorem intro_Z : 
-  (x:nat) (EX y:Z | (inject_nat x)=y /\ 
-      	  (Zle ZERO (Zplus (Zmult y (POS xH)) ZERO))).
+Theorem intro_Z :
+ forall n:nat,  exists y : Z | Z_of_nat n = y /\ 0 <= y * 1 + 0.
 Proof.
-Intros x; Exists (inject_nat x); Split; [
-  Trivial with arith
-| Rewrite Zmult_sym; Rewrite Zmult_one; Rewrite Zero_right; 
-  Unfold Zle ; Elim x; Intros;Simpl; Discriminate ].
+intros x; exists (Z_of_nat x); split;
+ [ trivial with arith
+ | rewrite Zmult_comm; rewrite Zmult_1_l; rewrite Zplus_0_r;
+    unfold Zle in |- *; elim x; intros; simpl in |- *; 
+    discriminate ].
 Qed.
 
 Theorem inj_minus1 :
-  (x,y:nat) (le y x) -> 
-    (inject_nat (minus x y)) = (Zminus (inject_nat x) (inject_nat y)).
+ forall n m:nat, (m <= n)%nat -> Z_of_nat (n - m) = Z_of_nat n - Z_of_nat m.
 Proof.
-Intros x y H; Apply (Zsimpl_plus_l (inject_nat y)); Unfold Zminus ;
-Rewrite Zplus_permute; Rewrite Zplus_inverse_r; Rewrite <- inj_plus;
-Rewrite <- (le_plus_minus y x H);Rewrite Zero_right; Trivial with arith.
+intros x y H; apply (Zplus_reg_l (Z_of_nat y)); unfold Zminus in |- *;
+ rewrite Zplus_permute; rewrite Zplus_opp_r; rewrite <- inj_plus;
+ rewrite <- (le_plus_minus y x H); rewrite Zplus_0_r; 
+ trivial with arith.
 Qed.
  
-Theorem inj_minus2: (x,y:nat) (gt y x) -> (inject_nat (minus x y)) = ZERO.
+Theorem inj_minus2 : forall n m:nat, (m > n)%nat -> Z_of_nat (n - m) = 0.
 Proof.
-Intros x y H; Rewrite inj_minus_aux; [ Trivial with arith | Apply gt_not_le; Assumption].
+intros x y H; rewrite not_le_minus_0;
+ [ trivial with arith | apply gt_not_le; assumption ].
 Qed.
 
-V7only [ (* From Zdivides *) ].
-Theorem POS_inject: (x : positive) (POS x) = (inject_nat (convert x)).
+Theorem Zpos_eq_Z_of_nat_o_nat_of_P :
+ forall p:positive, Zpos p = Z_of_nat (nat_of_P p).
 Proof.
-Intros x; Elim x; Simpl; Auto.
-Intros p H; Rewrite ZL6.
-Apply f_equal with f := POS.
-Apply convert_intro.
-Rewrite bij1; Unfold convert; Simpl.
-Rewrite ZL6; Auto.
-Intros p H; Unfold convert; Simpl.
-Rewrite ZL6; Simpl.
-Rewrite inj_plus; Repeat Rewrite <- H.
-Rewrite POS_xO; Simpl; Rewrite add_x_x; Reflexivity.
+intros x; elim x; simpl in |- *; auto.
+intros p H; rewrite ZL6.
+apply f_equal with (f := Zpos).
+apply nat_of_P_inj.
+rewrite nat_of_P_o_P_of_succ_nat_eq_succ; unfold nat_of_P in |- *;
+ simpl in |- *.
+rewrite ZL6; auto.
+intros p H; unfold nat_of_P in |- *; simpl in |- *.
+rewrite ZL6; simpl in |- *.
+rewrite inj_plus; repeat rewrite <- H.
+rewrite Zpos_xO; simpl in |- *; rewrite Pplus_diag; reflexivity.
 Qed.
-