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

2 files changed, 79 insertions, 87 deletions

diff --git a/theories/Structures/DecidableTypeEx.v b/theories/Structures/DecidableTypeEx.v
index 2c02f8ddd..971fcd7f8 100644
--- a/theories/Structures/DecidableTypeEx.v
+++ b/theories/Structures/DecidableTypeEx.v
@@ -79,9 +79,9 @@ End PairDecidableType.
 Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType.
  Definition t := prod D1.t D2.t.
  Definition eq := @eq t.
- Definition eq_refl := @refl_equal t.
- Definition eq_sym := @sym_eq t.
- Definition eq_trans := @trans_eq t.
+ Definition eq_refl := @eq_refl t.
+ Definition eq_sym := @eq_sym t.
+ Definition eq_trans := @eq_trans t.
  Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }.
  Proof.
  intros (x1,x2) (y1,y2);
diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v
index adeba9e48..83130deb2 100644
--- a/theories/Structures/OrderedTypeEx.v
+++ b/theories/Structures/OrderedTypeEx.v
@@ -21,9 +21,9 @@ Module Type UsualOrderedType.
  Parameter Inline t : Type.
  Definition eq := @eq t.
  Parameter Inline lt : t -> t -> Prop.
- Definition eq_refl := @refl_equal t.
- Definition eq_sym := @sym_eq t.
- Definition eq_trans := @trans_eq t.
+ Definition eq_refl := @eq_refl t.
+ Definition eq_sym := @eq_sym t.
+ Definition eq_trans := @eq_trans t.
  Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
  Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
  Parameter compare : forall x y : t, Compare lt eq x y.
@@ -41,9 +41,9 @@ Module Nat_as_OT <: UsualOrderedType.
   Definition t := nat.
 
   Definition eq := @eq nat.
-  Definition eq_refl := @refl_equal t.
-  Definition eq_sym := @sym_eq t.
-  Definition eq_trans := @trans_eq t.
+  Definition eq_refl := @eq_refl t.
+  Definition eq_sym := @eq_sym t.
+  Definition eq_trans := @eq_trans t.
 
   Definition lt := lt.
 
@@ -53,12 +53,12 @@ Module Nat_as_OT <: UsualOrderedType.
   Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
   Proof. unfold lt, eq; intros; omega. Qed.
 
-  Definition compare : forall x y : t, Compare lt eq x y.
+  Definition compare x y : Compare lt eq x y.
   Proof.
-    intros x y; destruct (nat_compare x y) as [ | | ]_eqn.
-    apply EQ. apply nat_compare_eq; assumption.
-    apply LT. apply nat_compare_Lt_lt; assumption.
-    apply GT. apply nat_compare_Gt_gt; assumption.
+    case_eq (nat_compare x y); intro.
+    - apply EQ. now apply nat_compare_eq.
+    - apply LT. now apply nat_compare_Lt_lt.
+    - apply GT. now apply nat_compare_Gt_gt.
   Defined.
 
   Definition eq_dec := eq_nat_dec.
@@ -68,15 +68,15 @@ End Nat_as_OT.
 
 (** [Z] is an ordered type with respect to the usual order on integers. *)
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 Module Z_as_OT <: UsualOrderedType.
 
   Definition t := Z.
   Definition eq := @eq Z.
-  Definition eq_refl := @refl_equal t.
-  Definition eq_sym := @sym_eq t.
-  Definition eq_trans := @trans_eq t.
+  Definition eq_refl := @eq_refl t.
+  Definition eq_sym := @eq_sym t.
+  Definition eq_trans := @eq_trans t.
 
   Definition lt (x y:Z) := (x<y).
 
@@ -86,81 +86,73 @@ Module Z_as_OT <: UsualOrderedType.
   Lemma lt_not_eq : forall x y, x<y -> ~ x=y.
   Proof. intros; omega. Qed.
 
-  Definition compare : forall x y, Compare lt eq x y.
+  Definition compare x y : Compare lt eq x y.
   Proof.
-    intros x y; destruct (x ?= y) as [ | | ]_eqn.
-    apply EQ; apply Zcompare_Eq_eq; assumption.
-    apply LT; assumption.
-    apply GT; apply Zgt_lt; assumption.
+    case_eq (x ?= y); intro.
+    - apply EQ. now apply Z.compare_eq.
+    - apply LT. assumption.
+    - apply GT. now apply Z.gt_lt.
   Defined.
 
-  Definition eq_dec := Z_eq_dec.
+  Definition eq_dec := Z.eq_dec.
 
 End Z_as_OT.
 
 (** [positive] is an ordered type with respect to the usual order on natural numbers. *)
 
-Open Local Scope positive_scope.
+Local Open Scope positive_scope.
 
 Module Positive_as_OT <: UsualOrderedType.
   Definition t:=positive.
   Definition eq:=@eq positive.
-  Definition eq_refl := @refl_equal t.
-  Definition eq_sym := @sym_eq t.
-  Definition eq_trans := @trans_eq t.
+  Definition eq_refl := @eq_refl t.
+  Definition eq_sym := @eq_sym t.
+  Definition eq_trans := @eq_trans t.
 
-  Definition lt := Plt.
+  Definition lt := Pos.lt.
 
-  Definition lt_trans := Plt_trans.
+  Definition lt_trans := Pos.lt_trans.
 
   Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
   Proof.
-  intros x y H. contradict H. rewrite H. apply Plt_irrefl.
+  intros x y H. contradict H. rewrite H. apply Pos.lt_irrefl.
   Qed.
 
