Modularization of BinPos + fixes in Stdlib

 BinPos now contain a sub-module Pos, in which are placed functions
 like add (ex-Pplus), mul (ex-Pmult), ... and properties like
 add_comm, add_assoc, ...

 In addition to the name changes, the organisation is changed quite
 a lot, to try to take advantage more of the orders < and <= instead
 of speaking only of the comparison function.

 The main source of incompatibilities in scripts concerns this compare:
 Pos.compare is now a binary operation, expressed in terms of the
 ex-Pcompare which is ternary (expecting an initial comparision as 3rd arg),
 this ternary version being called now Pos.compare_cont. As for everything
 else, compatibility notations (only parsing) are provided. But notations
 "_ ?= _" on positive will have to be edited, since they now point to
 Pos.compare.

 We also make the sub-module Pos to be directly an OrderedType,
 and include results about min and max.

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

8 files changed, 50 insertions, 55 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 6e5443e35..61885951d 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -69,13 +69,13 @@ Definition Zplus (x y:Z) :=
     | Zneg x', Z0 => Zneg x'
     | Zpos x', Zpos y' => Zpos (x' + y')
     | Zpos x', Zneg y' =>
-      match (x' ?= y')%positive Eq with
+      match (x' ?= y')%positive with
 	| Eq => Z0
 	| Lt => Zneg (y' - x')
 	| Gt => Zpos (x' - y')
       end
     | Zneg x', Zpos y' =>
-      match (x' ?= y')%positive Eq with
+      match (x' ?= y')%positive with
 	| Eq => Z0
 	| Lt => Zpos (y' - x')
 	| Gt => Zneg (x' - y')
@@ -132,11 +132,11 @@ Definition Zcompare (x y:Z) :=
     | Z0, Zpos y' => Lt
     | Z0, Zneg y' => Gt
     | Zpos x', Z0 => Gt
-    | Zpos x', Zpos y' => (x' ?= y')%positive Eq
+    | Zpos x', Zpos y' => (x' ?= y')%positive
     | Zpos x', Zneg y' => Gt
     | Zneg x', Z0 => Lt
     | Zneg x', Zpos y' => Lt
-    | Zneg x', Zneg y' => CompOpp ((x' ?= y')%positive Eq)
+    | Zneg x', Zneg y' => CompOpp ((x' ?= y')%positive)
   end.
 
 Infix "?=" := Zcompare (at level 70, no associativity) : Z_scope.
@@ -270,8 +270,8 @@ Theorem Zplus_comm : forall n m:Z, n + m = m + n.
 Proof.
   induction n as [|p|p]; intros [|q|q]; simpl; try reflexivity.
   rewrite Pplus_comm; reflexivity.
-  rewrite ZC4. now case Pcompare_spec.
-  rewrite ZC4; now case Pcompare_spec.
+  rewrite Pos.compare_antisym. now case Pcompare_spec.
+  rewrite Pos.compare_antisym. now case Pcompare_spec.
   rewrite Pplus_comm; reflexivity.
 Qed.
 
@@ -280,7 +280,7 @@ Qed.
 Theorem Zopp_plus_distr : forall n m:Z, - (n + m) = - n + - m.
 Proof.
   intro x; destruct x as [| p| p]; intro y; destruct y as [| q| q];
-    simpl; reflexivity || destruct ((p ?= q)%positive Eq);
+    simpl; reflexivity || destruct ((p ?= q)%positive);
       reflexivity.
 Qed.
 
@@ -319,8 +319,7 @@ Proof.
  assert (H := Plt_plus_r z x). rewrite Pplus_comm in H. apply ZC2 in H.
  now rewrite H, Pplus_minus_eq.
  (* y < z *)
- assert (Hz : (z = (z-y)+y)%positive).
-  rewrite Pplus_comm, Pplus_minus_lt; trivial.
+ assert (Hz : (z = (z-y)+y)%positive) by (now rewrite Pos.sub_add).
  pattern z at 4. rewrite Hz, Pplus_compare_mono_r.
  case Pcompare_spec; intros E1; trivial; f_equal.
  symmetry. rewrite Pplus_comm. apply Pminus_plus_distr.
@@ -627,13 +626,12 @@ Proof.
   reflexivity.
 Qed.
 
-Lemma Zpos_minus_morphism : forall a b:positive, Pcompare a b Eq = Lt ->
+Lemma Zpos_minus_morphism : forall a b:positive, Pos.compare a b = Lt ->
   Zpos (b-a) = Zpos b - Zpos a.
 Proof.
   intros.
   simpl.
-  change Eq with (CompOpp Eq).
-  rewrite <- Pcompare_antisym.
+  rewrite Pos.compare_antisym.
   rewrite H; simpl; auto.
 Qed.
 
