Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Export Relations Morphisms Setoid Equalities.
Set Implicit Arguments.
Unset Strict Implicit.

Ordered types

First, signatures with only the order relations

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

Module Type HasLe (Import T:Typ).
  Parameter Inline(40) 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 StrOrder := EqualityType <+ HasLt <+ IsStrOrder.
Module Type StrOrder' := StrOrder <+ EqLtNotation.

Versions with a decidable ternary comparison

Module Type HasCmp (Import T:Typ).
  Parameter Inline compare : t -> t -> comparison.
End HasCmp.

Module Type CmpNotation (T:Typ)(C:HasCmp T).
  Infix "?=" := C.compare (at level 70, no associativity).
End CmpNotation.

Module Type CmpSpec (Import E:EqLt')(Import C:HasCmp E).
  Axiom compare_spec : forall x y, CompareSpec (x==y) (x<y) (y<x) (compare x y).
End CmpSpec.

Module Type HasCompare (E:EqLt) := HasCmp E <+ CmpSpec E.

Module Type DecStrOrder := StrOrder <+ HasCompare.
Module Type DecStrOrder' := DecStrOrder <+ EqLtNotation <+ CmpNotation.

Module Type OrderedType <: DecidableType := DecStrOrder <+ HasEqDec.
Module Type OrderedType' := OrderedType <+ EqLtNotation <+ CmpNotation.

Module Type OrderedTypeFull := OrderedType <+ HasLe <+ LeIsLtEq.
Module Type OrderedTypeFull' :=
 OrderedTypeFull <+ EqLtLeNotation <+ CmpNotation.

NB: in OrderedType, an eq_dec could be deduced from compare. But adding this redundant field allows seeing 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.forall x y : t, eqb x y = true <-> x == y
 Proof.forall x y : t, eqb x y = true <-> x == y
 unfold eqb.forall x y : t,
match x ?= y with
| Eq => true
| _ => false
end = true <-> x == y intros x y.x, y:t
match x ?= y with
| Eq => true
| _ => false
end = true <-> x == y
 destruct (compare_spec x y) as [H|H|H]; split; auto; try discriminate.x, y:t
H:x < y
x == y -> false = true
x, y:t
H:y < x
x == y -> false = true
 -x, y:t
H:x < y
x == y -> false = true intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H).
 -x, y:t
H:y < x
x == y -> false = true intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H).
 Qed.

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.forall x y : t, le x y <-> x < y \/ x == y
 Proof.forall x y : t, le x y <-> x < y \/ x == y unfold le; split; auto. Qed.
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.forall x y : t, x < y \/ x == y \/ y < x
 Proof.forall x y : t, x < y \/ x == y \/ y < x intros; destruct (compare_spec x y); auto. Qed.
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.

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

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

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

Module Type LebNotation (T:Typ)(E:HasLeb T).
 Infix "<=?" := E.leb (at level 35).
End LebNotation.

Module Type LtbNotation (T:Typ)(E:HasLtb T).
 Infix "<?" := E.ltb (at level 35).
End LtbNotation.

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

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

Module Type LeBool := Typ <+ HasLeb.
Module Type LtBool := Typ <+ HasLtb.
Module Type LeBool' := LeBool <+ LebNotation.
Module Type LtBool' := LtBool <+ LtbNotation.

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

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

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

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

Grouping all boolean comparison functions

Module Type HasBoolOrdFuns (T:Typ) := HasEqb T <+ HasLtb T <+ HasLeb T.

Module Type HasBoolOrdFuns' (T:Typ) :=
 HasBoolOrdFuns T <+ EqbNotation T <+ LtbNotation T <+ LebNotation T.

Module Type BoolOrdSpecs (O:EqLtLe)(F:HasBoolOrdFuns O) :=
 EqbSpec O O F <+ LtbSpec O O F <+ LebSpec O O F.

