Better visibility of the inductive CompSpec used to specify comparison functions

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

3 files changed, 23 insertions, 15 deletions

diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index a684d5a10..1dc74af73 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -171,7 +171,17 @@ Proof.
    apply -> nat_compare_lt; auto.
 Qed.
 
-(** Some projections of the above equivalences, used in OrderedTypeEx. *)
+Lemma nat_compare_spec : forall x y, CompSpec eq lt x y (nat_compare x y).
+Proof.
+ intros.
+ destruct (nat_compare x y) as [ ]_eqn; constructor.
+ apply nat_compare_eq; auto.
+ apply <- nat_compare_lt; auto.
+ apply <- nat_compare_gt; auto.
+Qed.
+
+
+(** Some projections of the above equivalences. *)
 
 Lemma nat_compare_Lt_lt : forall n m, nat_compare n m = Lt -> n<m.
 Proof.
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index 1fb5b3e55..bdd7ce092 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -144,6 +144,13 @@ Proof.
   induction 1; auto with arith.
 Qed.
 
+Theorem le_lt_or_eq_iff : forall n m, n <= m <-> n < m \/ n = m.
+Proof.
+  split.
+  intros; apply le_lt_or_eq; auto.
+  destruct 1; subst; auto with arith.
+Qed.
+
 Theorem lt_le_weak : forall n m, n < m -> n <= m.
 Proof.
   auto with arith.
diff --git a/theories/Arith/NatOrderedType.v b/theories/Arith/NatOrderedType.v
index c4e71632c..dda2fca6c 100644
--- a/theories/Arith/NatOrderedType.v
+++ b/theories/Arith/NatOrderedType.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Peano_dec Compare_dec
+Require Import Lt Peano_dec Compare_dec
  DecidableType2 OrderedType2 OrderedType2Facts.
 
 
@@ -33,26 +33,17 @@ Module Nat_as_OT <: OrderedTypeFull.
  Definition compare := nat_compare.
 
  Instance lt_strorder : StrictOrder lt.
- Proof. split; [ exact Lt.lt_irrefl | exact Lt.lt_trans ]. Qed.
+ Proof. split; [ exact lt_irrefl | exact lt_trans ]. Qed.
 
  Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) lt.
  Proof. repeat red; intros; subst; auto. Qed.
 
- Lemma le_lteq : forall x y, x <= y <-> x < y \/ x=y.
- Proof. intuition; subst; auto using Lt.le_lt_or_eq. Qed.
-
- Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y).
- Proof.
- intros; unfold compare.
- destruct (nat_compare x y) as [ ]_eqn; constructor.
- apply nat_compare_eq; auto.
- apply nat_compare_Lt_lt; auto.
- apply nat_compare_Gt_gt; auto.
- Qed.
+ Definition le_lteq := le_lt_or_eq_iff.
+ Definition compare_spec := nat_compare_spec.
 
 End Nat_as_OT.
 
-(* Note that [Nat_as_OT] can also be seen as a [UsualOrderedType]
+(** Note that [Nat_as_OT] can also be seen as a [UsualOrderedType]
    and a [OrderedType] (and also as a [DecidableType]). *)