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, 135 insertions, 125 deletions

diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index eecfc42b2..4c2efceb1 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -8,14 +8,12 @@
 
 (*i $Id$ i*)
 
-Require BinInt.
-Require Zcompare.
-Require Zorder.
-Require Znat.
-Require Zmisc.
-Require Zsyntax.
-Require Wf_nat.
-V7only [Import Z_scope.].
+Require Import BinInt.
+Require Import Zcompare.
+Require Import Zorder.
+Require Import Znat.
+Require Import Zmisc.
+Require Import Wf_nat.
 Open Local Scope Z_scope.
 
 (** Our purpose is to write an induction shema for {0,1,2,...}
@@ -36,86 +34,83 @@ Open Local Scope Z_scope.
 >>
   Then the  diagram will be closed and the theorem proved. *)
 
-Lemma inject_nat_complete :
-  (x:Z)`0 <= x` -> (EX n:nat | x=(inject_nat n)).
-Intro x; NewDestruct x; Intros;
-[ Exists  O; Auto with arith
-| Specialize (ZL4 p); Intros Hp; Elim Hp; Intros;
-  Exists (S x); Intros; Simpl;
-  Specialize (bij1 x); Intro Hx0;
-  Rewrite <- H0 in Hx0;
-  Apply f_equal with f:=POS;
-  Apply convert_intro; Auto with arith
-| Absurd `0 <= (NEG p)`;
-  [ Unfold Zle; Simpl; Do 2 (Unfold not); Auto with arith
-  | Assumption]
-].
+Lemma Z_of_nat_complete :
+ forall x:Z, 0 <= x ->  exists n : nat | x = Z_of_nat n.
+intro x; destruct x; intros;
+ [ exists 0%nat; auto with arith
+ | specialize (ZL4 p); intros Hp; elim Hp; intros; exists (S x); intros;
+    simpl in |- *; specialize (nat_of_P_o_P_of_succ_nat_eq_succ x); 
+    intro Hx0; rewrite <- H0 in Hx0; apply f_equal with (f := Zpos);
+    apply nat_of_P_inj; auto with arith
+ | absurd (0 <= Zneg p);
+    [ unfold Zle in |- *; simpl in |- *; do 2 unfold not in |- *;
+       auto with arith
+    | assumption ] ].
 Qed.
 
-Lemma ZL4_inf: (y:positive) { h:nat | (convert y)=(S h) }.
-Intro y; NewInduction y as [p H|p H1|]; [
-  Elim H; Intros x H1; Exists (plus (S x) (S x));
-  Unfold convert ;Simpl; Rewrite ZL0; Rewrite ZL2; Unfold convert in H1;
-  Rewrite H1; Auto with arith
-| Elim H1;Intros x H2; Exists (plus x (S x)); Unfold convert;
-  Simpl; Rewrite ZL0; Rewrite ZL2;Unfold convert in H2; Rewrite H2; Auto with arith
-| Exists O ;Auto with arith].
+Lemma ZL4_inf : forall y:positive, {h : nat | nat_of_P y = S h}.
+intro y; induction y as [p H| p H1| ];
+ [ elim H; intros x H1; exists (S x + S x)%nat; unfold nat_of_P in |- *;
+    simpl in |- *; rewrite ZL0; rewrite Pmult_nat_r_plus_morphism;
+    unfold nat_of_P in H1; rewrite H1; auto with arith
+ | elim H1; intros x H2; exists (x + S x)%nat; unfold nat_of_P in |- *;
+    simpl in |- *; rewrite ZL0; rewrite Pmult_nat_r_plus_morphism;
+    unfold nat_of_P in H2; rewrite H2; auto with arith
+ | exists 0%nat; auto with arith ].
 Qed.
 
-Lemma inject_nat_complete_inf :
-  (x:Z)`0 <= x` -> { n:nat | (x=(inject_nat n)) }.
-Intro x; NewDestruct x; Intros;
-[ Exists  O; Auto with arith
-| Specialize (ZL4_inf p); Intros Hp; Elim Hp; Intros x0 H0;
-  Exists (S x0); Intros; Simpl;
-  Specialize (bij1 x0); Intro Hx0;
-  Rewrite <- H0 in Hx0;
-  Apply f_equal with f:=POS;
-  Apply convert_intro; Auto with arith
-| Absurd `0 <= (NEG p)`;
-  [ Unfold Zle; Simpl; Do 2 (Unfold not); Auto with arith
-  | Assumption]
-].
+Lemma Z_of_nat_complete_inf :
+ forall x:Z, 0 <= x -> {n : nat | x = Z_of_nat n}.
+intro x; destruct x; intros;
+ [ exists 0%nat; auto with arith
+ | specialize (ZL4_inf p); intros Hp; elim Hp; intros x0 H0; exists (S x0);
+    intros; simpl in |- *; specialize (nat_of_P_o_P_of_succ_nat_eq_succ x0);
+    intro Hx0; rewrite <- H0 in Hx0; apply f_equal with (f := Zpos);
+    apply nat_of_P_inj; auto with arith
+ | absurd (0 <= Zneg p);
+    [ unfold Zle in |- *; simpl in |- *; do 2 unfold not in |- *;
+       auto with arith
+    | assumption ] ].
 Qed.
 
