diff options
Diffstat (limited to 'lib/Ordered.v')
-rw-r--r-- | lib/Ordered.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/lib/Ordered.v b/lib/Ordered.v index 4b1f4e0f..eddc3721 100644 --- a/lib/Ordered.v +++ b/lib/Ordered.v @@ -45,6 +45,8 @@ Proof. assert (Zpos x <> Zpos y). congruence. omega. Qed. +Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := peq. + End OrderedPositive. (** Indexed types (those that inject into [positive]) are ordered. *) @@ -81,6 +83,13 @@ Proof. apply GT. exact l. Qed. +Lemma eq_dec : forall x y, { eq x y } + { ~ eq x y }. +Proof. + intros. case (peq (A.index x) (A.index y)); intros. + left. apply A.index_inj; auto. + right; red; unfold eq; intros; subst. congruence. +Qed. + End OrderedIndexed. (** The product of two ordered types is ordered. *) @@ -164,5 +173,15 @@ Proof. apply GT. red. left. auto. Qed. +Lemma eq_dec : forall x y, { eq x y } + { ~ eq x y }. +Proof. + unfold eq; intros. + case (A.eq_dec (fst x) (fst y)); intros. + case (B.eq_dec (snd x) (snd y)); intros. + left; auto. + right; intuition. + right; intuition. +Qed. + End OrderedPair. |