Module Type OrderFunctions (E:EqLtLe) :=
  HasCompare E <+ HasBoolOrdFuns E <+ BoolOrdSpecs E.
Module Type OrderFunctions' (E:EqLtLe) :=
  HasCompare E <+ CmpNotation E <+ HasBoolOrdFuns' E <+ BoolOrdSpecs E.

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.forall x y : t, leb x y <-> x <= y
 Proof.forall x y : t, leb x y <-> x <= y
 intros.x, y:t
leb x y <-> x <= y unfold leb.x, y:t
match x ?= y with
| Gt => false
| _ => true
end <-> x <= y rewrite le_lteq.x, y:t
match x ?= y with
| Gt => false
| _ => true
end <-> x < y \/ x == y
 destruct (compare_spec x y) as [EQ|LT|GT]; split; auto.x, y:t
GT:y < x
false -> x < y \/ x == y
x, y:t
GT:y < x
x < y \/ x == y -> false
 -x, y:t
GT:y < x
false -> x < y \/ x == y discriminate.
 -x, y:t
GT:y < x
x < y \/ x == y -> false intros LE.x, y:t
GT:y < x
LE:x < y \/ x == y
is_true false elim (StrictOrder_Irreflexive x).x, y:t
GT:y < x
LE:x < y \/ x == y
x < x
   destruct LE as [LT|EQ].x, y:t
GT:y < x
LT:x < y
x < x
x, y:t
GT:y < x
EQ:x == y
x < x
   +x, y:t
GT:y < x
LT:x < y
x < x now transitivity y.
   +x, y:t
GT:y < x
EQ:x == y
x < x now rewrite <- EQ in GT.
 Qed.

 Lemma leb_total : forall x y, leb x y \/ leb y x.forall x y : t, leb x y \/ leb y x
 Proof.forall x y : t, leb x y \/ leb y x
 intros.x, y:t
leb x y \/ leb y x rewrite 2 leb_le.x, y:t
x <= y \/ y <= x rewrite 2 le_lteq.x, y:t
(x < y \/ x == y) \/ y < x \/ y == x
 destruct (compare_spec x y); intuition.
 Qed.

 Lemma leb_trans : Transitive leb.Transitive (fun x y : t => leb x y)
 Proof.Transitive (fun x y : t => leb x y)
 intros x y z.x, y, z:t
leb x y -> leb y z -> leb x z rewrite !leb_le, !le_lteq.x, y, z:t
x < y \/ x == y -> y < z \/ y == z -> x < z \/ x == z
 intros [Hxy|Hxy] [Hyz|Hyz].x, y, z:t
Hxy:x < y
Hyz:y < z
x < z \/ x == z
x, y, z:t
Hxy:x < y
Hyz:y == z
x < z \/ x == z
x, y, z:t
Hxy:x == y
Hyz:y < z
x < z \/ x == z
x, y, z:t
Hxy:x == y
Hyz:y == z
x < z \/ x == z
 -x, y, z:t
Hxy:x < y
Hyz:y < z
x < z \/ x == z left; transitivity y; auto.
 -x, y, z:t
Hxy:x < y
Hyz:y == z
x < z \/ x == z left; rewrite <- Hyz; auto.
 -x, y, z:t
Hxy:x == y
Hyz:y < z
x < z \/ x == z left; rewrite Hxy; auto.
 -x, y, z:t
Hxy:x == y
Hyz:y == z
x < z \/ x == z right; transitivity y; auto.
 Qed.

 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).forall x y : O.t, CompSpec eq lt x y (compare x y)
 Proof.forall x y : O.t, CompSpec eq lt x y (compare x y)
 intros.x, y:O.t
CompSpec eq lt x y (compare x y) unfold compare.x, y:O.t
CompSpec eq lt x y
  (if x <=? y then if y <=? x then Eq else Lt else Gt)
 case_eq (x <=? y).x, y:O.t
