From ce5a3cd114d3a570cdd569e65f1a2a71f81c39f4 Mon Sep 17 00:00:00 2001
From: letouzey
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 +-
 theories/Init/Datatypes.v                       | 54 ++++++++++++++++---------
 theories/MSets/MSetAVL.v                        |  2 +-
 theories/NArith/BinNat.v                        |  2 +-
 theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v |  2 +-
 theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v |  2 +-
 theories/Numbers/Rational/SpecViaQ/QSig.v       |  2 +-
 theories/PArith/BinPos.v                        |  2 +-
 theories/QArith/QArith_base.v                   |  2 +-
 theories/Reals/ROrderedType.v                   |  2 +-
 theories/Structures/Orders.v                    |  4 +-
 theories/ZArith/Zcompare.v                      |  2 +-
 12 files changed, 47 insertions(+), 33 deletions(-)

diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 53a959d711..360d760a54 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.
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 184839eff6..9895bd30bc 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -232,33 +232,47 @@ Proof.
   split; intros; apply CompOpp_inj; rewrite CompOpp_involutive; auto.
 Qed.
 
-(** The [CompSpec] inductive will be used to relate a [compare] function
-    (returning a comparison answer) and some equality and order predicates.
-    Interest: [CompSpec] behave nicely with [case] and [destruct]. *)
-
-Inductive CompSpec {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Prop :=
- | CompEq : eq x y -> CompSpec eq lt x y Eq
- | CompLt : lt x y -> CompSpec eq lt x y Lt
- | CompGt : lt y x -> CompSpec eq lt x y Gt.
-Hint Constructors CompSpec.
-
-(** For having clean interfaces after extraction, [CompSpec] is declared
+(** The [CompareSpec] inductive relates a [comparison] value with three
+   propositions, one for each possible case. Typically, it can be used to
+   specify a comparison function via some equality and order predicates.
+   Interest: [CompareSpec] behave nicely with [case] and [destruct]. *)
+
+Inductive CompareSpec (Peq Plt Pgt : Prop) : comparison -> Prop :=
+ | CompEq : Peq -> CompareSpec Peq Plt Pgt Eq
+ | CompLt : Plt -> CompareSpec Peq Plt Pgt Lt
+ | CompGt : Pgt -> CompareSpec Peq Plt Pgt Gt.
+Hint Constructors CompareSpec.
+
+(** For having clean interfaces after extraction, [CompareSpec] is declared
     in Prop. For some situations, it is nonetheless useful to have a
-    version in Type. Interestingly, these two versions are equivalent.
-*)
+    version in Type. Interestingly, these two versions are equivalent. *)
 
-Inductive CompSpecT {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Type :=
- | CompEqT : eq x y -> CompSpecT eq lt x y Eq
- | CompLtT : lt x y -> CompSpecT eq lt x y Lt
- | CompGtT : lt y x -> CompSpecT eq lt x y Gt.
-Hint Constructors CompSpecT.
+Inductive CompareSpecT (Peq Plt Pgt : Prop) : comparison -> Type :=
+ | CompEqT : Peq -> CompareSpecT Peq Plt Pgt Eq
+ | CompLtT : Plt -> CompareSpecT Peq Plt Pgt Lt
+ | CompGtT : Pgt -> CompareSpecT Peq Plt Pgt Gt.
+Hint Constructors CompareSpecT.
 
-Lemma CompSpec2Type : forall A (eq lt:A->A->Prop) x y c,
- CompSpec eq lt x y c -> CompSpecT eq lt x y c.
+Lemma CompareSpec2Type : forall Peq Plt Pgt c,
+ CompareSpec Peq Plt Pgt c -> CompareSpecT Peq Plt Pgt c.
 Proof.
  destruct c; intros H; constructor; inversion_clear H; auto.
 Defined.
 
+(** As an alternate formulation, one may also directly refer to predicates
+ [eq] and [lt] for specifying a comparison, rather that fully-applied
+ propositions. This [CompSpec] is now a particular case of [CompareSpec]. *)
+
+Definition CompSpec {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Prop :=
+ CompareSpec (eq x y) (lt x y) (lt y x).
+Definition CompSpecT {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Type :=
+ CompareSpecT (eq x y) (lt x y) (lt y x).
+Hint Unfold CompSpec CompSpecT.
+
+Lemma CompSpec2Type : forall A (eq lt:A->A->Prop) x y c,
+ CompSpec eq lt x y c -> CompSpecT eq lt x y c.
+Proof. intros. apply CompareSpec2Type; assumption. Qed.
+
 (** Identity *)
 
 Definition ID := forall A:Type, A -> A.
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index 5d17dd3f1d..db6616b34b 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -1767,7 +1767,7 @@ Lemma compare_more_Cmp : forall x1 cont x2 r2 e2 l,
    Cmp (compare_more x1 cont (More x2 r2 e2)) (x1::l)
       (flatten_e (More x2 r2 e2)).
 Proof.
- simpl; intros; elim_compare x1 x2; simpl; auto.
+ simpl; intros; elim_compare x1 x2; simpl; red; auto.
 Qed.
 
 Lemma compare_cont_Cmp : forall s1 cont e2 l,
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 686a0692ce..3f256b40f6 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -547,7 +547,7 @@ Proof.
   intuition; now try discriminate V.
 Qed.
 
-Lemma Ncompare_spec : forall x y, CompSpec eq Nlt x y (Ncompare x y).
+Lemma Ncompare_spec : forall x y, CompareSpec (x=y) (x<y) (y<x) (x ?= y).
 Proof.
 intros.
 destruct (Ncompare x y) as [ ]_eqn; constructor; auto.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index cf38adf3a0..fe0e6567e2 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 cef8c38198..bff52fb37f 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 a4f0dbce1b..29e1e795a0 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] *)
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 64e32c560a..4570fde726 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1015,7 +1015,7 @@ Proof.
   symmetry; apply Pcompare_antisym.
 Qed.
 
-Lemma Pcompare_spec : forall p q, CompSpec eq Plt p q ((p ?= q) Eq).
+Lemma Pcompare_spec : forall p q, CompareSpec (p=q) (p<q) (q<p) ((p ?= q) Eq).
 Proof.
   intros. destruct ((p ?= q) Eq) as [ ]_eqn; constructor.
   apply Pcompare_Eq_eq; auto.
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index fe37fccb85..a32ccbc4b2 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -97,7 +97,7 @@ Proof.
  unfold "?=". intros. apply Zcompare_antisym.
 Qed.
 
-Lemma Qcompare_spec : forall x y, CompSpec Qeq Qlt x y (x ?= y).
+Lemma Qcompare_spec : forall x y, CompareSpec (x==y) (x<y) (y<x) (x ?= y).
 Proof.
  intros.
  destruct (x ?= y) as [ ]_eqn:H; constructor; auto.
diff --git a/theories/Reals/ROrderedType.v b/theories/Reals/ROrderedType.v
index 07f7f863c6..0a8d89c77f 100644
--- a/theories/Reals/ROrderedType.v
+++ b/theories/Reals/ROrderedType.v
@@ -55,7 +55,7 @@ Definition Rcompare x y :=
   | inright _ => Gt
  end.
 
-Lemma Rcompare_spec : forall x y, CompSpec eq Rlt x y (Rcompare x y).
+Lemma Rcompare_spec : forall x y, CompareSpec (x=y) (x<y) (y<x) (Rcompare x y).
 Proof.
  intros. unfold Rcompare.
  destruct total_order_T as [[H|H]|H]; auto.
diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v
index f83e77ed84..99dfb19d52 100644
--- a/theories/Structures/Orders.v
+++ b/theories/Structures/Orders.v
@@ -65,9 +65,9 @@ Module Type LeIsLtEq (Import E:EqLtLe').
   Axiom le_lteq : forall x y, x<=y <-> x<y \/ x==y.
 End LeIsLtEq.
 
-Module Type HasCompare (Import E:EqLt).
+Module Type HasCompare (Import E:EqLt').
   Parameter Inline compare : t -> t -> comparison.
-  Axiom compare_spec : forall x y, CompSpec eq lt x y (compare x y).
+  Axiom compare_spec : forall x y, CompareSpec (x==y) (x<y) (y<x) (compare x y).
 End HasCompare.
 
 Module Type StrOrder := EqualityType <+ HasLt <+ IsStrOrder.
diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v
index 10f07a8641..19e46bb2d8 100644
--- a/theories/ZArith/Zcompare.v
+++ b/theories/ZArith/Zcompare.v
@@ -55,7 +55,7 @@ Proof.
  intros [|x|x] [|y|y]; simpl; try easy; f_equal; apply Pcompare_antisym.
 Qed.
 
-Lemma Zcompare_spec : forall n m, CompSpec eq Zlt n m (n ?= m).
+Lemma Zcompare_spec : forall n m, CompareSpec (n=m) (n<m) (m<n) (n ?= m).
 Proof.
  intros.
  destruct (n?=m) as [ ]_eqn:H; constructor; trivial.
-- 
cgit v1.2.3