interfaces.orders

Require Import Morphisms abstract_algebra.


Class PartialOrder `{e: Equiv A} (o : Le A) : Prop :=
  { po_setoid : Setoid A
  ; po_proper:> Proper ((=) ==> (=) ==> iff) (≤)
  ; po_preorder:> PreOrder (≤)
  ; po_antisym:> AntiSymmetric (≤) }.

Class StrictSetoidOrder `{e : Equiv A} (o : Lt A) : Prop :=
  { strict_setoid_order_setoid : Setoid A
  ; strict_setoid_order_proper :> Proper ((=) ==> (=) ==> iff) (<)
  ; strict_setoid_order_strict :> StrictOrder (<) }.

Class PseudoOrder `{e : Equiv A} `{ap : Apart A} (so : Lt A) : Prop :=
  { pseudo_order_setoid : StrongSetoid A
  ; pseudo_order_antisym : x y, ¬(x < y y < x)
  ; pseudo_order_cotrans :> CoTransitive (<)
  ; apart_iff_total_lt : x y, x y x < y y < x }.

Class StrictPartialOrder `{e : Equiv A} `{ap : Apart A} (o : Le A) (so : Lt A) : Prop :=
  { strict_po_setoid : StrongSetoid A
  ; strict_po_po :> PartialOrder (≤)
  ; strict_po_trans :> Transitive (<)
  ; lt_iff_le_apart : x y, x < y x y x y }.

Class FullPseudoOrder `{e : Equiv A} `{ap : Apart A} (Ale : Le A) (Alt : Lt A) : Prop :=
  { full_pseudo_order_pseudo :> PseudoOrder Alt
  ; le_iff_not_lt_flip : x y, x y ¬y < x }.

Section order_maps.
  Context {A B : Type} {Ae: Equiv A} {Ale: Le A} {Alt: Lt A} {Be: Equiv B} {Ble: Le B} {Blt: Lt B} (f : A B).

  Class Order_Morphism :=
    { order_morphism_mor : Setoid_Morphism f
    ; order_morphism_proper_a :> Proper ((=) ==> (=) ==> iff) Ale
    ; order_morphism_proper_b :> Proper ((=) ==> (=) ==> iff) Ble }.

  Class StrictOrder_Morphism :=
    { strict_order_morphism_mor : Setoid_Morphism f
    ; strict_order_morphism_proper_a :> Proper ((=) ==> (=) ==> iff) Alt
    ; strict_order_morphism_proper_b :> Proper ((=) ==> (=) ==> iff) Blt }.

  Class OrderPreserving :=
    { order_preserving_morphism :> Order_Morphism
    ; order_preserving : `(x y f x f y) }.

  Class OrderPreservingBack :=
    { order_preserving_back_morphism :> Order_Morphism
    ; order_preserving_back : `(f x f y x y) }.

  Class OrderEmbedding :=
    { order_embedding_preserving :> OrderPreserving
    ; order_embedding_back :> OrderPreservingBack }.

  Class OrderIsomorphism `{!Inverse f} :=
    { order_iso_embedding :> OrderEmbedding
    ; order_iso_surjective :> Surjective f }.

  Class StrictlyOrderPreserving :=
    { strictly_order_preserving_morphism :> StrictOrder_Morphism
    ; strictly_order_preserving : `(x < y f x < f y) }.

  Class StrictlyOrderPreservingBack :=
    { strictly_order_preserving_back_morphism :> StrictOrder_Morphism
    ; strictly_order_preserving_back : `(f x < f y x < y) }.

  Class StrictOrderEmbedding :=
    { strict_order_embedding_preserving :> StrictlyOrderPreserving
    ; strict_order_embedding_back :> StrictlyOrderPreservingBack }.
End order_maps.

Class SemiRingOrder `{Equiv A} `{RingPlus A} `{RingMult A}
    `{RingZero A} (Ale : Le A) :=
  { srorder_po :> PartialOrder Ale
  ; srorder_partial_minus : x y, x y z, y = x + z
  ; srorder_plus :> z, OrderEmbedding (z +)
  ; nonneg_mult_compat : x y, PropHolds (0 x) PropHolds (0 y) PropHolds (0 x * y) }.

Class StrictSemiRingOrder `{Equiv A} `{RingPlus A} `{RingMult A}
    `{RingZero A} (Alt : Lt A) :=
  { strict_srorder_so :> StrictSetoidOrder Alt
  ; strict_srorder_partial_minus : x y, x < y z, y = x + z
  ; strict_srorder_plus :> z, StrictOrderEmbedding (z +)
  ; pos_mult_compat : x y, PropHolds (0 < x) PropHolds (0 < y) PropHolds (0 < x * y) }.

Class PseudoSemiRingOrder `{Equiv A} `{Apart A} `{RingPlus A}
    `{RingMult A} `{RingZero A} (Alt : Lt A) :=
  { pseudo_srorder_strict :> PseudoOrder Alt
  ; pseudo_srorder_partial_minus : x y, ¬y < x z, y = x + z
  ; pseudo_srorder_plus :> z, StrictOrderEmbedding (z +)
  ; pseudo_srorder_mult_ext :> StrongSetoid_BinaryMorphism (.*.)
  ; pseudo_srorder_pos_mult_compat : x y, PropHolds (0 < x) PropHolds (0 < y) PropHolds (0 < x * y) }.

Class FullPseudoSemiRingOrder `{Equiv A} `{Apart A} `{RingPlus A}
    `{RingMult A} `{RingZero A} (Ale : Le A) (Alt : Lt A) :=
  { full_pseudo_srorder_pso :> PseudoSemiRingOrder Alt
  ; full_pseudo_srorder_le_iff_not_lt_flip : x y, x y ¬y < x }.

Hint Extern 7 (PropHolds (0 < _ * _)) => eapply @pos_mult_compat : typeclass_instances.
Hint Extern 7 (PropHolds (0 _ * _)) => eapply @nonneg_mult_compat : typeclass_instances.