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 | |
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')
-rw-r--r-- | theories/Arith/Compare_dec.v | 4 | ||||
-rw-r--r-- | theories/Init/Datatypes.v | 54 | ||||
-rw-r--r-- | theories/MSets/MSetAVL.v | 2 | ||||
-rw-r--r-- | theories/NArith/BinNat.v | 2 | ||||
-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 | ||||
-rw-r--r-- | theories/PArith/BinPos.v | 2 | ||||
-rw-r--r-- | theories/QArith/QArith_base.v | 2 | ||||
-rw-r--r-- | theories/Reals/ROrderedType.v | 2 | ||||
-rw-r--r-- | theories/Structures/Orders.v | 4 | ||||
-rw-r--r-- | 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 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. |