Library Coq.Structures.Orders



Require Export Relations Morphisms Setoid Equalities.

Ordered types


First, signatures with only the order relations

Module Type HasLt (Import T:Typ).
  Parameter Inline lt : t -> t -> Prop.
End HasLt.

Module Type HasLe (Import T:Typ).
  Parameter Inline le : t -> t -> Prop.
End HasLe.

Module Type EqLt := Typ <+ HasEq <+ HasLt.
Module Type EqLe := Typ <+ HasEq <+ HasLe.
Module Type EqLtLe := Typ <+ HasEq <+ HasLt <+ HasLe.

Versions with nice notations

Module Type LtNotation (E:EqLt).
  Infix "<" := E.lt.
  Notation "x > y" := (y<x) (only parsing).
  Notation "x < y < z" := (x<y /\ y<z).
End LtNotation.

Module Type LeNotation (E:EqLe).
  Infix "<=" := E.le.
  Notation "x >= y" := (y<=x) (only parsing).
  Notation "x <= y <= z" := (x<=y /\ y<=z).
End LeNotation.

Module Type LtLeNotation (E:EqLtLe).
  Include LtNotation E <+ LeNotation E.
  Notation "x <= y < z" := (x<=y /\ y<z).
  Notation "x < y <= z" := (x<y /\ y<=z).
End LtLeNotation.

Module Type EqLtNotation (E:EqLt) := EqNotation E <+ LtNotation E.
Module Type EqLeNotation (E:EqLe) := EqNotation E <+ LeNotation E.
Module Type EqLtLeNotation (E:EqLtLe) := EqNotation E <+ LtLeNotation E.

Module Type EqLt' := EqLt <+ EqLtNotation.
Module Type EqLe' := EqLe <+ EqLeNotation.
Module Type EqLtLe' := EqLtLe <+ EqLtLeNotation.

Versions with logical specifications

Module Type IsStrOrder (Import E:EqLt).
  Declare Instance lt_strorder : StrictOrder lt.
  Declare Instance lt_compat : Proper (eq==>eq==>iff) lt.
End IsStrOrder.

