ZArith + other : favor the use of modern names instead of compat notations

 - For instance, refl_equal --> eq_refl
 - Npos, Zpos, Zneg now admit more uniform qualified aliases
   N.pos, Z.pos, Z.neg.
 - A new module BinInt.Pos2Z with results about injections from
   positive to Z
 - A result about Z.pow pushed in the generic layer
 - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
 - Using tactic Z.le_elim instead of Zle_lt_or_eq
 - Some cleanup in ring, field, micromega
   (use of "Equivalence", "Proper" ...)
 - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
 - In ZMake and ZMake, functor parameters are now named NN and ZZ
   instead of N and Z for avoiding confusions

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 29 insertions, 54 deletions

diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index ca26787bd..cac3cd4e5 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -21,20 +21,16 @@ Proof.
 Defined.
 (* end hide *)
 
-Lemma Zcompare_rect :
-  forall (P:Type) (n m:Z),
-    ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P.
+Lemma Zcompare_rect (P:Type) (n m:Z) :
+  ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P.
 Proof.
-  intros * H1 H2 H3.
+  intros H1 H2 H3.
   destruct (n ?= m); auto.
 Defined.
 
-Lemma Zcompare_rec :
-  forall (P:Set) (n m:Z),
-    ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P.
-Proof.
-  intro; apply Zcompare_rect.
-Defined.
+Lemma Zcompare_rec (P:Set) (n m:Z) :
+  ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P.
+Proof. apply Zcompare_rect. Defined.
 
 Notation Z_eq_dec := Z.eq_dec (compat "8.3").
 
@@ -46,38 +42,22 @@ Section decidability.
 
   Definition Z_lt_dec : {x < y} + {~ x < y}.
   Proof.
-    unfold Zlt in |- *.
-    apply Zcompare_rec with (n := x) (m := y); intro H.
-    right. rewrite H. discriminate.
-    left; assumption.
-    right. rewrite H. discriminate.
+    unfold Z.lt; case Z.compare; (now left) || (now right).
   Defined.
 
   Definition Z_le_dec : {x <= y} + {~ x <= y}.
   Proof.
-    unfold Zle in |- *.
-    apply Zcompare_rec with (n := x) (m := y); intro H.
-    left. rewrite H. discriminate.
-    left. rewrite H. discriminate.
-    right. tauto.
+    unfold Z.le; case Z.compare; (now left) || (right; tauto).
   Defined.
 
   Definition Z_gt_dec : {x > y} + {~ x > y}.
   Proof.
-    unfold Zgt in |- *.
-    apply Zcompare_rec with (n := x) (m := y); intro H.
-    right. rewrite H. discriminate.
-    right. rewrite H. discriminate.
-    left; assumption.
+    unfold Z.gt; case Z.compare; (now left) || (now right).
   Defined.
 
   Definition Z_ge_dec : {x >= y} + {~ x >= y}.
   Proof.
-    unfold Zge in |- *.
-    apply Zcompare_rec with (n := x) (m := y); intro H.
-    left. rewrite H. discriminate.
-    right. tauto.
-    left. rewrite H. discriminate.
+    unfold Z.ge; case Z.compare; (now left) || (right; tauto).
   Defined.
 
   Definition Z_lt_ge_dec : {x < y} + {x >= y}.
@@ -87,16 +67,15 @@ Section decidability.
 
   Lemma Z_lt_le_dec : {x < y} + {y <= x}.
   Proof.
-    intros.
     elim Z_lt_ge_dec.
-    intros; left; assumption.
-    intros; right; apply Zge_le; assumption.
+    * now left.
+    * right; now apply Z.ge_le.
   Defined.
 
   Definition Z_le_gt_dec : {x <= y} + {x > y}.
   Proof.
     elim Z_le_dec; auto with arith.
-    intro. right. apply Znot_le_gt; auto with arith.
+    intro. right. Z.swap_greater. now apply Z.nle_gt.
   Defined.
 
   Definition Z_gt_le_dec : {x > y} + {x <= y}.
@@ -107,15 +86,15 @@ Section decidability.
   Definition Z_ge_lt_dec : {x >= y} + {x < y}.
   Proof.
     elim Z_ge_dec; auto with arith.
