orders.orders

Require Import
  abstract_algebra interfaces.orders strong_setoids.

Lemma le_flip `{Le A} `{!TotalRelation (≤)} x y : ¬y x x y.

Section partial_order.
  Context `{PartialOrder A}.

  Instance: Setoid A := po_setoid.

  Lemma eq_le x y : x = y x y.

  Lemma eq_le_flip x y : x = y y x.

  Lemma not_le_ne x y : ¬x y x y.
End partial_order.

Section strict_order.
  Context `{StrictSetoidOrder A}.

  Instance: Setoid A := strict_setoid_order_setoid.

  Lemma lt_flip x y : x < y ¬(y < x).

  Lemma lt_antisym x y : ¬(x < y < x).

  Lemma lt_ne x y : x < y x y.

  Lemma lt_ne_flip x y : x < y y x.

  Lemma eq_not_lt x y : x = y ¬x < y.
End strict_order.

Section pseudo_order.
  Context `{PseudoOrder A}.

  Instance: StrongSetoid A := pseudo_order_setoid.

  Lemma apart_total_lt x y : x y x < y y < x.

  Lemma pseudo_order_lt_apart x y : x < y x y.

  Lemma pseudo_order_lt_apart_flip x y : x < y y x.

  Lemma not_lt_apart_lt_flip x y : ¬x < y x y y < x.

  Lemma pseudo_order_cotrans_twice x₁ y₁ x₂ y₂ : x₁ < y₁ x₂ < y₂ x₁ < x₂ y₂ < y₁.

  Lemma pseudo_order_lt_ext x₁ y₁ x₂ y₂ : x₁ < y₁ x₂ < y₂ x₁ x₂ y₂ y₁.

  Instance: Proper ((=) ==> (=) ==> iff) (<).

  Global Instance: StrictSetoidOrder (_ : Lt A).

  Global Instance: Transitive (complement (<)).

  Global Instance: AntiSymmetric (complement (<)).

  Lemma ne_total_lt `{!TrivialApart A} x y : x y x < y y < x.

  Global Instance lt_trichotomy `{!TrivialApart A} `{ x y, Decision (x = y)} : Trichotomy (<).
End pseudo_order.

Section strict_partial_order.
  Context `{StrictPartialOrder A}.

  Instance: StrongSetoid A := strict_po_setoid.

  Instance strict_po_apart_ne x y : PropHolds (x y) PropHolds (x y).

  Global Instance apart_proper: Proper ((=) ==> (=) ==> iff) (⪥).

  Global Instance: StrictSetoidOrder (_ : Lt A).

  Lemma lt_le x y : PropHolds (x < y) PropHolds (x y).

  Lemma not_le_not_lt x y : ¬x y ¬x < y.

  Lemma lt_apart x y : x < y x y.

  Lemma lt_apart_flip x y : x < y y x.

  Lemma le_not_lt_flip x y : y x ¬x < y.

  Lemma lt_not_le_flip x y : y < x ¬x y.

  Lemma lt_le_trans x y z : x < y y z x < z.

  Lemma le_lt_trans x y z : x y y < z x < z.

  Lemma lt_iff_le_ne `{!TrivialApart A} x y : x < y x y x y.

  Lemma le_equiv_lt `{!TrivialApart A} `{ x y, Decision (x = y)} x y : x y x = y x < y.

  Program Instance dec_from_lt_dec `{!TrivialApart A} `{ x y, Decision (x y)} :
      x y, Decision (x = y) := λ x y,
    match decide_rel (≤) x y with
    | left E1 => match decide_rel (≤) y x with
       | left E2 => left _
       | right E2 => right _
       end
     | right E1 => right _
     end.

  Definition lt_dec_slow `{!TrivialApart A} `{ x y, Decision (x y)} :
     x y, Decision (x < y).
End strict_partial_order.

Hint Extern 5 (PropHolds (_ _)) => eapply @strict_po_apart_ne : typeclass_instances.
Hint Extern 10 (PropHolds (_ _)) => eapply @lt_le : typeclass_instances.
Hint Extern 20 (Decision (_ < _)) => eapply @lt_dec_slow : typeclass_instances.

Section full_pseudo_order.
  Context `{FullPseudoOrder A}.

  Instance: StrongSetoid A := pseudo_order_setoid.

  Lemma not_lt_le_flip x y : ¬y < x x y.

  Instance: PartialOrder (_ : Le A).

  Global Instance: StrictPartialOrder (_ : Le A) (_ : Lt A).

  Global Instance: x y, Stable (x y).

  Lemma le_or_lt `{!TrivialApart A} `{ x y, Decision (x = y)} x y : x y y < x.

  Global Instance le_total `{!TrivialApart A} `{ x y, Decision (x = y)} : TotalRelation (≤).

  Lemma not_le_lt_flip `{!TrivialApart A} `{ x y, Decision (x = y)} x y : ¬y x x < y.


  Program Definition lt_dec `{!TrivialApart A} `{ x y, Decision (x y)} :
       x y, Decision (x < y) := λ x y,
    match decide_rel (≤) y x with
    | left E => right _
    | right E => left _
    end.
End full_pseudo_order.

Hint Extern 8 (Decision (_ < _)) => eapply @lt_dec : typeclass_instances.

Section dec_partial_order.
  Context `{PartialOrder A} `{ x y, Decision (x = y)}.

  Instance: Setoid A := po_setoid.
  Definition dec_lt: Lt A := λ x y, x y x y.

  Context `{Lt A} (lt_correct : x y, x < y x y x y).

  Instance dec_order: StrictSetoidOrder (<).

  Context `{Apart A} `{!TrivialApart A}.

  Instance: StrongSetoid A := dec_strong_setoid.

  Instance dec_strict_partial_order: StrictPartialOrder (≤) (<).

  Context `{!TotalRelation (≤)}.

  Instance dec_pseudo_order: PseudoOrder (<).

  Instance dec_full_pseudo_order: FullPseudoOrder (≤) (<).
End dec_partial_order.