diff options
Diffstat (limited to 'theories/Structures/OrderedType.v')
| -rw-r--r-- | theories/Structures/OrderedType.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index 75578195..cc8c2261 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -49,7 +49,7 @@ Module Type OrderedType. Include MiniOrderedType. (** A [eq_dec] can be deduced from [compare] below. But adding this - redundant field allows to see an OrderedType as a DecidableType. *) + redundant field allows seeing an OrderedType as a DecidableType. *) Parameter eq_dec : forall x y, { eq x y } + { ~ eq x y }. End OrderedType. @@ -85,16 +85,16 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z. Proof. - intros; destruct (compare x z); auto. + intros; destruct (compare x z) as [Hlt|Heq|Hlt]; auto. elim (lt_not_eq H); apply eq_trans with z; auto. - elim (lt_not_eq (lt_trans l H)); auto. + elim (lt_not_eq (lt_trans Hlt H)); auto. Qed. Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z. Proof. - intros; destruct (compare x z); auto. + intros; destruct (compare x z) as [Hlt|Heq|Hlt]; auto. elim (lt_not_eq H0); apply eq_trans with x; auto. - elim (lt_not_eq (lt_trans H0 l)); auto. + elim (lt_not_eq (lt_trans H0 Hlt)); auto. Qed. Instance lt_compat : Proper (eq==>eq==>iff) lt. @@ -225,7 +225,7 @@ Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l. Proof. exact (InfA_ltA lt_strorder). Qed. Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l. -Proof. exact (InfA_eqA eq_equiv lt_strorder lt_compat). Qed. +Proof. exact (InfA_eqA eq_equiv lt_compat). Qed. Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x. Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed. @@ -398,7 +398,7 @@ Module KeyOrderedType(O:OrderedType). Qed. Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l. - Proof. exact (InfA_eqA eqk_equiv ltk_strorder ltk_compat). Qed. + Proof. exact (InfA_eqA eqk_equiv ltk_compat). Qed. Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l. Proof. exact (InfA_ltA ltk_strorder). Qed. |