Module Type LeIsLtEq (Import E:EqLtLe').
  Axiom le_lteq : forall x y, x<=y <-> x<y \/ x==y.
End LeIsLtEq.

Module Type HasCompare (Import E:EqLt).
  Parameter Inline compare : t -> t -> comparison.
  Axiom compare_spec : forall x y, CompSpec eq lt x y (compare x y).
End HasCompare.

Module Type StrOrder := EqualityType <+ HasLt <+ IsStrOrder.
Module Type DecStrOrder := StrOrder <+ HasCompare.
Module Type OrderedType <: DecidableType := DecStrOrder <+ HasEqDec.
Module Type OrderedTypeFull := OrderedType <+ HasLe <+ LeIsLtEq.

Module Type StrOrder' := StrOrder <+ EqLtNotation.
Module Type DecStrOrder' := DecStrOrder <+ EqLtNotation.
Module Type OrderedType' := OrderedType <+ EqLtNotation.
Module Type OrderedTypeFull' := OrderedTypeFull <+ EqLtLeNotation.

NB: in OrderedType, an eq_dec could be deduced from compare. But adding this redundant field allows to see an OrderedType as a DecidableType.

Versions with eq being the usual Leibniz equality of Coq


Module Type UsualStrOrder := UsualEqualityType <+ HasLt <+ IsStrOrder.
Module Type UsualDecStrOrder := UsualStrOrder <+ HasCompare.
Module Type UsualOrderedType <: UsualDecidableType <: OrderedType
 := UsualDecStrOrder <+ HasEqDec.
Module Type UsualOrderedTypeFull := UsualOrderedType <+ HasLe <+ LeIsLtEq.

NB: in UsualOrderedType, the field lt_compat is useless since eq is Leibniz, but it should be there for subtyping.

Module Type UsualStrOrder' := UsualStrOrder <+ LtNotation.
Module Type UsualDecStrOrder' := UsualDecStrOrder <+ LtNotation.
Module Type UsualOrderedType' := UsualOrderedType <+ LtNotation.
Module Type UsualOrderedTypeFull' := UsualOrderedTypeFull <+ LtLeNotation.

Purely logical versions


Module Type LtIsTotal (Import E:EqLt').
  Axiom lt_total : forall x y, x<y \/ x==y \/ y<x.
End LtIsTotal.

Module Type TotalOrder := StrOrder <+ HasLe <+ LeIsLtEq <+ LtIsTotal.
Module Type UsualTotalOrder <: TotalOrder
 := UsualStrOrder <+ HasLe <+ LeIsLtEq <+ LtIsTotal.

Module Type TotalOrder' := TotalOrder <+ EqLtLeNotation.
Module Type UsualTotalOrder' := UsualTotalOrder <+ LtLeNotation.

Conversions


From compare to eqb, and then eq_dec

Module Compare2EqBool (Import O:DecStrOrder') <: HasEqBool O.

 Definition eqb x y :=
   match compare x y with Eq => true | _ => false end.

 Lemma eqb_eq : forall x y, eqb x y = true <-> x==y.

End Compare2EqBool.

Module DSO_to_OT (O:DecStrOrder) <: OrderedType :=
  O <+ Compare2EqBool <+ HasEqBool2Dec.

From OrderedType To OrderedTypeFull (adding <=)

Module OT_to_Full (O:OrderedType') <: OrderedTypeFull.
 Include O.
 Definition le x y := x<y \/ x==y.
 Lemma le_lteq : forall x y, le x y <-> x<y \/ x==y.
End OT_to_Full.

From computational to logical versions

Module OTF_LtIsTotal (Import O:OrderedTypeFull') <: LtIsTotal O.
 Lemma lt_total : forall x y, x<y \/ x==y \/ y<x.
End OTF_LtIsTotal.

Module OTF_to_TotalOrder (O:OrderedTypeFull) <: TotalOrder
 := O <+ OTF_LtIsTotal.

Versions with boolean comparisons



This style is used in Mergesort

For stating properties like transitivity of leb, we coerce bool into Prop.

Local Coercion is_true : bool >-> Sortclass.
Hint Unfold is_true.

Module Type HasLeBool (Import T:Typ).
  Parameter Inline leb : t -> t -> bool.
End HasLeBool.

Module Type HasLtBool (Import T:Typ).
  Parameter Inline ltb : t -> t -> bool.
End HasLtBool.

Module Type LeBool := Typ <+ HasLeBool.
Module Type LtBool := Typ <+ HasLtBool.

Module Type LeBoolNotation (E:LeBool).
  Infix "<=?" := E.leb (at level 35).
End LeBoolNotation.

Module Type LtBoolNotation (E:LtBool).
  Infix "<?" := E.ltb (at level 35).
End LtBoolNotation.

Module Type LeBool' := LeBool <+ LeBoolNotation.
Module Type LtBool' := LtBool <+ LtBoolNotation.

Module Type LeBool_Le (T:Typ)(X:HasLeBool T)(Y:HasLe T).
 Parameter leb_le : forall x y, X.leb x y = true <-> Y.le x y.
End LeBool_Le.

Module Type LtBool_Lt (T:Typ)(X:HasLtBool T)(Y:HasLt T).
 Parameter ltb_lt : forall x y, X.ltb x y = true <-> Y.lt x y.
End LtBool_Lt.

Module Type LeBoolIsTotal (Import X:LeBool').
 Axiom leb_total : forall x y, (x <=? y) = true \/ (y <=? x) = true.
End LeBoolIsTotal.

Module Type TotalLeBool := LeBool <+ LeBoolIsTotal.
Module Type TotalLeBool' := LeBool' <+ LeBoolIsTotal.

Module Type LeBoolIsTransitive (Import X:LeBool').
 Axiom leb_trans : Transitive X.leb.
End LeBoolIsTransitive.

Module Type TotalTransitiveLeBool := TotalLeBool <+ LeBoolIsTransitive.
Module Type TotalTransitiveLeBool' := TotalLeBool' <+ LeBoolIsTransitive.

From OrderedTypeFull to TotalTransitiveLeBool


Module OTF_to_TTLB (Import O : OrderedTypeFull') <: TotalTransitiveLeBool.

 Definition leb x y :=
  match compare x y with Gt => false | _ => true end.

 Lemma leb_le : forall x y, leb x y <-> x <= y.

 Lemma leb_total : forall x y, leb x y \/ leb y x.

 Lemma leb_trans : Transitive leb.

 Definition t := t.

End OTF_to_TTLB.

From TotalTransitiveLeBool to OrderedTypeFull



le is leb ... = true. eq is le /\ swap le. lt is le /\ ~swap le.

Local Open Scope bool_scope.

Module TTLB_to_OTF (Import O : TotalTransitiveLeBool') <: OrderedTypeFull.

 Definition t := t.

 Definition le x y : Prop := x <=? y.
 Definition eq x y : Prop := le x y /\ le y x.
 Definition lt x y : Prop := le x y /\ ~le y x.

 Definition compare x y :=
  if x <=? y then (if y <=? x then Eq else Lt) else Gt.

 Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).

 Definition eqb x y := (x <=? y) && (y <=? x).

 Lemma eqb_eq : forall x y, eqb x y <-> eq x y.

 Include HasEqBool2Dec.

 Instance eq_equiv : Equivalence eq.

 Instance lt_strorder : StrictOrder lt.

 Instance lt_compat : Proper (eq ==> eq ==> iff) lt.

 Definition le_lteq : forall x y, le x y <-> lt x y \/ eq x y.

End TTLB_to_OTF.