@@ -800,7 +798,7 @@ Lemma weak_Zmult_plus_distr_r :
 Proof.
  intros x [ |y|y] [ |z|z]; simpl; trivial; f_equal;
   apply Pmult_plus_distr_l || rewrite Pmult_compare_mono_l;
-  case_eq ((y ?= z) Eq)%positive; intros H; trivial;
+  case_eq ((y ?= z)%positive); intros H; trivial;
    rewrite Pmult_minus_distr_l; trivial; now apply ZC1.
 Qed.
 
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index 3a0d7090d..62cce1d26 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -220,10 +220,10 @@ Module MoreInt (I:Int).
       | (?x \/ ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPor ex ey)
       | (~ ?x) => let ex := p2ep x in constr:(EPneg ex)
       | (eq (A:=Z) ?x ?y) => let ex := z2ez x with ey := z2ez y in constr:(EPeq ex ey)
-      | (?x<?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPlt ex ey)
-      | (?x<=?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPle ex ey)
-      | (?x>?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPgt ex ey)
-      | (?x>=?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPge ex ey)
+      | (?x < ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPlt ex ey)
+      | (?x <= ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPle ex ey)
+      | (?x > ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPgt ex ey)
+      | (?x >= ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPge ex ey)
       | ?x =>  constr:(EPraw x)
     end.
 
diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v
index 19e46bb2d..becd34f11 100644
--- a/theories/ZArith/Zcompare.v
+++ b/theories/ZArith/Zcompare.v
@@ -79,7 +79,7 @@ Lemma Zcompare_Lt_trans :
 Proof.
  intros n m p; destruct n,m,p; simpl; try discriminate; trivial.
  eapply Plt_trans; eauto.
- rewrite 3 Pcompare_antisym; simpl. intros; eapply Plt_trans; eauto.
+ rewrite <- 3 Pos.compare_antisym; simpl. intros; eapply Plt_trans; eauto.
 Qed.
 
 Lemma Zcompare_Gt_trans :
@@ -96,7 +96,7 @@ Qed.
 
 Lemma Zcompare_opp : forall n m:Z, (n ?= m) = (- m ?= - n).
 Proof.
- destruct n, m; simpl; trivial; intros; now rewrite <- ZC4.
+ destruct n, m; simpl; trivial; intros; now rewrite <- Pos.compare_antisym.
 Qed.
 
 (** * Comparison first-order specification *)
@@ -134,14 +134,14 @@ Proof.
  case Pcompare_spec; intros E0; simpl; subst.
   now case Pcompare_spec.
   case Pcompare_spec; intros E1; simpl; subst; trivial.
-  now rewrite <- ZC4.
+  now rewrite <- Pos.compare_antisym.
   f_equal.
   apply Pminus_compare_mono_r; trivial.
-  rewrite <- ZC4. symmetry. now apply Plt_trans with z.
+  rewrite <- Pos.compare_antisym. symmetry. now apply Plt_trans with z.
   case Pcompare_spec; intros E1; simpl; subst; trivial.
   now rewrite E0.
   symmetry. apply CompOpp_iff. now apply Plt_trans with z.
-  rewrite <- ZC4.
+  rewrite <- Pos.compare_antisym.
   apply Pminus_compare_mono_l; trivial.
 Qed.
 
diff --git a/theories/ZArith/Zdiv_def.v b/theories/ZArith/Zdiv_def.v
index a45d433c8..87e04b0be 100644
--- a/theories/ZArith/Zdiv_def.v
+++ b/theories/ZArith/Zdiv_def.v
@@ -207,7 +207,7 @@ Proof.
  split. now apply Zle_minus_le_0.
   apply AUX.
   destruct r as [|r|r]; try (now destruct Hr); try easy.
