diff options
Diffstat (limited to 'theories/FSets/OrderedTypeEx.v')
-rw-r--r-- | theories/FSets/OrderedTypeEx.v | 24 |
1 files changed, 23 insertions, 1 deletions
diff --git a/theories/FSets/OrderedTypeEx.v b/theories/FSets/OrderedTypeEx.v index 03171396..03e3ab83 100644 --- a/theories/FSets/OrderedTypeEx.v +++ b/theories/FSets/OrderedTypeEx.v @@ -11,7 +11,7 @@ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud * 91405 Orsay, France *) -(* $Id: OrderedTypeEx.v 10739 2008-04-01 14:45:20Z herbelin $ *) +(* $Id: OrderedTypeEx.v 11699 2008-12-18 11:49:08Z letouzey $ *) Require Import OrderedType. Require Import ZArith. @@ -34,6 +34,7 @@ Module Type UsualOrderedType. Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y. Parameter compare : forall x y : t, Compare lt eq x y. + Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }. End UsualOrderedType. (** a [UsualOrderedType] is in particular an [OrderedType]. *) @@ -68,6 +69,8 @@ Module Nat_as_OT <: UsualOrderedType. intro; constructor 3; auto. Defined. + Definition eq_dec := eq_nat_dec. + End Nat_as_OT. @@ -99,6 +102,8 @@ Module Z_as_OT <: UsualOrderedType. apply GT; unfold lt, Zlt; rewrite <- Zcompare_Gt_Lt_antisym; auto. Defined. + Definition eq_dec := Z_eq_dec. + End Z_as_OT. (** [positive] is an ordered type with respect to the usual order on natural numbers. *) @@ -140,6 +145,11 @@ Module Positive_as_OT <: UsualOrderedType. rewrite <- Pcompare_antisym; rewrite H; auto. Defined. + Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }. + Proof. + intros; unfold eq; decide equality. + Defined. + End Positive_as_OT. @@ -183,6 +193,11 @@ Module N_as_OT <: UsualOrderedType. destruct (Nleb x y); intuition. Defined. + Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }. + Proof. + intros. unfold eq. decide equality. apply Positive_as_OT.eq_dec. + Defined. + End N_as_OT. @@ -243,5 +258,12 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. apply GT; unfold lt; auto. Defined. + Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}. + Proof. + intros; elim (compare x y); intro H; [ right | left | right ]; auto. + auto using lt_not_eq. + assert (~ eq y x); auto using lt_not_eq, eq_sym. + Defined. + End PairOrderedType. |