orders.maps

Require Import
  abstract_algebra interfaces.orders orders.orders theory.setoids theory.strong_setoids.

Section strictly_order_preserving.
  Context `{StrictPartialOrder A} `{StrictPartialOrder B}.

  Global Instance strictly_order_preserving_inj `{!OrderPreserving (f : A B)} `{!StrongInjective f} :
    StrictlyOrderPreserving f | 20.

  Global Instance strictly_order_preserving_back_mor `{!OrderPreservingBack (f : A B)} `{!StrongSetoid_Morphism f} :
    StrictlyOrderPreservingBack f | 20.
End strictly_order_preserving.

Section strictly_order_preserving_dec.
  Context `{StrictPartialOrder A} `{!TrivialApart A} `{StrictPartialOrder B} `{!TrivialApart B}.

  Instance: StrongSetoid A := strict_po_setoid.
  Instance: StrongSetoid B := strict_po_setoid.

  Global Instance dec_strictly_order_preserving_inj `{!OrderPreserving (f : A B)} `{!Injective f} :
    StrictlyOrderPreserving f | 19.

  Global Instance dec_strictly_order_preserving_back_mor `{!OrderPreservingBack (f : A B)} :
    StrictlyOrderPreservingBack f | 19.
End strictly_order_preserving_dec.

Section pseudo_injective.
  Context `{PseudoOrder A} `{PseudoOrder B}.


  Instance pseudo_order_embedding_ext `{!StrictOrderEmbedding (f : A B)} :
    StrongSetoid_Morphism f.

  Lemma pseudo_order_embedding_inj `{!StrictOrderEmbedding (f : A B)} :
    StrongInjective f.
End pseudo_injective.

Section full_pseudo_strictly_preserving.
  Context `{FullPseudoOrder A} `{FullPseudoOrder B}.


  Lemma full_pseudo_order_preserving `{!StrictlyOrderPreservingBack (f : A B)} : OrderPreserving f.

  Lemma full_pseudo_order_preserving_back `{!StrictlyOrderPreserving (f : A B)} : OrderPreservingBack f.
End full_pseudo_strictly_preserving.

Section order_preserving_ops.
  Context `{Equiv R} `{Le R} `{Lt R}.

  Lemma order_preserving_flip `{!Commutative op} `{!Proper ((=) ==> (=) ==> (=)) op} `{!OrderPreserving (op z)} :
    OrderPreserving (λ y, op y z).

  Lemma strictly_order_preserving_flip `{!Commutative op} `{!Proper ((=) ==> (=) ==> (=)) op} `{!StrictlyOrderPreserving (op z)} :
    StrictlyOrderPreserving (λ y, op y z).

  Lemma order_preserving_back_flip `{!Commutative op} `{!Proper ((=) ==> (=) ==> (=)) op} `{!OrderPreservingBack (op z) } :
    OrderPreservingBack (λ y, op y z).

  Lemma strictly_order_preserving_back_flip `{!Commutative op} `{!Proper ((=) ==> (=) ==> (=)) op} `{!StrictlyOrderPreservingBack (op z) } :
    StrictlyOrderPreservingBack (λ y, op y z).

  Lemma order_preserving_nonneg (op : R R R) `{!RingZero R} `{ z, PropHolds (0 z) OrderPreserving (op z)} z :
    0 z OrderPreserving (op z).

  Lemma order_preserving_flip_nonneg (op : R R R) `{!RingZero R} `{ z, PropHolds (0 z) OrderPreserving (λ y, op y z)} z :
    0 z OrderPreserving (λ y, op y z).

  Lemma strictly_order_preserving_pos (op : R R R) `{!RingZero R} `{ z, PropHolds (0 < z) StrictlyOrderPreserving (op z)} z :
    0 < z StrictlyOrderPreserving (op z).

  Lemma strictly_order_preserving_flip_pos (op : R R R) `{!RingZero R} `{ z, PropHolds (0 < z) StrictlyOrderPreserving (λ y, op y z)} z :
    0 < z StrictlyOrderPreserving (λ y, op y z).

  Lemma order_preserving_back_pos (op : R R R) `{!RingZero R} `{ z, PropHolds (0 < z) OrderPreservingBack (op z)} z :
    0 < z OrderPreservingBack (op z).

  Lemma order_preserving_back_flip_pos (op : R R R) `{!RingZero R} `{ z, PropHolds (0 < z) OrderPreservingBack (λ y, op y z)} z :
    0 < z OrderPreservingBack (λ y, op y z).