-  red. simpl. apply Pcompare_eq_Lt. exact Hr'.
+  red. simpl. apply Pcompare_Gt_Lt. exact Hr'.
  (* ~0 *)
  destruct Zdiv_eucl_POS as (q,r). cbv zeta.
  simpl in IHa; destruct IHa as (Hr,Hr').
diff --git a/theories/ZArith/Zgcd_def.v b/theories/ZArith/Zgcd_def.v
index 1785d4e66..ad4c35eee 100644
--- a/theories/ZArith/Zgcd_def.v
+++ b/theories/ZArith/Zgcd_def.v
@@ -6,20 +6,20 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import BinPos BinInt Pgcd.
+Require Import BinPos BinInt.
 
 Open Local Scope Z_scope.
 
-(** * Definition of a Pgcd function for relative numbers *)
+(** * Definition of a gcd function for relative numbers *)
 
 Definition Zgcd (a b : Z) : Z :=
   match a,b with
     | Z0, _ => Zabs b
     | _, Z0 => Zabs a
-    | Zpos a, Zpos b => Zpos (Pgcd a b)
-    | Zpos a, Zneg b => Zpos (Pgcd a b)
-    | Zneg a, Zpos b => Zpos (Pgcd a b)
-    | Zneg a, Zneg b => Zpos (Pgcd a b)
+    | Zpos a, Zpos b => Zpos (Pos.gcd a b)
+    | Zpos a, Zneg b => Zpos (Pos.gcd a b)
+    | Zneg a, Zpos b => Zpos (Pos.gcd a b)
+    | Zneg a, Zneg b => Zpos (Pos.gcd a b)
   end.
 
 (** * Generalized Gcd, also computing division of a and b by gcd. *)
@@ -29,13 +29,13 @@ Definition Zggcd (a b : Z) : Z*(Z*Z) :=
     | Z0, _ => (Zabs b,(Z0, Zsgn b))
     | _, Z0 => (Zabs a,(Zsgn a, Z0))
     | Zpos a, Zpos b =>
-       let '(g,(aa,bb)) := Pggcd a b in (Zpos g, (Zpos aa, Zpos bb))
+       let '(g,(aa,bb)) := Pos.ggcd a b in (Zpos g, (Zpos aa, Zpos bb))
     | Zpos a, Zneg b =>
-       let '(g,(aa,bb)) := Pggcd a b in (Zpos g, (Zpos aa, Zneg bb))
+       let '(g,(aa,bb)) := Pos.ggcd a b in (Zpos g, (Zpos aa, Zneg bb))
     | Zneg a, Zpos b =>
-       let '(g,(aa,bb)) := Pggcd a b in (Zpos g, (Zneg aa, Zpos bb))
+       let '(g,(aa,bb)) := Pos.ggcd a b in (Zpos g, (Zneg aa, Zpos bb))
     | Zneg a, Zneg b =>
-       let '(g,(aa,bb)) := Pggcd a b in (Zpos g, (Zneg aa, Zneg bb))
+       let '(g,(aa,bb)) := Pos.ggcd a b in (Zpos g, (Zneg aa, Zneg bb))
   end.
 
 (** The first component of Zggcd is Zgcd *)
@@ -43,7 +43,7 @@ Definition Zggcd (a b : Z) : Z*(Z*Z) :=
 Lemma Zggcd_gcd : forall a b, fst (Zggcd a b) = Zgcd a b.
 Proof.
  intros [ |p|p] [ |q|q]; simpl; auto;
-  generalize (Pggcd_gcd p q); destruct Pggcd as (g,(aa,bb)); simpl; congruence.
+  generalize (Pos.ggcd_gcd p q); destruct Pos.ggcd as (g,(aa,bb)); simpl; congruence.
 Qed.
 
 (** The other components of Zggcd are indeed the correct factors. *)
@@ -53,8 +53,8 @@ Lemma Zggcd_correct_divisors : forall a b,
   a = g*aa /\ b = g*bb.
 Proof.
  intros [ |p|p] [ |q|q]; simpl; rewrite ?Pmult_1_r; auto;
-  generalize (Pggcd_correct_divisors p q);
-  destruct Pggcd as (g,(aa,bb)); simpl; destruct 1; subst; auto.
+  generalize (Pos.ggcd_correct_divisors p q);
+  destruct Pos.ggcd as (g,(aa,bb)); simpl; destruct 1; subst; auto.
 Qed.
 
 (** Divisibility. We use here a simple "exists", while the historical
@@ -102,11 +102,11 @@ Qed.
 
 Lemma Zgcd_greatest : forall a b c, (c|a) -> (c|b) -> (c|Zgcd a b).
 Proof.
- assert (D : forall p q c, (c|Zpos p) -> (c|Zpos q) -> (c|Zpos (Pgcd p q))).
+ assert (D : forall p q c, (c|Zpos p) -> (c|Zpos q) -> (c|Zpos (Pos.gcd p q))).
   intros p q [|r|r] H H'.
   apply Zdivide'_0_l in H. discriminate.
-  apply Zdivide'_Pdivide, Pgcd_greatest; now apply Zdivide'_Pdivide.
-  apply Zdivide'_Zpos_Zneg_l, Zdivide'_Pdivide, Pgcd_greatest;
+  apply Zdivide'_Pdivide, Pos.gcd_greatest; now apply Zdivide'_Pdivide.
+  apply Zdivide'_Zpos_Zneg_l, Zdivide'_Pdivide, Pos.gcd_greatest;
    now apply Zdivide'_Pdivide, Zdivide'_Zpos_Zneg_l.
  intros [ |p|p] [ |q|q]; simpl; auto; intros; try apply D; trivial;
   now apply Zdivide'_Zpos_Zneg_r.
@@ -135,5 +135,5 @@ Theorem Zggcd_opp: forall x y,
                  (g,(-aa,bb)).
 Proof.
 intros [|x|x] [|y|y]; unfold Zggcd, Zopp; auto;
- destruct (Pggcd x y) as (g,(aa,bb)); auto.
+ destruct (Pos.ggcd x y) as (g,(aa,bb)); auto.
 Qed.
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index 482a96f43..375646bbd 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -83,9 +83,8 @@ Definition Zplus_max_distr_r : forall n m p:Z, Zmax (n + p) (m + p) = Zmax n m +
 
 Lemma Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q).
 Proof.
- intros; unfold Zmax, Pmax; simpl; generalize (Pcompare_Eq_eq p q).
- destruct Pcompare; auto.
- intro H; rewrite H; auto.
+ intros; unfold Zmax, Pmax. simpl.
+ case Pos.compare_spec; auto; congruence.
 Qed.
 
 Lemma Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p.
@@ -97,9 +96,8 @@ Qed.
 
 Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q).
 Proof.