-  Definition compare : forall x y : t, Compare lt eq x y.
+  Definition compare x y : Compare lt eq x y.
   Proof.
-  intros x y. destruct (x ?= y) as [ | | ]_eqn.
-  apply EQ; apply Pcompare_Eq_eq; assumption.
-  apply LT; assumption.
-  apply GT; apply ZC1; assumption.
+  case_eq (x ?= y); intros H.
+  - apply EQ. now apply Pos.compare_eq.
+  - apply LT; assumption.
+  - apply GT. now apply Pos.gt_lt.
   Defined.
 
-  Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
-  Proof.
-   intros; unfold eq; decide equality.
-  Defined.
+  Definition eq_dec := Pos.eq_dec.
 
 End Positive_as_OT.
 
 
 (** [N] is an ordered type with respect to the usual order on natural numbers. *)
 
-Open Local Scope positive_scope.
-
 Module N_as_OT <: UsualOrderedType.
   Definition t:=N.
   Definition eq:=@eq N.
-  Definition eq_refl := @refl_equal t.
-  Definition eq_sym := @sym_eq t.
-  Definition eq_trans := @trans_eq t.
+  Definition eq_refl := @eq_refl t.
+  Definition eq_sym := @eq_sym t.
+  Definition eq_trans := @eq_trans t.
 
-  Definition lt:=Nlt.
-  Definition lt_trans := Nlt_trans.
-  Definition lt_not_eq := Nlt_not_eq.
+  Definition lt := N.lt.
+  Definition lt_trans := N.lt_trans.
+  Definition lt_not_eq := N.lt_neq.
 
-  Definition compare : forall x y : t, Compare lt eq x y.
+  Definition compare x y : Compare lt eq x y.
   Proof.
-  intros x y. destruct (x ?= y)%N as [ | | ]_eqn.
-  apply EQ; apply Ncompare_Eq_eq; assumption.
-  apply LT; assumption.
-  apply GT. apply Ngt_Nlt; assumption.
+  case_eq (x ?= y)%N; intro.
+  - apply EQ. now apply N.compare_eq.
+  - apply LT. assumption.
+  - apply GT. now apply N.gt_lt.
   Defined.
 
-  Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
-  Proof.
-   intros. unfold eq. decide equality. apply Positive_as_OT.eq_dec.
-  Defined.
+  Definition eq_dec := N.eq_dec.
 
 End N_as_OT.
 
@@ -240,9 +232,9 @@ End PairOrderedType.
 Module PositiveOrderedTypeBits <: UsualOrderedType.
   Definition t:=positive.
   Definition eq:=@eq positive.
-  Definition eq_refl := @refl_equal t.
-  Definition eq_sym := @sym_eq t.
-  Definition eq_trans := @trans_eq t.
+  Definition eq_refl := @eq_refl t.
+  Definition eq_sym := @eq_sym t.
+  Definition eq_trans := @eq_trans t.
 
   Fixpoint bits_lt (p q:positive) : Prop :=
    match p, q with
@@ -286,38 +278,38 @@ Module PositiveOrderedTypeBits <: UsualOrderedType.
   Definition compare : forall x y : t, Compare lt eq x y.
   Proof.
   induction x; destruct y.
-  (* I I *)
-  destruct (IHx y).
-  apply LT; auto.
-  apply EQ; rewrite e; red; auto.
-  apply GT; auto.
-  (* I O *)
-  apply GT; simpl; auto.
-  (* I H *)
-  apply GT; simpl; auto.
-  (* O I *)
-  apply LT; simpl; auto.
-  (* O O *)
-  destruct (IHx y).
-  apply LT; auto.
-  apply EQ; rewrite e; red; auto.
-  apply GT; auto.
-  (* O H *)
-  apply LT; simpl; auto.
-  (* H I *)
-  apply LT; simpl; auto.
-  (* H O *)
-  apply GT; simpl; auto.
-  (* H H *)
-  apply EQ; red; auto.
+  - (* I I *)
+    destruct (IHx y).
+    apply LT; auto.
+    apply EQ; rewrite e; red; auto.
+    apply GT; auto.
+  - (* I O *)
+    apply GT; simpl; auto.
+  - (* I H *)
+    apply GT; simpl; auto.
+  - (* O I *)
+    apply LT; simpl; auto.
+  - (* O O *)
+    destruct (IHx y).
+    apply LT; auto.
+    apply EQ; rewrite e; red; auto.
+    apply GT; auto.
+  - (* O H *)
+    apply LT; simpl; auto.
+  - (* H I *)
+    apply LT; simpl; auto.
+  - (* H O *)
+    apply GT; simpl; auto.
+  - (* H H *)
+    apply EQ; red; auto.
   Qed.
 
   Lemma eq_dec (x y: positive): {x = y} + {x <> y}.
   Proof.
   intros. case_eq (x ?= y); intros.
-  left. apply Pcompare_Eq_eq; auto.
-  right. red. intro. subst y. rewrite (Pos.compare_refl x) in H. discriminate.
-  right. red. intro. subst y. rewrite (Pos.compare_refl x) in H. discriminate.
+  - left. now apply Pos.compare_eq.
+  - right. intro. subst y. now rewrite (Pos.compare_refl x) in *.
+  - right. intro. subst y. now rewrite (Pos.compare_refl x) in *.
   Qed.
 
 End PositiveOrderedTypeBits.