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

diff --git a/theories/ZArith/ZOrderedType.v b/theories/ZArith/ZOrderedType.v
index 6e30e0bf8b..34456dcf9c 100644
--- a/theories/ZArith/ZOrderedType.v
+++ b/theories/ZArith/ZOrderedType.v
@@ -39,24 +39,12 @@ Module Z_as_OT <: OrderedTypeFull.
  Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) Zlt.
  Proof. repeat red; intros; subst; auto. Qed.
 
- Lemma le_lteq : forall x y, x <= y <-> x < y \/ x=y.
- Proof.
- unfold le, lt, Zle, Zlt. intros.
- rewrite <- Zcompare_Eq_iff_eq.
- destruct (x ?= y); intuition; discriminate.
- Qed.
-
- Lemma compare_spec : forall x y, Cmp eq lt x y (Zcompare x y).
- Proof.
- intros; unfold compare.
- destruct (Zcompare x y) as [ ]_eqn; constructor; auto.
- apply Zcompare_Eq_eq; auto.
- apply Zgt_lt; auto.
- Qed.
+ Definition le_lteq := Zle_lt_or_eq_iff.
+ Definition compare_spec := Zcompare_spec.
 
 End Z_as_OT.
 
-(* Note that [Z_as_OT] can also be seen as a [UsualOrderedType]
+(** Note that [Z_as_OT] can also be seen as a [UsualOrderedType]
    and a [OrderedType] (and also as a [DecidableType]). *)
 
 
diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v
index 2515b7f7b2..3e611d5437 100644
--- a/theories/ZArith/Zcompare.v
+++ b/theories/ZArith/Zcompare.v
@@ -72,6 +72,15 @@ Proof.
   intros; f_equal; auto.
 Qed.
 
+Lemma Zcompare_spec : forall n m, CompSpec eq Zlt n m (n ?= m).
+Proof.
+  intros.
+  destruct (n?=m) as [ ]_eqn:H; constructor; auto.
+  apply Zcompare_Eq_eq; auto.
+  red; rewrite <- Zcompare_antisym, H; auto.
+Qed.
+
+
 (** * Transitivity of comparison *)
 
 Lemma Zcompare_Lt_trans :
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 70cbe0f28f..0db71e68d0 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -257,6 +257,13 @@ Proof.
       | absurd (n > m); [ apply Zle_not_gt | idtac ]; assumption ].
 Qed.
 
+Lemma Zle_lt_or_eq_iff : forall n m, n <= m <-> n < m \/ n = m.
+Proof.
+  unfold Zle, Zlt. intros.
+  generalize (Zcompare_Eq_iff_eq n m).
+  destruct (n ?= m); intuition; discriminate.
+Qed.
+
 (** Dichotomy *)
 
 Lemma Zle_or_lt : forall n m:Z, n <= m \/ m < n.