aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--theories/Arith/Compare_dec.v4
-rw-r--r--theories/Init/Datatypes.v54
-rw-r--r--theories/MSets/MSetAVL.v2
-rw-r--r--theories/NArith/BinNat.v2
-rw-r--r--theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v2
-rw-r--r--theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v2
-rw-r--r--theories/Numbers/Rational/SpecViaQ/QSig.v2
-rw-r--r--theories/PArith/BinPos.v2
-rw-r--r--theories/QArith/QArith_base.v2
-rw-r--r--theories/Reals/ROrderedType.v2
-rw-r--r--theories/Structures/Orders.v4
-rw-r--r--theories/ZArith/Zcompare.v2
12 files changed, 47 insertions, 33 deletions
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.
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 184839eff..9895bd30b 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 5d17dd3f1..db6616b34 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 686a0692c..3f256b40f 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 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] *)
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 64e32c560..4570fde72 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 fe37fccb8..a32ccbc4b 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 07f7f863c..0a8d89c77 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 f83e77ed8..99dfb19d5 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 10f07a864..19e46bb2d 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 20:37:32 +0000