diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-06-05 13:39:59 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-06-05 13:39:59 +0000 |
| commit | 615fb53c13f2407a0b6b470bbdf8e468fc4a1d78 (patch) | |
| tree | ec5f45b6546e19519f59b1ee0f42955616ca1b98 /lib/Ordered.v | |
| parent | d1cdc0496d7d52e3ab91554dbf53fcc0e7f244eb (diff) | |
| download | compcert-kvx-615fb53c13f2407a0b6b470bbdf8e468fc4a1d78.tar.gz compcert-kvx-615fb53c13f2407a0b6b470bbdf8e468fc4a1d78.zip | |
Adapted to work with Coq 8.2-1v1.4.1
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1076 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
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. |