diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-17 21:46:43 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-17 21:46:43 +0000 |
commit | ce5a3cd114d3a570cdd569e65f1a2a71f81c39f4 (patch) | |
tree | cdfc5975af04c229f6187fd88f2a83a7c35e8ebe /theories/Numbers | |
parent | 7cc3c1b16771a7e8230fb0d1f74d63ade6f393a7 (diff) |
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
Diffstat (limited to 'theories/Numbers')
-rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Rational/SpecViaQ/QSig.v | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index cf38adf3a..fe0e6567e 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -138,7 +138,7 @@ Qed. (** Order *) -Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). +Lemma compare_spec : forall x y, CompareSpec (x==y) (x<y) (y<x) (compare x y). Proof. intros. zify. destruct (Zcompare_spec [x] [y]); auto. Qed. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index cef8c3819..bff52fb37 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -126,7 +126,7 @@ Qed. (** Order *) -Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). +Lemma compare_spec : forall x y, CompareSpec (x==y) (x<y) (y<x) (compare x y). Proof. intros. zify. destruct (Zcompare_spec [x] [y]); auto. Qed. diff --git a/theories/Numbers/Rational/SpecViaQ/QSig.v b/theories/Numbers/Rational/SpecViaQ/QSig.v index a4f0dbce1..29e1e795a 100644 --- a/theories/Numbers/Rational/SpecViaQ/QSig.v +++ b/theories/Numbers/Rational/SpecViaQ/QSig.v @@ -135,7 +135,7 @@ Program Instance power_wd : Proper (eq==>Logic.eq==>eq) power. (** Let's implement [HasCompare] *) -Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). +Lemma compare_spec : forall x y, CompareSpec (x==y) (x<y) (y<x) (compare x y). Proof. intros. qify. destruct (Qcompare_spec [x] [y]); auto. Qed. (** Let's implement [TotalOrder] *) |