-  intros; simpl. destruct (Pcompare p q Eq) as [ ]_eqn:H.
-  rewrite (Pcompare_Eq_eq _ _ H).
-  unfold Pminus; rewrite Pminus_mask_diag; reflexivity.
+  intros; simpl. case Pos.compare_spec; intros H.
+  now rewrite H, Pos.sub_diag.
   rewrite Pminus_Lt; auto.
   symmetry. apply Zpos_max_1.
 Qed.
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index 84155d6f2..98aea6d20 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -80,8 +80,7 @@ Notation Zmin_plus := Z.add_min_distr_r (only parsing).
 
 Lemma Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q).
 Proof.
- intros; unfold Zmin, Pmin; simpl; generalize (Pcompare_Eq_eq p q).
- destruct Pcompare; auto.
+ intros; unfold Zmin, Pmin; simpl. destruct Pos.compare; auto.
 Qed.
 
 Lemma Zpos_min_1 : forall p, Zmin 1 (Zpos p) = 1.
diff --git a/theories/ZArith/Zsqrt_def.v b/theories/ZArith/Zsqrt_def.v
index 824a447c2..b3d1fa1eb 100644
--- a/theories/ZArith/Zsqrt_def.v
+++ b/theories/ZArith/Zsqrt_def.v
@@ -8,7 +8,7 @@
 
 (** Definition of a square root function for Z. *)
 
-Require Import BinPos BinInt Psqrt.
+Require Import BinPos BinInt.
 
 Local Open Scope Z_scope.
 
@@ -16,7 +16,7 @@ Definition Zsqrtrem n :=
  match n with
   | 0 => (0, 0)
   | Zpos p =>
-    match Psqrtrem p with
+    match Pos.sqrtrem p with
      | (s, IsPos r) => (Zpos s, Zpos r)
      | (s, _) => (Zpos s, 0)
     end
@@ -26,7 +26,7 @@ Definition Zsqrtrem n :=
 Definition Zsqrt n :=
  match n with
   | 0 => 0
-  | Zpos p => Zpos (Psqrt p)
+  | Zpos p => Zpos (Pos.sqrt p)
   | Zneg _ => 0
  end.
 
@@ -34,7 +34,7 @@ Lemma Zsqrtrem_spec : forall n, 0<=n ->
  let (s,r) := Zsqrtrem n in n = s*s + r /\ 0 <= r <= 2*s.
 Proof.
  destruct n. now repeat split.
- generalize (Psqrtrem_spec p). simpl.
+ generalize (Pos.sqrtrem_spec p). simpl.
  destruct 1; simpl; subst; now repeat split.
  now destruct 1.
 Qed.
@@ -43,7 +43,7 @@ Lemma Zsqrt_spec : forall n, 0<=n ->
  let s := Zsqrt n in s*s <= n < (Zsucc s)*(Zsucc s).
 Proof.
  destruct n. now repeat split. unfold Zsqrt.
- rewrite <- Zpos_succ_morphism. intros _. apply (Psqrt_spec p).
+ rewrite <- Zpos_succ_morphism. intros _. apply (Pos.sqrt_spec p).
  now destruct 1.
 Qed.
 
@@ -55,6 +55,6 @@ Qed.
 Lemma Zsqrtrem_sqrt : forall n, fst (Zsqrtrem n) = Zsqrt n.
 Proof.
  destruct n; try reflexivity.
- unfold Zsqrtrem, Zsqrt, Psqrt.
- destruct (Psqrtrem p) as (s,r). now destruct r.
+ unfold Zsqrtrem, Zsqrt, Pos.sqrt.
+ destruct (Pos.sqrtrem p) as (s,r). now destruct r.
 Qed.
\ No newline at end of file