x <=? y = true ->
CompSpec eq lt x y (if y <=? x then Eq else Lt)
x, y:O.t
x <=? y = false -> CompSpec eq lt x y Gt
 -x, y:O.t
x <=? y = true ->
CompSpec eq lt x y (if y <=? x then Eq else Lt) case_eq (y <=? x).x, y:O.t
y <=? x = true ->
x <=? y = true -> CompSpec eq lt x y Eq
x, y:O.t
y <=? x = false ->
x <=? y = true -> CompSpec eq lt x y Lt
   +x, y:O.t
y <=? x = true ->
x <=? y = true -> CompSpec eq lt x y Eq constructor.x, y:O.t
H:y <=? x = true
H0:x <=? y = true
eq x y split; auto.
   +x, y:O.t
y <=? x = false ->
x <=? y = true -> CompSpec eq lt x y Lt constructor.x, y:O.t
H:y <=? x = false
H0:x <=? y = true
lt x y split; congruence.
 -x, y:O.t
x <=? y = false -> CompSpec eq lt x y Gt constructor.x, y:O.t
H:x <=? y = false
lt y x destruct (leb_total x y); split; congruence.
 Qed.

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

 Lemma eqb_eq : forall x y, eqb x y <-> eq x y.forall x y : O.t, eqb x y <-> eq x y
 Proof.forall x y : O.t, eqb x y <-> eq x y
 intros.x, y:O.t
eqb x y <-> eq x y unfold eq, eqb, le.x, y:O.t
x <=? y && y <=? x <-> x <=? y /\ y <=? x
 case leb; simpl; intuition; discriminate.
 Qed.

 Include HasEqBool2Dec.

 Instance eq_equiv : Equivalence eq.Equivalence eq
 Proof.Equivalence eq
 split.Reflexive eq
Symmetric eq
Transitive eq
 -Reflexive eq intros x; unfold eq, le.x:O.t
x <=? x /\ x <=? x destruct (leb_total x x); auto.
 -Symmetric eq intros x y; unfold eq, le.x, y:O.t
x <=? y /\ y <=? x -> y <=? x /\ x <=? y intuition.
 -Transitive eq intros x y z; unfold eq, le.x, y, z:O.t
x <=? y /\ y <=? x ->
y <=? z /\ z <=? y -> x <=? z /\ z <=? x intuition; apply leb_trans with y; auto.
 Qed.

 Instance lt_strorder : StrictOrder lt.StrictOrder lt
 Proof.StrictOrder lt
 split.Irreflexive lt
Transitive lt
 -Irreflexive lt intros x.x:O.t
complement lt x x unfold lt; red; intuition.
 -Transitive lt intros x y z; unfold lt, le.x, y, z:O.t
x <=? y /\ ~ y <=? x ->
y <=? z /\ ~ z <=? y -> x <=? z /\ ~ z <=? x intuition.x, y, z:O.t
H1:is_true (x <=? y)
H2:y <=? x -> False
H:is_true (y <=? z)
H3:z <=? y -> False
is_true (x <=? z)
x, y, z:O.t
H1:is_true (x <=? y)
H2:y <=? x -> False
H:is_true (y <=? z)
H3:z <=? y -> False
H0:is_true (z <=? x)
False
   +x, y, z:O.t
H1:is_true (x <=? y)
H2:y <=? x -> False
H:is_true (y <=? z)
H3:z <=? y -> False
is_true (x <=? z) apply leb_trans with y; auto.
   +x, y, z:O.t
H1:is_true (x <=? y)
H2:y <=? x -> False
H:is_true (y <=? z)
H3:z <=? y -> False
H0:is_true (z <=? x)
False absurd (z <=? y); auto.x, y, z:O.t
H1:is_true (x <=? y)
H2:y <=? x -> False
H:is_true (y <=? z)
H3:z <=? y -> False
H0:is_true (z <=? x)
is_true (z <=? y)
     apply leb_trans with x; auto.
 Qed.

 Instance lt_compat : Proper (eq ==> eq ==> iff) lt.Proper (eq ==> eq ==> iff) lt
 Proof.Proper (eq ==> eq ==> iff) lt
 apply proper_sym_impl_iff_2; auto with *.Proper (eq ==> eq ==> Basics.impl) lt
 intros x x' Hx y y' Hy' H.x, x':O.t
