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

diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index 8d27f81d2..01e8d4870 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -8,39 +8,38 @@
 
 (*i $Id$ i*)
 
-Require ZArithRing.
-Require ZArith_base.
-Require Omega.
-Require Wf_nat.
-V7only [Import Z_scope.].
+Require Import ZArithRing.
+Require Import ZArith_base.
+Require Import Omega.
+Require Import Wf_nat.
 Open Local Scope Z_scope.
 
-V7only [Set Implicit Arguments.].
 
 (**********************************************************************)
 (** About parity *)
 
-Lemma two_or_two_plus_one : (x:Z) { y:Z | `x = 2*y`}+{ y:Z | `x = 2*y+1`}. 
+Lemma two_or_two_plus_one :
+ forall n:Z, {y : Z | n = 2 * y} + {y : Z | n = 2 * y + 1}. 
 Proof.
-Intro x; NewDestruct x.
-Left ; Split with ZERO; Reflexivity.
+intro x; destruct x.
+left; split with 0; reflexivity.
 
-NewDestruct p.
-Right ; Split with (POS p); Reflexivity.
+destruct p.
+right; split with (Zpos p); reflexivity.
 
-Left ; Split with (POS p); Reflexivity.
+left; split with (Zpos p); reflexivity.
 
-Right ; Split with ZERO; Reflexivity.
+right; split with 0; reflexivity.
 
-NewDestruct p.
-Right ; Split with (NEG (add xH p)).
-Rewrite NEG_xI.
-Rewrite NEG_add.
-Omega.
+destruct p.
+right; split with (Zneg (1 + p)).
+rewrite BinInt.Zneg_xI.
+rewrite BinInt.Zneg_plus_distr.
+omega.
 
-Left ; Split with (NEG p); Reflexivity.
+left; split with (Zneg p); reflexivity.
 
-Right ; Split with `-1`; Reflexivity.
+right; split with (-1); reflexivity.
 Qed.
 
 (**********************************************************************)
@@ -49,164 +48,165 @@ Qed.
     Easy to compute: replace all "1" of the binary representation by
     "0", except the first "1" (or the first one :-) *)
 
-Fixpoint floor_pos [a : positive] : positive :=
-  Cases a of
-  | xH => xH
-  | (xO a') => (xO (floor_pos a'))
-  | (xI b') => (xO (floor_pos b'))
+Fixpoint floor_pos (a:positive) : positive :=
+  match a with
+  | xH => 1%positive
+  | xO a' => xO (floor_pos a')
+  | xI b' => xO (floor_pos b')
   end.
 
-Definition floor := [a:positive](POS (floor_pos a)).
+Definition floor (a:positive) := Zpos (floor_pos a).
 
-Lemma floor_gt0 : (x:positive) `(floor x) > 0`.
+Lemma floor_gt0 : forall p:positive, floor p > 0.
 Proof.
-Intro.
-Compute.
-Trivial.
+intro.
+compute in |- *.
+trivial.
 Qed.
 
-Lemma floor_ok : (a:positive) 
-  `(floor a) <=  (POS a) < 2*(floor a)`. 
+Lemma floor_ok : forall p:positive, floor p <= Zpos p < 2 * floor p. 
 Proof.
-Unfold floor.
-Intro a; NewInduction a as [p|p|].
-
-Simpl.
-Repeat Rewrite POS_xI.
-Rewrite (POS_xO (xO (floor_pos p))). 
-Rewrite (POS_xO (floor_pos p)).
-Omega.
-
-Simpl.
-Repeat Rewrite POS_xI.
-Rewrite (POS_xO (xO (floor_pos p))).
-Rewrite (POS_xO (floor_pos p)).
-Rewrite (POS_xO p).
-Omega.
-
-Simpl; Omega.
+unfold floor in |- *.
+intro a; induction a as [p| p| ].
+
+simpl in |- *.
+repeat rewrite BinInt.Zpos_xI.
+rewrite (BinInt.Zpos_xO (xO (floor_pos p))). 
+rewrite (BinInt.Zpos_xO (floor_pos p)).
+omega.
+
+simpl in |- *.
+repeat rewrite BinInt.Zpos_xI.
+rewrite (BinInt.Zpos_xO (xO (floor_pos p))).
+rewrite (BinInt.Zpos_xO (floor_pos p)).
+rewrite (BinInt.Zpos_xO p).
+omega.
+
+simpl in |- *; omega.
 Qed.
 
 (**********************************************************************)
 (** Two more induction principles over [Z]. *)
 
-Theorem Z_lt_abs_rec : (P: Z -> Set)
-  ((n: Z) ((m: Z) `|m|<|n|` -> (P m)) -> (P n)) -> (p: Z) (P p).
+Theorem Z_lt_abs_rec :
+ forall P:Z -> Set,
+   (forall n:Z, (forall m:Z, Zabs m < Zabs n -> P m) -> P n) ->
+   forall n:Z, P n.
 Proof.
