Library Coq.Structures.OrdersAlt



Require Import OrderedType Orders.
Set Implicit Arguments.

Some alternative (but equivalent) presentations for an Ordered Type

inferface.

The original interface

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.

#[global]
 Instance lt_strorder : StrictOrder lt.

#[global]
 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.

#[global]
 Instance eq_equiv : Equivalence eq.

#[global]
 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.

#[global]
 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.