-Lemma inject_nat_prop :
-  (P:Z->Prop)((n:nat)(P (inject_nat n))) -> 
-    (x:Z) `0 <= x` -> (P x).
-Intros P H x H0.
-Specialize (inject_nat_complete x H0).
-Intros Hn; Elim Hn; Intros.
-Rewrite -> H1; Apply H.
+Lemma Z_of_nat_prop :
+ forall P:Z -> Prop,
+   (forall n:nat, P (Z_of_nat n)) -> forall x:Z, 0 <= x -> P x.
+intros P H x H0.
+specialize (Z_of_nat_complete x H0).
+intros Hn; elim Hn; intros.
+rewrite H1; apply H.
 Qed.
 
-Lemma inject_nat_set :
-  (P:Z->Set)((n:nat)(P (inject_nat n))) -> 
-    (x:Z) `0 <= x` -> (P x).
-Intros P H x H0.
-Specialize (inject_nat_complete_inf x H0).
-Intros Hn; Elim Hn; Intros.
-Rewrite -> p; Apply H.
+Lemma Z_of_nat_set :
+ forall P:Z -> Set,
+   (forall n:nat, P (Z_of_nat n)) -> forall x:Z, 0 <= x -> P x.
+intros P H x H0.
+specialize (Z_of_nat_complete_inf x H0).
+intros Hn; elim Hn; intros.
+rewrite p; apply H.
 Qed.
 
-Lemma natlike_ind : (P:Z->Prop) (P `0`) ->
-  ((x:Z)(`0 <= x` -> (P x) -> (P (Zs x)))) ->
-  (x:Z) `0 <= x` -> (P x).
-Intros P H H0 x H1; Apply inject_nat_prop;
-[ Induction n;
-  [ Simpl; Assumption
-  | Intros; Rewrite -> (inj_S n0);
-    Exact (H0 (inject_nat n0) (ZERO_le_inj n0) H2) ]
-| Assumption].
+Lemma natlike_ind :
+ forall P:Z -> Prop,
+   P 0 ->
+   (forall x:Z, 0 <= x -> P x -> P (Zsucc x)) -> forall x:Z, 0 <= x -> P x.
+intros P H H0 x H1; apply Z_of_nat_prop;
+ [ simple induction n;
+    [ simpl in |- *; assumption
+    | intros; rewrite (inj_S n0); exact (H0 (Z_of_nat n0) (Zle_0_nat n0) H2) ]
+ | assumption ].
 Qed.
 
-Lemma natlike_rec : (P:Z->Set) (P `0`) ->
-  ((x:Z)(`0 <= x` -> (P x) -> (P (Zs x)))) ->
-  (x:Z) `0 <= x` -> (P x).
-Intros P H H0 x H1; Apply inject_nat_set;
-[ Induction n;
-  [ Simpl; Assumption
-  | Intros; Rewrite -> (inj_S n0);
-    Exact (H0 (inject_nat n0) (ZERO_le_inj n0) H2) ]
-| Assumption].
+Lemma natlike_rec :
+ forall P:Z -> Set,
+   P 0 ->
+   (forall x:Z, 0 <= x -> P x -> P (Zsucc x)) -> forall x:Z, 0 <= x -> P x.
+intros P H H0 x H1; apply Z_of_nat_set;
+ [ simple induction n;
+    [ simpl in |- *; assumption
+    | intros; rewrite (inj_S n0); exact (H0 (Z_of_nat n0) (Zle_0_nat n0) H2) ]
+ | assumption ].
 Qed.
 
 Section Efficient_Rec. 
@@ -123,72 +118,87 @@ Section Efficient_Rec.
 (** [natlike_rec2] is the same as [natlike_rec], but with a different proof, designed 
      to give a better extracted term. *)
 
-Local R := [a,b:Z]`0<=a`/\`a<b`.
+Let R (a b:Z) := 0 <= a /\ a < b.
 
-Local R_wf : (well_founded Z R).
+Let R_wf : well_founded R.
 Proof.
-LetTac f := [z]Cases z of (POS p) => (convert p) | ZERO => O | (NEG _) => O end.
-Apply  well_founded_lt_compat with f.
-Unfold R f; Clear f R.
-Intros x y; Case x; Intros; Elim H; Clear H.
-Case y; Intros; Apply compare_convert_O Orelse Inversion H0.
-Case y; Intros; Apply compare_convert_INFERIEUR Orelse Inversion H0; Auto.
-Intros; Elim H; Auto.
+set
+ (f :=
+  fun z =>
+    match z with
+    | Zpos p => nat_of_P p
+    | Z0 => 0%nat
+    | Zneg _ => 0%nat
+    end) in *.
+apply well_founded_lt_compat with f.
+unfold R, f in |- *; clear f R.
+intros x y; case x; intros; elim H; clear H.
+case y; intros; apply lt_O_nat_of_P || inversion H0.
+case y; intros; apply nat_of_P_lt_Lt_compare_morphism || inversion H0; auto.
+intros; elim H; auto.
 Qed.
 