-    intro. right. apply Znot_ge_lt; auto with arith.
+    intro. right. Z.swap_greater. now apply Z.lt_nge.
   Defined.
 
   Definition Z_le_lt_eq_dec : x <= y -> {x < y} + {x = y}.
   Proof.
     intro H.
     apply Zcompare_rec with (n := x) (m := y).
-    intro. right. elim (Zcompare_Eq_iff_eq x y); auto with arith.
-    intro. left. elim (Zcompare_Eq_iff_eq x y); auto with arith.
+    intro. right. elim (Z.compare_eq_iff x y); auto with arith.
+    intro. left. elim (Z.compare_eq_iff x y); auto with arith.
     intro H1. absurd (x > y); auto with arith.
   Defined.
 
@@ -132,8 +111,8 @@ Proof.
   assumption.
   intro.
   right.
-  apply Zle_lt_trans with (m := x).
-  apply Zge_le.
+  apply Z.le_lt_trans with (m := x).
+  apply Z.ge_le.
   assumption.
   assumption.
 Defined.
@@ -142,20 +121,16 @@ Lemma Zlt_cotrans_pos : forall n m:Z, 0 < n + m -> {0 < n} + {0 < m}.
 Proof.
   intros x y H.
   case (Zlt_cotrans 0 (x + y) H x).
-  intro.
-  left.
-  assumption.
-  intro.
-  right.
-  apply Zplus_lt_reg_l with (p := x).
-  rewrite Zplus_0_r.
-  assumption.
+  - now left.
+  - right.
+    apply Z.add_lt_mono_l with (p := x).
+    now rewrite Z.add_0_r.
 Defined.
 
 Lemma Zlt_cotrans_neg : forall n m:Z, n + m < 0 -> {n < 0} + {m < 0}.
 Proof.
   intros x y H; case (Zlt_cotrans (x + y) 0 H x); intro Hxy;
-    [ right; apply Zplus_lt_reg_l with (p := x); rewrite Zplus_0_r | left ];
+    [ right; apply Z.add_lt_mono_l with (p := x); rewrite Z.add_0_r | left ];
     assumption.
 Defined.
 
@@ -167,7 +142,7 @@ Proof.
   left.
   assumption.
   intro H0.
-  generalize (Zge_le _ _ H0).
+  generalize (Z.ge_le _ _ H0).
   intro.
   case (Z_le_lt_eq_dec _ _ H1).
   intro.
@@ -189,13 +164,13 @@ Proof.
   left.
   assumption.
   intro H.
-  generalize (Zge_le _ _ H).
+  generalize (Z.ge_le _ _ H).
   intro H0.
   case (Z_le_lt_eq_dec y x H0).
   intro H1.
   left.
   right.
-  apply Zlt_gt.
+  apply Z.lt_gt.
   assumption.
   intro.
   right.
@@ -207,7 +182,7 @@ Defined.
 Lemma Z_dec' : forall n m:Z, {n < m} + {m < n} + {n = m}.
 Proof.
   intros x y.
-  case (Z_eq_dec x y); intro H;
+  case (Z.eq_dec x y); intro H;
     [ right; assumption | left; apply (not_Zeq_inf _ _ H) ].
 Defined.
 
@@ -215,12 +190,12 @@ Defined.
 (* To deprecate ? *)
 Corollary Z_zerop : forall x:Z, {x = 0} + {x <> 0}.
 Proof.
-  exact (fun x:Z => Z_eq_dec x 0).
+  exact (fun x:Z => Z.eq_dec x 0).
 Defined.
 
 Corollary Z_notzerop : forall (x:Z), {x <> 0} + {x = 0}.
 Proof (fun x => sumbool_not _ _ (Z_zerop x)).
 
 Corollary Z_noteq_dec : forall (x y:Z), {x <> y} + {x = y}.
-Proof (fun x y => sumbool_not _ _ (Z_eq_dec x y)).
+Proof (fun x y => sumbool_not _ _ (Z.eq_dec x y)).
 (* end hide *)