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