NZAxioms plus a compare allows to build an OrderedType

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

2 files changed, 27 insertions, 8 deletions

diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index 480314f96..ee7ee159f 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -16,7 +16,7 @@ Require Export Equalities Orders NumPrelude GenericMinMax.
     and a bi-directional induction principle. We require [P (S n) = n]
     but not the other way around, since this domain is meant
     to be either N or Z. In fact it can be a few other things,
-    for instance [Z/nZ] (See file [NZDomain for a study of that).
+    for instance [Z/nZ] (See file [NZDomain] for a study of that).
 *)
 
 Module Type ZeroSuccPred (Import T:Typ).
@@ -109,3 +109,11 @@ Module Type NZOrdAxiomsSig' <: NZOrdAxiomsSig
  := NZOrdSig' <+ AddSubMul' <+ IsAddSubMul <+ HasMinMax.
 
 
+(** Same, plus a comparison function. *)
+
+Module Type NZDecOrdSig := NZOrdSig <+ HasCompare.
+Module Type NZDecOrdSig' := NZOrdSig' <+ HasCompare.
+
+Module Type NZDecOrdAxiomsSig := NZOrdAxiomsSig <+ HasCompare.
+Module Type NZDecOrdAxiomsSig' := NZOrdAxiomsSig' <+ HasCompare.
+
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 9764d1557..ed59bca43 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -122,7 +122,7 @@ Qed.
 
 (** We know enough now to benefit from the generic [order] tactic. *)
 
-Module OrderElts.
+Module OrderElts <: TotalOrder.
  Definition t := t.
  Definition eq := eq.
  Definition lt := lt.
@@ -252,7 +252,7 @@ reduce to a normal form that will say if the numbers are equal or not,
 which cannot be true in all finite rings. Therefore, we prove decidability
 in the presence of order. *)
 
-Theorem eq_dec : forall n m, decidable (n == m).
+Theorem eq_decidable : forall n m, decidable (n == m).
 Proof.
 intros n m; destruct (lt_trichotomy n m) as [ | [ | ]];
  (right; order) || (left; order).
@@ -263,7 +263,7 @@ Qed.
 Theorem eq_dne : forall n m, ~ ~ n == m <-> n == m.
 Proof.
 intros n m; split; intro H.
-destruct (eq_dec n m) as [H1 | H1].
+destruct (eq_decidable n m) as [H1 | H1].
 assumption. false_hyp H1 H.
 intro H1; now apply H1.
 Qed.
@@ -276,7 +276,7 @@ Proof. intuition order. Qed.
 Theorem nlt_ge : forall n m, ~ n < m <-> n >= m.
 Proof. intuition order. Qed.
 
-Theorem lt_dec : forall n m, decidable (n < m).
+Theorem lt_decidable : forall n m, decidable (n < m).
 Proof.
 intros n m; destruct (le_gt_cases m n); [right|left]; order.
 Qed.
@@ -284,7 +284,7 @@ Qed.
 Theorem lt_dne : forall n m, ~ ~ n < m <-> n < m.
 Proof.
 intros n m; split; intro H.
-destruct (lt_dec n m) as [H1 | H1]; [assumption | false_hyp H1 H].
+destruct (lt_decidable n m) as [H1 | H1]; [assumption | false_hyp H1 H].
 intro H1; false_hyp H H1.
 Qed.
 
@@ -296,7 +296,7 @@ Proof. intuition order. Qed.
 Theorem lt_nge : forall n m, n < m <-> ~ n >= m.
 Proof. intuition order. Qed.
 
-Theorem le_dec : forall n m, decidable (n <= m).
+Theorem le_decidable : forall n m, decidable (n <= m).
 Proof.
 intros n m; destruct (le_gt_cases n m); [left|right]; order.
 Qed.
@@ -304,7 +304,7 @@ Qed.
 Theorem le_dne : forall n m, ~ ~ n <= m <-> n <= m.
 Proof.
 intros n m; split; intro H.
-destruct (le_dec n m) as [H1 | H1]; [assumption | false_hyp H1 H].
+destruct (le_decidable n m) as [H1 | H1]; [assumption | false_hyp H1 H].
 intro H1; false_hyp H H1.
 Qed.
 
@@ -614,3 +614,14 @@ End NZOrderPropSig.
 Module NZOrderPropFunct (NZ : NZOrdSig) :=
  NZBasePropSig NZ <+ NZOrderPropSig NZ.
 
+(** If we have moreover a [compare] function, we can build
+    an [OrderedType] structure. *)
+
+Module NZOrderedTypeFunct (NZ : NZDecOrdSig')
+  <: DecidableTypeFull <: OrderedTypeFull.
+ Include NZ <+ NZOrderPropFunct.
+ Instance lt_compat : Proper (eq==>eq==>iff) lt := lt_wd.
+ Instance lt_strorder : StrictOrder lt.
+ Include Compare2EqBool <+ HasEqBool2Dec.
+ Definition le_lteq := lt_eq_cases.
+End NZOrderedTypeFunct.