diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-12 16:03:55 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-12 16:03:55 +0000 |
commit | 1826065d7603d0993b78829856a5725f253c782d (patch) | |
tree | 67f82826fee80d3124f8a2e670f3c75310d77ff6 /theories/Structures | |
parent | 08528250663d850bc56c48dfaab9f5d71e1e7dee (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
Diffstat (limited to 'theories/Structures')
-rw-r--r-- | theories/Structures/GenericMinMax.v | 32 | ||||
-rw-r--r-- | theories/Structures/OrdersAlt.v | 5 | ||||
-rw-r--r-- | theories/Structures/OrdersFacts.v | 4 |
3 files changed, 20 insertions, 21 deletions
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. |