Require Import Bool Basics OrdersTac.
Require Export Orders.

Set Implicit Arguments.

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

 Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order.

 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.

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

 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.

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

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

  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.

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.

Module OrderedTypeRev (O:OrderedTypeFull) <: OrderedTypeFull.

Definition t := O.t.
Definition eq := O.eq.
Program 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.

Unset Implicit Arguments.

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.

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.

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

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.

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

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.