From ce5a3cd114d3a570cdd569e65f1a2a71f81c39f4 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 17 Mar 2011 21:46:43 +0000
Subject: CompareSpec: a slight generalization/reformulation of CompSpec

 CompareSpec expects 3 propositions Peq Plt Pgt instead of 2 relations
 eq lt and 2 points x y. For the moment, we still always use (Peq=eq x y),
 (Plt=lt x y) (Pgt=lt y x), but this may not be always the case,
 especially for Pgt. The former CompSpec is now defined in term of
 CompareSpec. Compatibility is preserved (except maybe a rare unfold
 or red to break the CompSpec definition).

 Typically, CompareSpec looks nicer when we have infix notations, e.g.

  forall x y, CompareSpec (x=y) (x<y) (y<x) (x?=x)

 while CompSpec is shorter when we directly refer to predicates:

  forall x y, CompSpec eq lt x y (compare x y)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13914 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Arith/Compare_dec.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories/Arith')

diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 53a959d71..360d760a5 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -198,7 +198,8 @@ Proof.
    apply -> nat_compare_lt; auto.
 Qed.
 
-Lemma nat_compare_spec : forall x y, CompSpec eq lt x y (nat_compare x y).
+Lemma nat_compare_spec :
+  forall x y, CompareSpec (x=y) (x<y) (y<x) (nat_compare x y).
 Proof.
  intros.
  destruct (nat_compare x y) as [ ]_eqn; constructor.
@@ -207,7 +208,6 @@ Proof.
  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.
-- 
cgit v1.2.3