-Intros P HP p.
-LetTac Q:=[z]`0<=z`->(P z)*(P `-z`).
-Cut (Q `|p|`);[Intros|Apply (Z_lt_rec Q);Auto with zarith].
-Elim (Zabs_dec p);Intro eq;Rewrite eq;Elim H;Auto with zarith.
-Unfold Q;Clear Q;Intros.
-Apply pair;Apply HP.
-Rewrite Zabs_eq;Auto;Intros.
-Elim (H `|m|`);Intros;Auto with zarith.
-Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial.
-Rewrite Zabs_non_eq;Auto with zarith.
-Rewrite Zopp_Zopp;Intros.
-Elim (H `|m|`);Intros;Auto with zarith.
-Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial.
+intros P HP p.
+set (Q := fun z => 0 <= z -> P z * P (- z)) in *.
+cut (Q (Zabs p)); [ intros | apply (Z_lt_rec Q); auto with zarith ].
+elim (Zabs_dec p); intro eq; rewrite eq; elim H; auto with zarith.
+unfold Q in |- *; clear Q; intros.
+apply pair; apply HP.
+rewrite Zabs_eq; auto; intros.
+elim (H (Zabs m)); intros; auto with zarith.
+elim (Zabs_dec m); intro eq; rewrite eq; trivial.
+rewrite Zabs_non_eq; auto with zarith.
+rewrite Zopp_involutive; intros.
+elim (H (Zabs m)); intros; auto with zarith.
+elim (Zabs_dec m); intro eq; rewrite eq; trivial.
 Qed.
 
-Theorem Z_lt_abs_induction : (P: Z -> Prop)
-  ((n: Z) ((m: Z) `|m|<|n|` -> (P m)) -> (P n)) -> (p: Z) (P p).
+Theorem Z_lt_abs_induction :
+ forall P:Z -> Prop,
+   (forall n:Z, (forall m:Z, Zabs m < Zabs n -> P m) -> P n) ->
+   forall n:Z, P n.
 Proof.
-Intros P HP p.
-LetTac Q:=[z]`0<=z`->(P z) /\ (P `-z`).
-Cut (Q `|p|`);[Intros|Apply (Z_lt_induction Q);Auto with zarith].
-Elim (Zabs_dec p);Intro eq;Rewrite eq;Elim H;Auto with zarith.
-Unfold Q;Clear Q;Intros.
-Split;Apply HP.
-Rewrite Zabs_eq;Auto;Intros.
-Elim (H `|m|`);Intros;Auto with zarith.
-Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial.
-Rewrite Zabs_non_eq;Auto with zarith.
-Rewrite Zopp_Zopp;Intros.
-Elim (H `|m|`);Intros;Auto with zarith.
-Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial.
+intros P HP p.
+set (Q := fun z => 0 <= z -> P z /\ P (- z)) in *.
+cut (Q (Zabs p)); [ intros | apply (Z_lt_induction Q); auto with zarith ].
+elim (Zabs_dec p); intro eq; rewrite eq; elim H; auto with zarith.
+unfold Q in |- *; clear Q; intros.
+split; apply HP.
+rewrite Zabs_eq; auto; intros.
+elim (H (Zabs m)); intros; auto with zarith.
+elim (Zabs_dec m); intro eq; rewrite eq; trivial.
+rewrite Zabs_non_eq; auto with zarith.
+rewrite Zopp_involutive; intros.
+elim (H (Zabs m)); intros; auto with zarith.
+elim (Zabs_dec m); intro eq; rewrite eq; trivial.
 Qed.
-V7only [Unset Implicit Arguments.].
 
 (** To do case analysis over the sign of [z] *) 
 
-Lemma Zcase_sign : (x:Z)(P:Prop)
- (`x=0` -> P) ->
- (`x>0` -> P) ->
- (`x<0` -> P) -> P.
+Lemma Zcase_sign :
+ forall (n:Z) (P:Prop), (n = 0 -> P) -> (n > 0 -> P) -> (n < 0 -> P) -> P.
 Proof.
-Intros x P Hzero Hpos Hneg.
-Induction x.
-Apply Hzero; Trivial.
-Apply Hpos; Apply POS_gt_ZERO.
-Apply Hneg; Apply NEG_lt_ZERO.
-Save.
-
-Lemma sqr_pos : (x:Z)`x*x >= 0`.
+intros x P Hzero Hpos Hneg.
+induction  x as [| p| p].
+apply Hzero; trivial.
+apply Hpos; apply Zorder.Zgt_pos_0.
+apply Hneg; apply Zorder.Zlt_neg_0.
+Qed.
+
+Lemma sqr_pos : forall n:Z, n * n >= 0.
 Proof.
