Library HoTT.Classes.interfaces.orders

Require Import HoTT.Classes.interfaces.abstract_algebra.

Generalizable Variables A.

In this file we describe interfaces for ordered structures. Since we are in a constructive setting we use a pseudo order instead of a total order. Therefore we also have to include an apartness relation.
Obviously, in case we consider decidable structures these interfaces are quite inconvenient. Hence we will, later on, provide means to go back and forth between the usual classical notions and these constructive notions.
On the one hand, if we have an ordinary (total) partial order (≤) with a corresponding strict order (<), we will prove that we can construct a FullPartialOrder and PseudoPartialOrder, respectively.
On the other hand, if equality is decidable, we will prove that we have the usual properties like Trichotomy (<) and TotalRelation (≤).

Class PartialOrder `(Ale : Le A) :=
  { po_hset :: IsHSet A
  ; po_hprop :: is_mere_relation A Ale
  ; po_preorder :: PreOrder (≤)
  ; po_antisym :: AntiSymmetric (≤) }.

Class TotalOrder `(Ale : Le A) :=
  { total_order_po :: PartialOrder (≤)
  ; total_order_total :: TotalRelation (≤) }.

(*
We define a variant of the order theoretic definition of meet and join
semilattices. Notice that we include a meet operation instead of the
more common:
  forall x y, exists m, m ≤ x /\ m ≤ y /\ forall z, z ≤ x -> z ≤ y -> m ≤ z
Our definition is both stronger and more convenient than the above.
This is needed to prove equivalence with the algebraic definition. We
do this in orders.lattices.
*)
Class MeetSemiLatticeOrder `(Ale : Le A) `{Meet A} :=
  { meet_sl_order :: PartialOrder (≤)
  ; meet_lb_l : ∀ x y, x ⊓ y ≤ x
  ; meet_lb_r : ∀ x y, x ⊓ y ≤ y
  ; meet_glb : ∀ x y z, z ≤ x → z ≤ y → z ≤ x ⊓ y }.

Class JoinSemiLatticeOrder `(Ale : Le A) `{Join A} :=
  { join_sl_order :: PartialOrder (≤)
  ; join_ub_l : ∀ x y, x ≤ x ⊔ y
  ; join_ub_r : ∀ x y, y ≤ x ⊔ y
  ; join_lub : ∀ x y z, x ≤ z → y ≤ z → x ⊔ y ≤ z }.

Class LatticeOrder `(Ale : Le A) `{Meet A} `{Join A} :=
  { lattice_order_meet :: MeetSemiLatticeOrder (≤)
  ; lattice_order_join :: JoinSemiLatticeOrder (≤) }.

Class StrictOrder `(Alt : Lt A) :=
  { strict_order_mere :: is_mere_relation A lt
  ; strictorder_irrefl :: Irreflexive (<)
  ; strictorder_trans :: Transitive (<) }.

The constructive notion of a total strict total order. We will prove that (<) is in fact a StrictOrder.
Class PseudoOrder `{Aap : Apart A} (Alt : Lt A) :=
{ pseudo_order_apart : IsApart A
  ; pseudo_order_mere_lt :: is_mere_relation A lt
  ; 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 }.

A partial order (≤) with a corresponding (<). We will prove that (<) is in fact a StrictOrder
Class FullPartialOrder `{Aap : Apart A} (Ale : Le A) (Alt : Lt A) :=
  { strict_po_apart : IsApart A
  ; strict_po_mere_lt : is_mere_relation A lt
  ; strict_po_po :: PartialOrder (≤)
  ; strict_po_trans :: Transitive (<)
  ; lt_iff_le_apart : ∀ x y, x < y ↔ x ≤ y ∧ x ≶ y }.

