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

1 files changed, 7 insertions, 9 deletions

diff --git a/plugins/setoid_ring/Cring_initial.v b/plugins/setoid_ring/Cring_initial.v
index 4a0beb3fa4..3cd9d4d3e3 100644
--- a/plugins/setoid_ring/Cring_initial.v
+++ b/plugins/setoid_ring/Cring_initial.v
@@ -147,7 +147,7 @@ Ltac rsimpl := simpl;  set_cring_notations.
 
  Lemma gen_phiZ1_add_pos_neg : forall x y,
  gen_phiZ1
-    match (x ?= y)%positive Eq with
+    match (x ?= y)%positive with
     | Eq => Z0
     | Lt => Zneg (y - x)
     | Gt => Zpos (x - y)
@@ -155,12 +155,11 @@ Ltac rsimpl := simpl;  set_cring_notations.
  == gen_phiPOS1 x + -gen_phiPOS1 y.
  Proof.
   intros x y.
-  assert (H:= (Pcompare_Eq_eq x y)); assert (H0 := Pminus_mask_Gt x y).
-  generalize (Pminus_mask_Gt y x).
-  replace Eq with (CompOpp Eq);[intro H1;simpl|trivial].
-  rewrite <- Pcompare_antisym in H1.
-  destruct ((x ?= y)%positive Eq).
-  cring_rewrite H;trivial. cring_rewrite cring_opp_def;gen_reflexivity.
+  assert (H0 := Pminus_mask_Gt x y). unfold Pgt in H0.
+  assert (H1 := Pminus_mask_Gt y x). unfold Pgt in H1.
+  rewrite Pos.compare_antisym in H1.
+  destruct (Pos.compare_spec x y) as [H|H|H].
+  subst. cring_rewrite cring_opp_def;gen_reflexivity.
   destruct H1 as [h [Heq1 [Heq2 Hor]]];trivial.
   unfold Pminus; cring_rewrite Heq1;rewrite <- Heq2.
   cring_rewrite ARgen_phiPOS_add;simpl;norm.
@@ -182,8 +181,7 @@ Ltac rsimpl := simpl;  set_cring_notations.
   induction x;destruct y;simpl;norm.
   apply ARgen_phiPOS_add.
   apply gen_phiZ1_add_pos_neg.
-  replace Eq with (CompOpp Eq);trivial.
-  rewrite <- Pcompare_antisym;simpl.
+  rewrite Pos.compare_antisym;simpl.
   cring_rewrite match_compOpp.
   cring_rewrite cring_add_comm.
   apply gen_phiZ1_add_pos_neg.