Hx:eq x x'
y, y':O.t
Hy':eq y y'
H:lt x y
lt x' y' unfold eq, lt, le in *.x, x':O.t
Hx:x <=? x' /\ x' <=? x
y, y':O.t
Hy':y <=? y' /\ y' <=? y
H:x <=? y /\ ~ y <=? x
x' <=? y' /\ ~ y' <=? x'
 intuition.x, x', y, y':O.t
H0:is_true (x <=? x')
H1:is_true (x' <=? x)
H2:is_true (y <=? y')
H3:is_true (y' <=? y)
H4:is_true (x <=? y)
H5:y <=? x -> False
is_true (x' <=? y')
x, x', y, y':O.t
H0:is_true (x <=? x')
H1:is_true (x' <=? x)
H2:is_true (y <=? y')
H3:is_true (y' <=? y)
H4:is_true (x <=? y)
H5:y <=? x -> False
H:is_true (y' <=? x')
False
 -x, x', y, y':O.t
H0:is_true (x <=? x')
H1:is_true (x' <=? x)
H2:is_true (y <=? y')
H3:is_true (y' <=? y)
H4:is_true (x <=? y)
H5:y <=? x -> False
is_true (x' <=? y') apply leb_trans with x; auto.x, x', y, y':O.t
H0:is_true (x <=? x')
H1:is_true (x' <=? x)
H2:is_true (y <=? y')
H3:is_true (y' <=? y)
H4:is_true (x <=? y)
H5:y <=? x -> False
is_true (x <=? y')
   apply leb_trans with y; auto.
 -x, x', y, y':O.t
H0:is_true (x <=? x')
H1:is_true (x' <=? x)
H2:is_true (y <=? y')
H3:is_true (y' <=? y)
H4:is_true (x <=? y)
H5:y <=? x -> False
H:is_true (y' <=? x')
False absurd (y <=? x); auto.x, x', y, y':O.t
H0:is_true (x <=? x')
H1:is_true (x' <=? x)
H2:is_true (y <=? y')
H3:is_true (y' <=? y)
H4:is_true (x <=? y)
H5:y <=? x -> False
H:is_true (y' <=? x')
is_true (y <=? x)
   apply leb_trans with x'; auto.x, x', y, y':O.t
H0:is_true (x <=? x')
H1:is_true (x' <=? x)
H2:is_true (y <=? y')
H3:is_true (y' <=? y)
H4:is_true (x <=? y)
H5:y <=? x -> False
H:is_true (y' <=? x')
is_true (y <=? x')
   apply leb_trans with y'; auto.
 Qed.

 Definition le_lteq : forall x y, le x y <-> lt x y \/ eq x y.forall x y : O.t, le x y <-> lt x y \/ eq x y
 Proof.forall x y : O.t, le x y <-> lt x y \/ eq x y
 intros.x, y:O.t
le x y <-> lt x y \/ eq x y
 unfold lt, eq, le.x, y:O.t
x <=? y <-> x <=? y /\ ~ y <=? x \/ x <=? y /\ y <=? x
 split; [ | intuition ].x, y:O.t
x <=? y -> x <=? y /\ ~ y <=? x \/ x <=? y /\ y <=? x
 intros LE.x, y:O.t
LE:is_true (x <=? y)
x <=? y /\ ~ y <=? x \/ x <=? y /\ y <=? x
 case_eq (y <=? x); [right|left]; intuition; try discriminate.
 Qed.

End TTLB_to_OTF.