A pseudo order (<) with a corresponding (≤). We will prove that (≤) is in fact a PartialOrder.
Class FullPseudoOrder `{Aap : Apart A} (Ale : Le A) (Alt : Lt A) :=
  { fullpseudo_le_hprop :: is_mere_relation A Ale
  ; full_pseudo_order_pseudo :: PseudoOrder Alt
  ; le_iff_not_lt_flip : ∀ x y, x ≤ y ↔ ~(y < x) }.

Section order_maps.
  Context {A B : Type} {Ale: Le A} {Ble: Le B}(f : A → B).

  Class OrderPreserving := order_preserving : ∀ x y, (x ≤ y → f x ≤ f y).

  Class OrderReflecting := order_reflecting : ∀ x y, (f x ≤ f y → x ≤ y).

  Class OrderEmbedding :=
    { order_embedding_preserving :: OrderPreserving
    ; order_embedding_reflecting :: OrderReflecting }.

End order_maps.

Section srorder_maps.
  Context {A B : Type} {Alt: Lt A} {Blt: Lt B} (f : A → B).

  Class StrictlyOrderPreserving := strictly_order_preserving
    : ∀ x y, (x < y → f x < f y).

  Class StrictlyOrderReflecting := strictly_order_reflecting
    : ∀ x y, (f x < f y → x < y).

  Class StrictOrderEmbedding :=
    { strict_order_embedding_preserving :: StrictlyOrderPreserving
    ; strict_order_embedding_reflecting :: StrictlyOrderReflecting }.

End srorder_maps.

#[export]
Hint Extern 4 (?f _ ≤ ?f _) ⇒ apply (order_preserving f) : core.
#[export]
Hint Extern 4 (?f _ < ?f _) ⇒ apply (strictly_order_preserving f) : core.

We define various classes to describe the order on the lower part of the algebraic hierarchy. This results in the notion of a PseudoSemiRingOrder, which specifies the order on the naturals, integers, rationals and reals. This notion is quite similar to a strictly linearly ordered unital commutative protoring in Davorin Lešnik's PhD thesis.
Class SemiRingOrder `{Plus A} `{Mult A}
    `{Zero A} `{One 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 `{Plus A} `{Mult A}
    `{Zero A} `{One A} (Alt : Lt A) :=
  { strict_srorder_so :: StrictOrder 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 `{Apart A} `{Plus A}
    `{Mult A} `{Zero A} `{One 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 :: StrongBinaryExtensionality (.*.)
  ; pseudo_srorder_pos_mult_compat : ∀ x y, PropHolds (0 < x) → PropHolds (0 < y) →
                                            PropHolds (0 < x × y) }.

Class FullPseudoSemiRingOrder `{Apart A} `{Plus A}
    `{Mult A} `{Zero A} `{One A} (Ale : Le A) (Alt : Lt A) :=
  { full_pseudo_srorder_le_hprop :: is_mere_relation A Ale
  ; full_pseudo_srorder_pso :: PseudoSemiRingOrder Alt
  ; full_pseudo_srorder_le_iff_not_lt_flip : ∀ x y, x ≤ y ↔ ~(y < x) }.

(* Due to bug 2528 *)
#[export]
Hint Extern 7 (PropHolds (0 < _ × _)) ⇒
  eapply @pos_mult_compat : typeclass_instances.
#[export]
Hint Extern 7 (PropHolds (0 ≤ _ × _)) ⇒
  eapply @nonneg_mult_compat : typeclass_instances.

(*
Alternatively, we could have defined the standard notion of a RingOrder:

Class RingOrder `{Equiv A} `{Plus A} `{Mult A} `{Zero A} (Ale : Le A) :=
  { ringorder_po :> PartialOrder Ale
  ; ringorder_plus :> forall z, OrderPreserving (z +)
  ; ringorder_mult : forall x y, 0 ≤ x -> 0 ≤ y -> 0 ≤ x * y }.

Unfortunately, this notion is too weak when we consider semirings (e.g. the
naturals). Moreover, in case of rings, we prove that this notion is equivalent
to our SemiRingOrder class (see orders.rings.from_ring_order). Hence we omit
defining such a class.

Similarly we prove that a FullSemiRingOrder
and a FullPseudoRingOrder are equivalent.

Class FullPseudoRingOrder `{Apart A} `{Plus A}
    `{Mult A} `{Zero A} (Ale : Le A) (Alt : Lt A) :=
  { pseudo_ringorder_spo :> FullPseudoOrder Ale Alt
  ; pseudo_ringorder_mult_ext :> StrongSetoid_BinaryMorphism (.*.)
  ; pseudo_ringorder_plus :> forall z, StrictlyOrderPreserving (z +)
  ; pseudo_ringorder_mult : forall x y, 0 < x -> 0 < y -> 0 < x * y }.
*)

(* Next, a constructive definition of fields - the ordered fields from
HoTT book chapter 11. *)

Class OrderedField (A : Type) {Alt : Lt A} {Ale : Le A} {Aap : Apart A} {Azero : Zero A}
      {Aone : One A} {Aplus : Plus A} {Anegate : Negate A} {Amult : Mult A}
      {Arecip : Recip A} {Ajoin : Join A} {Ameet : Meet A} :=
  { ordered_field_field :: @IsField A Aplus Amult Azero Aone Anegate Aap Arecip
  ; ordered_field_lattice :: LatticeOrder Ale
  ; ordered_field_fssro :: @FullPseudoSemiRingOrder A _ _ _ Azero _ _ _
  }.