aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-02-12 16:03:55 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-02-12 16:03:55 +0000
commit1826065d7603d0993b78829856a5725f253c782d (patch)
tree67f82826fee80d3124f8a2e670f3c75310d77ff6
parent08528250663d850bc56c48dfaab9f5d71e1e7dee (diff)
CompSpecType, a clone of CompSpec but in Type instead of Prop
In interfaces fields like compare_spec, a CompSpec is prefered to get nice extraction, but then no "destruct (compare_spec .. ..)" is possible in a Type context. Now you can say there "destruct (CompSpec2Type (compare_spec ... ...))" This translate to the Type variant, and make the analysis on it (which is equivalent to analysing the comparison directly). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12753 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--theories/FSets/FSetCompat.v6
-rw-r--r--theories/Init/Datatypes.v18
-rw-r--r--theories/MSets/MSetInterface.v5
-rw-r--r--theories/MSets/MSetList.v7
-rw-r--r--theories/Structures/GenericMinMax.v32
-rw-r--r--theories/Structures/OrdersAlt.v5
-rw-r--r--theories/Structures/OrdersFacts.v4
7 files changed, 43 insertions, 34 deletions
diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v
index 971daa215..439f0e528 100644
--- a/theories/FSets/FSetCompat.v
+++ b/theories/FSets/FSetCompat.v
@@ -209,10 +209,8 @@ Module Backport_Sets
Qed.
Definition compare : forall s s', Compare lt eq s s'.
Proof.
- intros s s'.
- assert (H := M.compare_spec s s').
- destruct (M.compare s s'); [ apply EQ | apply LT | apply GT ];
- inversion H; auto.
+ intros s s'; destruct (CompSpec2Type (M.compare_spec s s'));
+ [ apply EQ | apply LT | apply GT ]; auto.
Defined.
End Backport_Sets.
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index fc64f081b..4782194a3 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -223,7 +223,7 @@ 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 [destruct]. *)
+ 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
@@ -231,6 +231,22 @@ Inductive CompSpec {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Prop :=
| CompGt : lt y x -> CompSpec eq lt x y Gt.
Hint Constructors CompSpec.
+(** For having clean interfaces after extraction, [CompSpec] is declared
+ in Prop. For some situations, it is nonetheless useful to have a
+ 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.
+
+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.
+ destruct c; intros H; constructor; inversion_clear H; auto.
+Qed.
(** Identity *)
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index ae26fa7ed..10776a590 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -612,10 +612,7 @@ Module Raw2SetsOn (O:OrderedType)(M:RawSets O) <: SetsOn O.
Variable x y : elt.
Lemma compare_spec : CompSpec eq lt s s' (compare s s').
- Proof.
- assert (H:=@M.compare_spec s s' _ _).
- unfold compare; destruct M.compare; inversion_clear H; auto.
- Qed.
+ Proof. unfold compare; destruct (@M.compare_spec s s' _ _); auto. Qed.
(** Additional specification of [elements] *)
Lemma elements_spec2 : sort O.lt (elements s).
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index c29742332..d46803d75 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -805,10 +805,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
CompSpec eq lt s s' (compare s s').
Proof.
intros s s' Hs Hs'.
- generalize (compare_spec_aux s s').
- destruct (compare s s'); inversion_clear 1; auto.
- apply CompLt. exists s, s'; repeat split; auto using @ok.
- apply CompGt. exists s', s; repeat split; auto using @ok.
+ destruct (compare_spec_aux s s'); constructor; auto.
+ exists s, s'; repeat split; auto using @ok.
+ exists s', s; repeat split; auto using @ok.
Qed.
End MakeRaw.
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index a62d96aa0..68f201897 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -51,26 +51,26 @@ Module GenericMinMax (Import O:OrderedTypeFull') <: HasMinMax O.
Lemma max_l : forall x y, y<=x -> max x y == x.
Proof.
- intros. unfold max, gmax. destruct (compare_spec x y); auto with relations.
- elim (ge_not_lt x y); auto.
+ intros. unfold max, gmax. case compare_spec; auto with relations.
+ intros; elim (ge_not_lt x y); auto.
Qed.
Lemma max_r : forall x y, x<=y -> max x y == y.
Proof.
- intros. unfold max, gmax. destruct (compare_spec x y); auto with relations.
- elim (ge_not_lt y x); auto.
+ intros. unfold max, gmax. case compare_spec; auto with relations.
+ intros; elim (ge_not_lt y x); auto.
Qed.
Lemma min_l : forall x y, x<=y -> min x y == x.
Proof.
- intros. unfold min, gmin. destruct (compare_spec x y); auto with relations.
- elim (ge_not_lt y x); auto.
+ intros. unfold min, gmin. case compare_spec; auto with relations.
+ intros; elim (ge_not_lt y x); auto.
Qed.
Lemma min_r : forall x y, y<=x -> min x y == y.
Proof.
- intros. unfold min, gmin. destruct (compare_spec x y); auto with relations.
- elim (ge_not_lt x y); auto.
+ intros. unfold min, gmin. case compare_spec; auto with relations.
+ intros; elim (ge_not_lt x y); auto.
Qed.
End GenericMinMax.
@@ -483,12 +483,12 @@ Lemma max_case_strong : forall n m (P:t -> Type),
(m<=n -> P n) -> (n<=m -> P m) -> P (max n m).
Proof.
intros n m P Compat Hl Hr.
-assert (H:=compare_spec n m). destruct (compare n m).
-assert (n<=m) by (inversion H; rewrite le_lteq; auto).
+destruct (CompSpec2Type (compare_spec n m)) as [EQ|LT|GT].
+assert (n<=m) by (rewrite le_lteq; auto).
apply (Compat m), Hr; auto. symmetry; apply max_r; auto.
-assert (n<=m) by (inversion H; rewrite le_lteq; auto).
+assert (n<=m) by (rewrite le_lteq; auto).
apply (Compat m), Hr; auto. symmetry; apply max_r; auto.
-assert (m<=n) by (inversion H; rewrite le_lteq; auto).
+assert (m<=n) by (rewrite le_lteq; auto).
apply (Compat n), Hl; auto. symmetry; apply max_l; auto.
Defined.
@@ -512,12 +512,12 @@ Lemma min_case_strong : forall n m (P:O.t -> Type),
(n<=m -> P n) -> (m<=n -> P m) -> P (min n m).
Proof.
intros n m P Compat Hl Hr.
-assert (H:=compare_spec n m). destruct (compare n m).
-assert (n<=m) by (inversion H; rewrite le_lteq; auto).
+destruct (CompSpec2Type (compare_spec n m)) as [EQ|LT|GT].
+assert (n<=m) by (rewrite le_lteq; auto).
apply (Compat n), Hl; auto. symmetry; apply min_l; auto.
-assert (n<=m) by (inversion H; rewrite le_lteq; auto).
+assert (n<=m) by (rewrite le_lteq; auto).
apply (Compat n), Hl; auto. symmetry; apply min_l; auto.
-assert (m<=n) by (inversion H; rewrite le_lteq; auto).
+assert (m<=n) by (rewrite le_lteq; auto).
apply (Compat m), Hr; auto. symmetry; apply min_r; auto.
Defined.
diff --git a/theories/Structures/OrdersAlt.v b/theories/Structures/OrdersAlt.v
index 261e75e1c..d86b02a15 100644
--- a/theories/Structures/OrdersAlt.v
+++ b/theories/Structures/OrdersAlt.v
@@ -101,9 +101,8 @@ Module Backport_OT (O:OrderedType) <: OrderedTypeOrig.
Definition compare : forall x y, Compare lt eq x y.
Proof.
- intros. assert (H:=O.compare_spec x y).
- destruct (O.compare x y); [apply EQ|apply LT|apply GT];
- inversion H; auto.
+ intros x y; destruct (CompSpec2Type (O.compare_spec x y));
+ [apply EQ|apply LT|apply GT]; auto.
Defined.
End Backport_OT.
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index a318ecb85..a28b79776 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -134,8 +134,8 @@ Module OrderedTypeFacts (Import O: OrderedType').
Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}.
Proof.
- intros; assert (H:=compare_spec x y); destruct (compare x y);
- [ right | left | right ]; inversion_clear H; order.
+ intros x y; destruct (CompSpec2Type (compare_spec x y));
+ [ right | left | right ]; order.
Defined.
Definition eqb x y : bool := if eq_dec x y then true else false.