End order_preserving_ops.

Lemma projected_partial_order `{Equiv A} `{Ale : Le A} `{Equiv B} `{Ble : Le B}
  (f : A B) `{!OrderEmbedding f} `{!Injective f} `{!PartialOrder Ble} : PartialOrder Ale.

Lemma projected_total_order `{Equiv A} `{Ale : Le A} `{Equiv B} `{Ble : Le B}
  (f : A B) `{!OrderEmbedding f} `{!TotalRelation Ble} : TotalRelation Ale.

Lemma projected_strict_order `{Equiv A} `{Alt : Lt A} `{Equiv B} `{Blt : Lt B}
  (f : A B) `{!StrictOrderEmbedding f} `{!StrictSetoidOrder Blt} : StrictSetoidOrder Alt.

Lemma projected_strict_setoid_order `{Equiv A} `{Alt : Lt A} `{Equiv B} `{Blt : Lt B}
  (f : A B) `{!StrictOrderEmbedding f} `{!StrictOrder Blt} : StrictOrder Alt.

Lemma projected_pseudo_order `{Equiv A} `{Apart A} `{Alt : Lt A} `{Equiv B} `{Apart B} `{Blt : Lt B}
  (f : A B) `{!StrictOrderEmbedding f} `{!StrongInjective f} `{!PseudoOrder Blt} : PseudoOrder Alt.

Lemma projected_full_pseudo_order `{Equiv A} `{Apart A} `{Ale : Le A} `{Alt : Lt A}
  `{Equiv B} `{Apart B} `{Ble : Le B} `{Blt : Lt B}
  (f : A B) `{!OrderEmbedding f} `{!StrictOrderEmbedding f} `{!StrongInjective f}
  `{!FullPseudoOrder Ble Blt} : FullPseudoOrder Ale Alt.

Instance id_order_morphism `{Setoid A} `{Le A} `{!Proper ((=) ==> (=) ==> iff) (≤)} : Order_Morphism (@id A) := {}.

Instance id_order_preserving `{Setoid A} `{Le A} `{!Proper ((=) ==> (=) ==> iff) (≤)} : OrderPreserving (@id A).

Instance id_order_preserving_back `{Setoid A} `{Le A} `{!Proper ((=) ==> (=) ==> iff) (≤)} : OrderPreservingBack (@id A).

Section composition.
  Context `{Equiv A} `{Equiv B} `{Equiv C} `{Le A} `{Le B} `{Le C}.

  Instance compose_order_morphism `{!Order_Morphism (f : A B)} `{!Order_Morphism (g : B C)} :
    Order_Morphism (g f).

  Instance compose_order_preserving `{!OrderPreserving (f : A B)} `{!OrderPreserving (g : B C)} :
    OrderPreserving (g f).

  Instance compose_order_preserving_back `{!OrderPreservingBack (f : A B)} `{!OrderPreservingBack (g : B C)} :
    OrderPreservingBack (g f).

  Instance compose_order_embedding `{!OrderEmbedding (f : A B)} `{!OrderEmbedding (g : B C)} :
    OrderEmbedding (g f) := {}.
End composition.

Hint Extern 4 (Order_Morphism (_ _)) => eapply @compose_order_morphism : typeclass_instances.
Hint Extern 4 (OrderPreserving (_ _)) => eapply @compose_order_preserving : typeclass_instances.
Hint Extern 4 (OrderPreservingBack (_ _)) => eapply @compose_order_preserving_back : typeclass_instances.
Hint Extern 4 (OrderEmbedding (_ _)) => eapply @compose_order_embedding : typeclass_instances.

Section propers.
  Context `{Equiv A} `{Equiv B} `{Le A} `{Le B}.

  Global Instance order_morphism_proper: Proper ((=) ==> iff) (@Order_Morphism A B _ _ _ _).

  Global Instance order_preserving_proper: Proper ((=) ==> iff) (@OrderPreserving A B _ _ _ _).

  Global Instance order_preserving_back_proper: Proper ((=) ==> iff) (@OrderPreservingBack A B _ _ _ _).

  Global Instance order_embedding_proper: Proper ((=) ==> iff) (@OrderEmbedding A B _ _ _ _).
End propers.