Library Coq.Structures.OrdersFacts

Require Import Bool Basics OrdersTac.
Require Export Orders.

Set Implicit Arguments.

Properties of compare

Module Type CompareFacts (Import O:DecStrOrder').

Local Infix "?=" := compare (at level 70, no associativity).

Lemma compare_eq_iff x y : (x ?= y ) = Eq <-> x ==y.

Lemma compare_eq x y : (x ?= y ) = Eq -> x ==y.

Lemma compare_lt_iff x y : (x ?= y ) = Lt <-> x <y.

Lemma compare_gt_iff x y : (x ?= y ) = Gt <-> y <x.

Lemma compare_nlt_iff x y : (x ?= y ) <> Lt <-> ~(x <y ).

Lemma compare_ngt_iff x y : (x ?= y ) <> Gt <-> ~(y <x ).

Global Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order.

#[global]
Instance compare_compat : Proper (eq ==>eq ==>Logic.eq) compare.

Lemma compare_refl x : (x ?= x ) = Eq.

Lemma compare_antisym x y : (y ?= x ) = CompOpp (x ?= y).

End CompareFacts.

Properties of OrderedTypeFull

Module OrderedTypeFullFacts (Import O:OrderedTypeFull').

Module OrderTac := OTF_to_OrderTac O.
Ltac order := OrderTac.order.
Ltac iorder := intuition order.

#[global]
Instance le_compat : Proper (eq ==>eq ==>iff) le.

#[global]
Instance le_preorder : PreOrder le.

#[global]
Instance le_order : PartialOrder eq le.

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

Include CompareFacts O.

Lemma compare_le_iff x y : compare x y <> Gt <-> x <=y.

Lemma compare_ge_iff x y : compare x y <> Lt <-> y <=x.

End OrderedTypeFullFacts.

Properties of OrderedType

Module OrderedTypeFacts (Import O: OrderedType').

  Module OrderTac := OT_to_OrderTac O.
  Ltac order := OrderTac.order.

  Declare Scope 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.

  Include CompareFacts O.
  Notation compare_le_iff := compare_ngt_iff (only parsing).
  Notation compare_ge_iff := compare_nlt_iff (only parsing).

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 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.

#[global]
  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.
#[global]
Program Instance eq_equiv : Equivalence eq.
Definition eq_dec := O.eq_dec.

Definition lt := flip O.lt.
Definition le := flip O.le.

#[global]
Instance lt_strorder: StrictOrder lt.
#[global]
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.

Unset Implicit Arguments.

Order relations derived from a compare function.

We factorize here some common properties for ZArith, NArith and co, where lt and le are defined in terms of compare. Note that we do not require anything here concerning compatibility of compare w.r.t eq, nor anything concerning transitivity.

Module Type CompareBasedOrder (Import E:EqLtLe')(Import C:HasCmp E).
Include CmpNotation E C.
Include IsEq E.
Axiom compare_eq_iff : forall x y, (x ?= y ) = Eq <-> x == y.
Axiom compare_lt_iff : forall x y, (x ?= y ) = Lt <-> x < y.
Axiom compare_le_iff : forall x y, (x ?= y ) <> Gt <-> x <= y.
Axiom compare_antisym : forall x y, (y ?= x ) = CompOpp (x ?= y).
End CompareBasedOrder.

Module Type CompareBasedOrderFacts
(Import E:EqLtLe')
(Import C:HasCmp E)
(Import O:CompareBasedOrder E C).

Lemma compare_spec x y : CompareSpec (x ==y) (x <y) (y <x) (x ?=y).

Lemma compare_eq x y : (x ?= y ) = Eq -> x ==y.

Lemma compare_refl x : (x ?= x ) = Eq.

Lemma compare_gt_iff x y : (x ?= y ) = Gt <-> y <x.

Lemma compare_ge_iff x y : (x ?= y ) <> Lt <-> y <=x.

Lemma compare_ngt_iff x y : (x ?= y ) <> Gt <-> ~(y <x ).

Lemma compare_nlt_iff x y : (x ?= y ) <> Lt <-> ~(x <y ).

Lemma compare_nle_iff x y : (x ?= y ) = Gt <-> ~(x <=y ).

Lemma compare_nge_iff x y : (x ?= y ) = Lt <-> ~(y <=x ).

Lemma lt_irrefl x : ~ (x <x ).

Lemma lt_eq_cases n m : n <= m <-> n < m \/ n ==m.

End CompareBasedOrderFacts.

Basic facts about boolean comparisons

Module Type BoolOrderFacts
(Import E:EqLtLe')
(Import C:HasCmp E)
(Import F:HasBoolOrdFuns' E)
(Import O:CompareBasedOrder E C)
(Import S:BoolOrdSpecs E F).

Include CompareBasedOrderFacts E C O.

Nota : apart from eqb_compare below, facts about eqb are in BoolEqualityFacts

Alternate specifications based on BoolSpec and reflect

Lemma leb_spec0 x y : reflect (x <=y) (x <=?y).

Lemma leb_spec x y : BoolSpec (x <=y) (y <x) (x <=?y).

Lemma ltb_spec0 x y : reflect (x <y) (x <?y).

Lemma ltb_spec x y : BoolSpec (x <y) (y <=x) (x <?y).

Negated variants of the specifications

Lemma leb_nle x y : x <=? y = false <-> ~ (x <= y ).

Lemma leb_gt x y : x <=? y = false <-> y < x.

Lemma ltb_nlt x y : x <? y = false <-> ~ (x < y ).

Lemma ltb_ge x y : x <? y = false <-> y <= x.

Basic equality laws for boolean tests

Lemma leb_refl x : x <=? x = true.

Lemma leb_antisym x y : y <=? x = negb (x <? y).

Lemma ltb_irrefl x : x <? x = false.

Lemma ltb_antisym x y : y <? x = negb (x <=? y).

Relation between compare and the boolean comparisons

Lemma eqb_compare x y :
(x =? y ) = match compare x y with Eq => true | _ => false end.

Lemma ltb_compare x y :
(x <? y ) = match compare x y with Lt => true | _ => false end.

Lemma leb_compare x y :
(x <=? y ) = match compare x y with Gt => false | _ => true end.

End BoolOrderFacts.