-Lemma natlike_rec2 : (P:Z->Type)(P `0`) -> 
-        ((z:Z)`0<=z` -> (P z) -> (P (Zs z))) -> (z:Z)`0<=z` -> (P z).
+Lemma natlike_rec2 :
+ forall P:Z -> Type,
+   P 0 ->
+   (forall z:Z, 0 <= z -> P z -> P (Zsucc z)) -> forall z:Z, 0 <= z -> P z.
 Proof.
-Intros P Ho Hrec z; Pattern z; Apply (well_founded_induction_type Z R R_wf).
-Intro x; Case x.
-Trivial.
-Intros.
-Assert `0<=(Zpred (POS p))`.
-Apply Zlt_ZERO_pred_le_ZERO; Unfold Zlt; Simpl; Trivial.
-Rewrite Zs_pred.
-Apply Hrec.
-Auto.
-Apply X; Auto; Unfold R; Intuition; Apply Zlt_pred_n_n.
-Intros; Elim H; Simpl; Trivial.
+intros P Ho Hrec z; pattern z in |- *;
+ apply (well_founded_induction_type R_wf).
+intro x; case x.
+trivial.
+intros.
+assert (0 <= Zpred (Zpos p)).
+apply Zorder.Zlt_0_le_0_pred; unfold Zlt in |- *; simpl in |- *; trivial.
+rewrite Zsucc_pred.
+apply Hrec.
+auto.
+apply X; auto; unfold R in |- *; intuition; apply Zlt_pred.
+intros; elim H; simpl in |- *; trivial.
 Qed.
 
 (** A variant of the previous using [Zpred] instead of [Zs]. *)
 
-Lemma natlike_rec3 : (P:Z->Type)(P `0`) -> 
-        ((z:Z)`0<z` -> (P (Zpred z)) -> (P z)) -> (z:Z)`0<=z` -> (P z).
+Lemma natlike_rec3 :
+ forall P:Z -> Type,
+   P 0 ->
+   (forall z:Z, 0 < z -> P (Zpred z) -> P z) -> forall z:Z, 0 <= z -> P z.
 Proof.
-Intros P Ho Hrec z; Pattern z; Apply (well_founded_induction_type Z R R_wf).
-Intro x; Case x.
-Trivial.
-Intros; Apply Hrec.
-Unfold Zlt; Trivial.
-Assert `0<=(Zpred (POS p))`.
-Apply Zlt_ZERO_pred_le_ZERO; Unfold Zlt; Simpl; Trivial.
-Apply X; Auto; Unfold R; Intuition; Apply Zlt_pred_n_n.
-Intros; Elim H; Simpl; Trivial.
+intros P Ho Hrec z; pattern z in |- *;
+ apply (well_founded_induction_type R_wf).
+intro x; case x.
+trivial.
+intros; apply Hrec.
+unfold Zlt in |- *; trivial.
+assert (0 <= Zpred (Zpos p)).
+apply Zorder.Zlt_0_le_0_pred; unfold Zlt in |- *; simpl in |- *; trivial.
+apply X; auto; unfold R in |- *; intuition; apply Zlt_pred.
+intros; elim H; simpl in |- *; trivial.
 Qed.
 
 (** A more general induction principal using [Zlt]. *)
 
-Lemma Z_lt_rec : (P:Z->Type)
- ((x:Z)((y:Z)`0 <= y < x`->(P y))->(P x)) -> (x:Z)`0 <= x`->(P x).
+Lemma Z_lt_rec :
+ forall P:Z -> Type,
+   (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> P x) ->
+   forall x:Z, 0 <= x -> P x.
 Proof.
-Intros P Hrec z; Pattern z; Apply (well_founded_induction_type Z R R_wf).
-Intro x; Case x; Intros.
-Apply Hrec; Intros.
-Assert H2: `0<0`.
-  Apply Zle_lt_trans with y; Intuition.
-Inversion H2.
-Firstorder.
-Unfold Zle Zcompare in H; Elim H; Auto.
+intros P Hrec z; pattern z in |- *; apply (well_founded_induction_type R_wf).
+intro x; case x; intros.
+apply Hrec; intros.
+assert (H2 : 0 < 0).
+  apply Zle_lt_trans with y; intuition.
+inversion H2.
+firstorder.
+unfold Zle, Zcompare in H; elim H; auto.
 Defined.
 
-Lemma Z_lt_induction : 
-  (P:Z->Prop)
-     ((x:Z)((y:Z)`0 <= y < x`->(P y))->(P x))
-  -> (x:Z)`0 <= x`->(P x).
+Lemma Z_lt_induction :
+ forall P:Z -> Prop,
+   (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> P x) ->
+   forall x:Z, 0 <= x -> P x.
 Proof.
-Exact Z_lt_rec.
+exact Z_lt_rec.
 Qed.
 
-End Efficient_Rec.
+End Efficient_Rec.
\ No newline at end of file