-Intro x.
-Apply (Zcase_sign x `x*x >= 0`).
-Intros H; Rewrite H; Omega.
-Intros H; Replace `0` with `0*0`.
-Apply Zge_Zmult_pos_compat; Omega.
-Omega.
-Intros H; Replace `0` with `0*0`.
-Replace `x*x` with `(-x)*(-x)`.
-Apply Zge_Zmult_pos_compat; Omega.
-Ring.
-Omega.
-Save.
+intro x.
+apply (Zcase_sign x (x * x >= 0)).
+intros H; rewrite H; omega.
+intros H; replace 0 with (0 * 0).
+apply Zmult_ge_compat; omega.
+omega.
+intros H; replace 0 with (0 * 0).
+replace (x * x) with (- x * - x).
+apply Zmult_ge_compat; omega.
+ring.
+omega.
+Qed.
 
 (**********************************************************************)
 (** A list length in Z, tail recursive.  *)
 
-Require PolyList.
+Require Import List.
 
-Fixpoint Zlength_aux [acc: Z; A:Set; l:(list A)] : Z := Cases l of 
-    nil => acc
-  | (cons _ l) => (Zlength_aux (Zs acc) A l)
-end. 
+Fixpoint Zlength_aux (acc:Z) (A:Set) (l:list A) {struct l} : Z :=
+  match l with
+  | nil => acc
+  | _ :: l => Zlength_aux (Zsucc acc) A l
+  end. 
 
-Definition Zlength := (Zlength_aux 0).
-Implicits Zlength [1].
+Definition Zlength := Zlength_aux 0.
+Implicit Arguments Zlength [A].
 
 Section Zlength_properties.
 
-Variable A:Set.
+Variable A : Set.
 
-Implicit Variable Type l:(list A).
+Implicit Type l : list A.
 
-Lemma Zlength_correct : (l:(list A))(Zlength l)=(inject_nat (length l)).
+Lemma Zlength_correct : forall l, Zlength l = Z_of_nat (length l).
 Proof.
-Assert (l:(list A))(acc:Z)(Zlength_aux acc A l)=acc+(inject_nat (length l)). 
-Induction l.
-Simpl; Auto with zarith.
-Intros; Simpl (length (cons a l0)); Rewrite inj_S.
-Simpl; Rewrite H; Auto with zarith.
-Unfold Zlength; Intros; Rewrite H; Auto.
+assert (forall l (acc:Z), Zlength_aux acc A l = acc + Z_of_nat (length l)). 
+simple induction l.
+simpl in |- *; auto with zarith.
+intros; simpl (length (a :: l0)) in |- *; rewrite Znat.inj_S.
+simpl in |- *; rewrite H; auto with zarith.
+unfold Zlength in |- *; intros; rewrite H; auto.
 Qed.
 
-Lemma Zlength_nil : (Zlength 1!A (nil A))=0.
+Lemma Zlength_nil : Zlength (A:=A) nil = 0.
 Proof.
-Auto.
+auto.
 Qed.
 
-Lemma Zlength_cons : (x:A)(l:(list A))(Zlength (cons x l))=(Zs (Zlength l)).
+Lemma Zlength_cons : forall (x:A) l, Zlength (x :: l) = Zsucc (Zlength l).
 Proof.
-Intros; Do 2 Rewrite Zlength_correct.
-Simpl (length (cons x l)); Rewrite inj_S; Auto.
+intros; do 2 rewrite Zlength_correct.
+simpl (length (x :: l)) in |- *; rewrite Znat.inj_S; auto.
 Qed.
 
-Lemma Zlength_nil_inv : (l:(list A))(Zlength l)=0 -> l=(nil ?).
+Lemma Zlength_nil_inv : forall l, Zlength l = 0 -> l = nil.
 Proof.
-Intro l; Rewrite Zlength_correct.
-Case l; Auto.
-Intros x l'; Simpl (length (cons x l')).
-Rewrite inj_S.
-Intros; ElimType False; Generalize (ZERO_le_inj (length l')); Omega.
+intro l; rewrite Zlength_correct.
+case l; auto.
+intros x l'; simpl (length (x :: l')) in |- *.
+rewrite Znat.inj_S.
+intros; elimtype False; generalize (Zle_0_nat (length l')); omega.
 Qed.
 
 End Zlength_properties.
 
-Implicits Zlength_correct [1].
-Implicits Zlength_cons [1].
-Implicits Zlength_nil_inv [1].
+Implicit Arguments Zlength_correct [A].
+Implicit Arguments Zlength_cons [A].
+Implicit Arguments Zlength_nil_inv [A].
\ No newline at end of file