diff options
Diffstat (limited to 'theories/Structures/OrdersAlt.v')
| -rw-r--r-- | theories/Structures/OrdersAlt.v | 242 |
1 files changed, 242 insertions, 0 deletions
diff --git a/theories/Structures/OrdersAlt.v b/theories/Structures/OrdersAlt.v new file mode 100644 index 00000000..d86b02a1 --- /dev/null +++ b/theories/Structures/OrdersAlt.v @@ -0,0 +1,242 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* Finite sets library. + * Authors: Pierre Letouzey and Jean-Christophe Filliâtre + * Institution: LRI, CNRS UMR 8623 - Université Paris Sud + * 91405 Orsay, France *) + +(* $Id$ *) + +Require Import OrderedType Orders. +Set Implicit Arguments. + +(** * Some alternative (but equivalent) presentations for an Ordered Type + inferface. *) + +(** ** The original interface *) + +Module Type OrderedTypeOrig := OrderedType.OrderedType. + +(** ** An interface based on compare *) + +Module Type OrderedTypeAlt. + + Parameter t : Type. + + Parameter compare : t -> t -> comparison. + + Infix "?=" := compare (at level 70, no associativity). + + Parameter compare_sym : + forall x y, (y?=x) = CompOpp (x?=y). + Parameter compare_trans : + forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c. + +End OrderedTypeAlt. + +(** ** From OrderedTypeOrig to OrderedType. *) + +Module Update_OT (O:OrderedTypeOrig) <: OrderedType. + + Include Update_DT O. (* Provides : t eq eq_equiv eq_dec *) + + Definition lt := O.lt. + + Instance lt_strorder : StrictOrder lt. + Proof. + split. + intros x Hx. apply (O.lt_not_eq Hx); auto with *. + exact O.lt_trans. + Qed. + + Instance lt_compat : Proper (eq==>eq==>iff) lt. + Proof. + apply proper_sym_impl_iff_2; auto with *. + intros x x' Hx y y' Hy H. + assert (H0 : lt x' y). + destruct (O.compare x' y) as [H'|H'|H']; auto. + elim (O.lt_not_eq H). transitivity x'; auto with *. + elim (O.lt_not_eq (O.lt_trans H H')); auto. + destruct (O.compare x' y') as [H'|H'|H']; auto. + elim (O.lt_not_eq H). + transitivity x'; auto with *. transitivity y'; auto with *. + elim (O.lt_not_eq (O.lt_trans H' H0)); auto with *. + Qed. + + Definition compare x y := + match O.compare x y with + | EQ _ => Eq + | LT _ => Lt + | GT _ => Gt + end. + + Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). + Proof. + intros; unfold compare; destruct O.compare; auto. + Qed. + +End Update_OT. + +(** ** From OrderedType to OrderedTypeOrig. *) + +Module Backport_OT (O:OrderedType) <: OrderedTypeOrig. + + Include Backport_DT O. (* Provides : t eq eq_refl eq_sym eq_trans eq_dec *) + + Definition lt := O.lt. + + Lemma lt_not_eq : forall x y, lt x y -> ~eq x y. + Proof. + intros x y L E; rewrite E in L. apply (StrictOrder_Irreflexive y); auto. + Qed. + + Lemma lt_trans : Transitive lt. + Proof. apply O.lt_strorder. Qed. + + Definition compare : forall x y, Compare lt eq x y. + Proof. + intros x y; destruct (CompSpec2Type (O.compare_spec x y)); + [apply EQ|apply LT|apply GT]; auto. + Defined. + +End Backport_OT. + + +(** ** From OrderedTypeAlt to OrderedType. *) + +Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType. + + Definition t := t. + + Definition eq x y := (x?=y) = Eq. + Definition lt x y := (x?=y) = Lt. + + Instance eq_equiv : Equivalence eq. + Proof. + split; red. + (* refl *) + unfold eq; intros x. + assert (H:=compare_sym x x). + destruct (x ?= x); simpl in *; auto; discriminate. + (* sym *) + unfold eq; intros x y H. + rewrite compare_sym, H; simpl; auto. + (* trans *) + apply compare_trans. + Qed. + + Instance lt_strorder : StrictOrder lt. + Proof. + split; repeat red; unfold lt; try apply compare_trans. + intros x H. + assert (eq x x) by reflexivity. + unfold eq in *; congruence. + Qed. + + Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z. + Proof. + unfold lt, eq; intros x y z Hxy Hyz. + destruct (compare x z) as [ ]_eqn:Hxz; auto. + rewrite compare_sym, CompOpp_iff in Hyz. simpl in Hyz. + rewrite (compare_trans Hxz Hyz) in Hxy; discriminate. + rewrite compare_sym, CompOpp_iff in Hxy. simpl in Hxy. + rewrite (compare_trans Hxy Hxz) in Hyz; discriminate. + Qed. + + Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z. + Proof. + unfold lt, eq; intros x y z Hxy Hyz. + destruct (compare x z) as [ ]_eqn:Hxz; auto. + rewrite compare_sym, CompOpp_iff in Hxy. simpl in Hxy. + rewrite (compare_trans Hxy Hxz) in Hyz; discriminate. + rewrite compare_sym, CompOpp_iff in Hyz. simpl in Hyz. + rewrite (compare_trans Hxz Hyz) in Hxy; discriminate. + Qed. + + Instance lt_compat : Proper (eq==>eq==>iff) lt. + Proof. + apply proper_sym_impl_iff_2; auto with *. + repeat red; intros. + eapply lt_eq; eauto. eapply eq_lt; eauto. symmetry; auto. + Qed. + + Definition compare := O.compare. + + Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). + Proof. + unfold eq, lt, compare; intros. + destruct (O.compare x y) as [ ]_eqn:H; auto. + apply CompGt. + rewrite compare_sym, H; auto. + Qed. + + Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }. + Proof. + intros; unfold eq. + case (x ?= y); [ left | right | right ]; auto; discriminate. + Defined. + +End OT_from_Alt. + +(** From the original presentation to this alternative one. *) + +Module OT_to_Alt (Import O:OrderedType) <: OrderedTypeAlt. + + Definition t := t. + Definition compare := compare. + + Infix "?=" := compare (at level 70, no associativity). + + Lemma compare_sym : + forall x y, (y?=x) = CompOpp (x?=y). + Proof. + intros x y; unfold compare. + destruct (compare_spec x y) as [U|U|U]; + destruct (compare_spec y x) as [V|V|V]; auto. + rewrite U in V. elim (StrictOrder_Irreflexive y); auto. + rewrite U in V. elim (StrictOrder_Irreflexive y); auto. + rewrite V in U. elim (StrictOrder_Irreflexive x); auto. + rewrite V in U. elim (StrictOrder_Irreflexive x); auto. + rewrite V in U. elim (StrictOrder_Irreflexive x); auto. + rewrite V in U. elim (StrictOrder_Irreflexive y); auto. + Qed. + + Lemma compare_Eq : forall x y, compare x y = Eq <-> eq x y. + Proof. + unfold compare. + intros x y; destruct (compare_spec x y); intuition; + try discriminate. + rewrite H0 in H. elim (StrictOrder_Irreflexive y); auto. + rewrite H0 in H. elim (StrictOrder_Irreflexive y); auto. + Qed. + + Lemma compare_Lt : forall x y, compare x y = Lt <-> lt x y. + Proof. + unfold compare. + intros x y; destruct (compare_spec x y); intuition; + try discriminate. + rewrite H in H0. elim (StrictOrder_Irreflexive y); auto. + rewrite H in H0. elim (StrictOrder_Irreflexive x); auto. + Qed. + + Lemma compare_Gt : forall x y, compare x y = Gt <-> lt y x. + Proof. + intros x y. rewrite compare_sym, CompOpp_iff. apply compare_Lt. + Qed. + + Lemma compare_trans : + forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c. + Proof. + intros c x y z. + destruct c; unfold compare; + rewrite ?compare_Eq, ?compare_Lt, ?compare_Gt; + transitivity y; auto. + Qed. + +End OT_to_Alt. |