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, 15 deletions

diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v
index 496fca074..adeba9e48 100644
--- a/theories/Structures/OrderedTypeEx.v
+++ b/theories/Structures/OrderedTypeEx.v
@@ -109,26 +109,18 @@ Module Positive_as_OT <: UsualOrderedType.
   Definition eq_sym := @sym_eq t.
   Definition eq_trans := @trans_eq t.
 
-  Definition lt p q:= (p ?= q) Eq = Lt.
+  Definition lt := Plt.
 
-  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
-  Proof.
-  unfold lt; intros x y z.
-  change ((Zpos x < Zpos y)%Z -> (Zpos y < Zpos z)%Z -> (Zpos x < Zpos z)%Z).
-  omega.
-  Qed.
+  Definition lt_trans := Plt_trans.
 
   Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
   Proof.
-  intros; intro.
-  rewrite H0 in H.
-  unfold lt in H.
-  rewrite Pcompare_refl in H; discriminate.
+  intros x y H. contradict H. rewrite H. apply Plt_irrefl.
   Qed.
 
   Definition compare : forall x y : t, Compare lt eq x y.
   Proof.
-  intros x y. destruct ((x ?= y) Eq) as [ | | ]_eqn.
+  intros x y. destruct (x ?= y) as [ | | ]_eqn.
   apply EQ; apply Pcompare_Eq_eq; assumption.
   apply LT; assumption.
   apply GT; apply ZC1; assumption.
@@ -322,10 +314,10 @@ Module PositiveOrderedTypeBits <: UsualOrderedType.
 
   Lemma eq_dec (x y: positive): {x = y} + {x <> y}.
   Proof.
-  intros. case_eq ((x ?= y) Eq); intros.
+  intros. case_eq (x ?= y); intros.
   left. apply Pcompare_Eq_eq; auto.
-  right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate.
-  right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate.
+  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.
   Qed.
 
 End PositiveOrderedTypeBits.