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.

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.
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.

From OrderedType to OrderedTypeOrig.

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.

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.

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.