Library CoLoR.Util.Relation.OrdUtil

CoLoR, a Coq library on rewriting and termination.
See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2013-09-17

Structures for types equipped with a comparison function.


Set Implicit Arguments.


Properties of CompOpp.

Lemma CompOpp_eq : forall c d, CompOpp c = CompOpp d <-> c = d.

Structure for a type equipped with a comparison function.

Module Type Cmp.

  Parameter t : Type.

  Parameter cmp : t -> t -> comparison.

  Parameter cmp_opp : forall x y, cmp x y = CompOpp (cmp y x).

End Cmp.

Properties of types equipped with a comparison function.

Module CmpFacts (Import C : Cmp).

  Definition eq : relation t := fun x y => cmp x y = Eq.

  Definition lt : relation t := fun x y => cmp x y = Lt.

  Instance eq_refl : Reflexive eq.


  Instance eq_sym : Symmetric eq.


  Lemma lt_not_eq x y : lt x y -> ~eq x y.

  Lemma compare x y : Compare lt eq x y.

End CmpFacts.

Structure for a type equipped with a comparison function that is transitive. The type is therefore totally ordered. This structure is equivalent to Structures.OrderedTypeAlt.

Module Type CmpTrans.

  Include Cmp.

  Parameter cmp_eq_trans :
    forall x y z, cmp x y = Eq -> cmp y z = Eq -> cmp x z = Eq.

  Parameter cmp_lt_trans :
    forall x y z, cmp x y = Lt -> cmp y z = Lt -> cmp x z = Lt.

End CmpTrans.

Properties of types equipped with a comparison function that is transitive.

Module CmpTransFacts (Import CT : CmpTrans).

  Include CmpFacts CT.

  Instance eq_trans : Transitive eq.


  Instance lt_trans : Transitive lt.


End CmpTransFacts.

Functor buiding a MiniOrderedType structure from a CmpTrans structure.

Module MOT_of_CmpTrans (Import CT : CmpTrans) <: MiniOrderedType.

  Definition t := t.

  Include CmpTransFacts CT.

End MOT_of_CmpTrans.

Structure for a type equipped with a transitive comparison function whose equivalence is Leibniz equality.

Module Type CmpTransLeibniz.

  Include Cmp.

  Parameter cmp_eq : forall x y, cmp x y = Eq -> x = y.

  Parameter cmp_lt_trans :
    forall x y z, cmp x y = Lt -> cmp y z = Lt -> cmp x z = Lt.

End CmpTransLeibniz.

Functor building a CmpTrans structure from a CmpTransLeibniz structure.

Module CmpTrans_of_CmpTransLeibniz (CTL : CmpTransLeibniz) <: CmpTrans.

  Include CTL.

  Module Import CF := CmpFacts CTL.

  Lemma cmp_eq_trans x y z : cmp x y = Eq -> cmp y z = Eq -> cmp x z = Eq.

End CmpTrans_of_CmpTransLeibniz.

Functor building a MiniOrderedType structure from a CmpTransLeibniz structure.

Module MOT_of_CmpTransLeibniz (Import CTL : CmpTransLeibniz) <: MiniOrderedType.

  Definition t := t.

  Include LeibnizFacts CTL.

  Definition lt : relation t := fun x y => cmp x y = Lt.

  Instance lt_trans : Transitive lt.


  Lemma lt_not_eq x y : lt x y -> x <> y.

  Lemma compare x y : Compare lt eq x y.

End MOT_of_CmpTransLeibniz.