# Library Coq.Structures.OrdersFacts

Require Import Basics OrdersTac.
Require Export Orders.

# Properties of OrderedTypeFull

Module OrderedTypeFullFacts (Import O:OrderedTypeFull').
Module OrderTac := OTF_to_OrderTac O.
Ltac order := OrderTac.order.
Ltac iorder := intuition order.
Instance le_compat : Proper (eq ==> eq ==> iff) le.
Instance le_preorder : PreOrder le.
Instance le_order : PartialOrder eq le.
Instance le_antisym : Antisymmetric _ eq le.
Lemma le_not_gt_iff : forall x y, x <= y <-> ~ y < x.
Lemma lt_not_ge_iff : forall x y, x < y <-> ~ y <= x.
Lemma le_or_gt : forall x y, x <= y \/ y < x.
Lemma lt_or_ge : forall x y, x < y \/ y <= x.
Lemma eq_is_le_ge : forall x y, x == y <-> x <= y /\ y <= x.
End OrderedTypeFullFacts.

# Properties of OrderedType

Module OrderedTypeFacts (Import O: OrderedType').
Module OrderTac := OT_to_OrderTac O.
Ltac order := OrderTac.order.
Notation "x <= y" := (~ lt y x) : order.
Infix "?=" := compare (at level 70, no associativity) : order.
Local Open Scope order.
Tactic Notation "elim_compare" constr(x) constr(y) :=
destruct (compare_spec x y).
Tactic Notation "elim_compare" constr(x) constr(y) "as" ident(h) :=
destruct (compare_spec x y) as [h|h|h].
The following lemmas are either re-phrasing of eq_equiv and lt_strorder or immediately provable by order. Interest: compatibility, test of order, etc
Definition eq_refl (x:t) : x == x := Equivalence_Reflexive x.
Definition eq_sym (x y:t) : x == y -> y == x := Equivalence_Symmetric x y.
Definition eq_trans (x y z:t) : x == y -> y == z -> x == z :=
Equivalence_Transitive x y z.
Definition lt_trans (x y z:t) : x < y -> y < z -> x < z :=
StrictOrder_Transitive x y z.
Definition lt_irrefl (x:t) : ~ x < x := StrictOrder_Irreflexive x.
Some more about compare
Lemma compare_eq_iff : forall x y, ( x ?= y ) = Eq <-> x == y.
Lemma compare_lt_iff : forall x y, ( x ?= y ) = Lt <-> x < y.
Lemma compare_gt_iff : forall x y, ( x ?= y ) = Gt <-> y < x.
Lemma compare_ge_iff : forall x y, ( x ?= y ) <> Lt <-> y <= x.
Lemma compare_le_iff : forall x y, ( x ?= y ) <> Gt <-> x <= y.
Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order.
Instance compare_compat : Proper (eq ==> eq ==> Logic.eq) compare.
Lemma compare_refl : forall x, ( x ?= x ) = Eq.
Lemma compare_antisym : forall x y, ( y ?= x ) = CompOpp (x ?= y).
For compatibility reasons
Definition eq_dec := eq_dec.
Lemma lt_dec : forall x y : t, { lt x y } + { ~ lt x y }.
Definition eqb x y : bool := if eq_dec x y then true else false.
Lemma if_eq_dec : forall x y (B:Type)(b b':B),
( if eq_dec x y then b else b' ) =
( match compare x y with Eq => b | _ => b' end ).
Lemma eqb_alt :
forall x y, eqb x y = match compare x y with Eq => true | _ => false end.
Instance eqb_compat : Proper (eq ==> eq ==> Logic.eq) eqb.
End OrderedTypeFacts.

# Tests of the order tactic

Is it at least capable of proving some basic properties ?
Module OrderedTypeTest (Import O:OrderedType').
Module Import MO := OrderedTypeFacts O.
Local Open Scope order.
Lemma lt_not_eq x y : x < y -> ~ x == y.
Lemma lt_eq x y z : x < y -> y == z -> x < z.
Lemma eq_lt x y z : x == y -> y < z -> x < z.
Lemma le_eq x y z : x <= y -> y == z -> x <= z.
Lemma eq_le x y z : x == y -> y <= z -> x <= z.
Lemma neq_eq x y z : ~ x == y -> y == z -> ~ x == z.
Lemma eq_neq x y z : x == y -> ~ y == z -> ~ x == z.
Lemma le_lt_trans x y z : x <= y -> y < z -> x < z.
Lemma lt_le_trans x y z : x < y -> y <= z -> x < z.
Lemma le_trans x y z : x <= y -> y <= z -> x <= z.
Lemma le_antisym x y : x <= y -> y <= x -> x == y.
Lemma le_neq x y : x <= y -> ~ x == y -> x < y.
Lemma neq_sym x y : ~ x == y -> ~ y == x.
Lemma lt_le x y : x < y -> x <= y.
Lemma gt_not_eq x y : y < x -> ~ x == y.
Lemma eq_not_lt x y : x == y -> ~ x < y.
Lemma eq_not_gt x y : x == y -> ~ y < x.
Lemma lt_not_gt x y : x < y -> ~ y < x.
Lemma eq_is_nlt_ngt x y : x == y <-> ~ x < y /\ ~ y < x.
End OrderedTypeTest.

# Reversed OrderedTypeFull.

we can switch the orientation of the order. This is used for example when deriving properties of min out of the ones of max (see GenericMinMax).
Module OrderedTypeRev (O:OrderedTypeFull) <: OrderedTypeFull.
Definition t := O.t.
Definition eq := O.eq.
Instance eq_equiv : Equivalence eq.
Definition eq_dec := O.eq_dec.
Definition lt := flip O.lt.
Definition le := flip O.le.
Instance lt_strorder: StrictOrder lt.
Instance lt_compat : Proper (eq ==> eq ==> iff) lt.
Lemma le_lteq : forall x y, le x y <-> lt x y \/ eq x y.
Definition compare := flip O.compare.
Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
End OrderedTypeRev.