Library Coq.Structures.OrdersAlt
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.
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.
Module Update_OT (O:OrderedTypeOrig) <: OrderedType.
Include Update_DT O.
Definition lt := O.lt.
Instance lt_strorder : StrictOrder lt.
Instance lt_compat : Proper (eq==>eq==>iff) lt.
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).
End Update_OT.
Module Backport_OT (O:OrderedType) <: OrderedTypeOrig.
Include Backport_DT O.
Definition lt := O.lt.
Lemma lt_not_eq : forall x y, lt x y -> ~eq x y.
Lemma lt_trans : Transitive lt.
Definition compare : forall x y, Compare lt eq x y.
End Backport_OT.
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.
Instance lt_strorder : StrictOrder lt.
Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z.
Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z.
Instance lt_compat : Proper (eq==>eq==>iff) lt.
Definition compare := O.compare.
Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
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).
Lemma compare_Eq : forall x y, compare x y = Eq <-> eq x y.
Lemma compare_Lt : forall x y, compare x y = Lt <-> lt x y.
Lemma compare_Gt : forall x y, compare x y = Gt <-> lt y x.
Lemma compare_trans :
forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c.
End OT_to_Alt.