diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-01-13 09:53:07 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-01-13 09:53:07 +0000 |
commit | 307da4d1fb744bb3c66e5a43acd7702f0ce1b7ac (patch) | |
tree | 1f8ce41f366bf19b777a1934ae0b1eb09be0a9f3 /backend/OrderedOption.v | |
parent | 33a4bcf3695d0ee2793b3bdd12f6ee787d152f36 (diff) | |
download | compcert-307da4d1fb744bb3c66e5a43acd7702f0ce1b7ac.tar.gz compcert-307da4d1fb744bb3c66e5a43acd7702f0ce1b7ac.zip |
Backtracking on commit 1220v1.6
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1228 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/OrderedOption.v')
-rwxr-xr-x | backend/OrderedOption.v | 96 |
1 files changed, 0 insertions, 96 deletions
diff --git a/backend/OrderedOption.v b/backend/OrderedOption.v deleted file mode 100755 index b2cebe2b..00000000 --- a/backend/OrderedOption.v +++ /dev/null @@ -1,96 +0,0 @@ -Require Import FSets. - -(* Definition of options types as ordered types, - in order to define weights *) - -Module OrderedOpt (O : OrderedType) <: OrderedType. - -Definition t := option O.t. - -Inductive eq_ : t -> t -> Prop := -|None_eq : eq_ None None -|Some_eq : forall x y, O.eq x y -> eq_ (Some x) (Some y). - -Definition eq := eq_. - -Inductive lt_ : t -> t -> Prop := -|None_lt : forall o : O.t, lt_ None (Some o) -|Some_lt : forall o o', O.lt o o' -> lt_ (Some o) (Some o'). - -Definition lt := lt_. - -Lemma eq_refl : forall x : t, eq x x. - -Proof. -unfold eq;intro x;destruct x;constructor;apply O.eq_refl. -Qed. - -Lemma eq_sym : forall x y : t, eq x y -> eq y x. - -Proof. -unfold eq;intros x y H;destruct x;destruct y. -constructor;inversion H;apply O.eq_sym;assumption. -inversion H. -inversion H. -assumption. -Qed. - -Lemma eq_trans : forall x y z, eq x y -> eq y z -> eq x z. - -Proof. -unfold eq;intros x y z H H0. -inversion H;inversion H0. -constructor. -rewrite <-H2 in H4;inversion H4. -rewrite <-H3 in H4;inversion H4. -rewrite <-H3 in H5;inversion H5;subst. -constructor;apply (O.eq_trans H1 H4). -Qed. - -Lemma lt_trans : forall x y z, lt x y -> lt y z -> lt x z. - -Proof. -unfold lt;intros x y z H H0. -inversion H;inversion H0;constructor. -rewrite <-H3 in H4;inversion H4. -rewrite <-H3 in H5;inversion H5. -subst. -apply (O.lt_trans H1 H4). -Qed. - -Lemma lt_not_eq : forall x y, lt x y -> ~eq x y. - -Proof. -intros x y H. -unfold eq;intro Heq. -inversion H;inversion Heq. -rewrite <-H3 in H1;inversion H1. -rewrite <-H0 in H3;inversion H3. -rewrite <-H1 in H3;inversion H3. -subst;inversion H4;inversion H5;subst. -elim (O.lt_not_eq H0 H3). -Qed. - -Lemma compare : forall x y : t, Compare lt eq x y. - -Proof. -intros x y. -destruct x;destruct y. -destruct (O.compare t0 t1); -[apply LT;unfold lt|apply EQ;unfold eq|apply GT;unfold lt];constructor;assumption. -apply GT;unfold lt;constructor. -apply LT;unfold lt;constructor. -apply EQ;unfold eq;constructor. -Qed. - -Lemma eq_dec : forall x y, {eq x y}+{~eq x y}. - -Proof. -intros x y. -destruct (compare x y). -right. apply lt_not_eq. assumption. -left. assumption. -right. intro H. generalize (eq_sym _ _ H). intro H0. elim (lt_not_eq _ _ l H0). -Qed. - -End OrderedOpt.
\ No newline at end of file |