Require Import HoTT.Classes.interfaces.abstract_algebra.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

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 (≤) }.
#[export] Existing Instances
  po_hset
  po_hprop
  po_preorder
  po_antisym. 

Class TotalOrder `(Ale : Le A) :=
  { total_order_po : PartialOrder (≤)
  ; total_order_total : TotalRelation (≤) }.
#[export] Existing Instances
  total_order_po
  total_order_total.

(*
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 equavalence with the algebraic definition. We
do this in orders.lattices.
*)
Class MeetSemiLatticeOrder `(Ale : Le A) `{Meet A} :=
  { meet_sl_order : PartialOrder (≤)
  ; meet_lb_l : forall x y, x ⊓ y ≤ x
  ; meet_lb_r : forall x y, x ⊓ y ≤ y
  ; meet_glb : forall x y z, z ≤ x -> z ≤ y -> z ≤ x ⊓ y }.
#[export] Existing Instances meet_sl_order.

Class JoinSemiLatticeOrder `(Ale : Le A) `{Join A} :=
  { join_sl_order : PartialOrder (≤)
  ; join_ub_l : forall x y, x ≤ x ⊔ y
  ; join_ub_r : forall x y, y ≤ x ⊔ y
  ; join_lub : forall x y z, x ≤ z -> y ≤ z -> x ⊔ y ≤ z }.
#[export] Existing Instances join_sl_order.

Class LatticeOrder `(Ale : Le A) `{Meet A} `{Join A} :=
  { lattice_order_meet : MeetSemiLatticeOrder (≤)
  ; lattice_order_join : JoinSemiLatticeOrder (≤) }.
#[export] Existing Instances lattice_order_meet lattice_order_join.

Class StrictOrder `(Alt : Lt A) :=
  { strict_order_mere : is_mere_relation A lt
  ; strictorder_irrefl : Irreflexive (<)
  ; strictorder_trans : Transitive (<) }.
#[export] Existing Instances strict_order_mere strictorder_irrefl strictorder_trans.

(* 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 : forall x y, ~(x < y /\ y < x)
  ; pseudo_order_cotrans : CoTransitive (<)
  ; apart_iff_total_lt : forall x y, x ≶ y <-> x < y |_| y < x }.
#[export] Existing Instances pseudo_order_mere_lt pseudo_order_cotrans.

(* 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 : forall x y, x < y <-> x ≤ y /\ x ≶ y }.
#[export] Existing Instances strict_po_po strict_po_trans.

(* 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 : forall x y, x ≤ y <-> ~(y < x) }.
#[export] Existing Instances fullpseudo_le_hprop full_pseudo_order_pseudo.

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

  Class OrderPreserving := order_preserving : forall x y, (x ≤ y -> f x ≤ f y).

  Class OrderReflecting := order_reflecting : forall x y, (f x ≤ f y -> x ≤ y).

  Class OrderEmbedding :=
    { order_embedding_preserving : OrderPreserving
    ; order_embedding_reflecting : OrderReflecting }.
  #[export] Existing Instances order_embedding_preserving order_embedding_reflecting.
End order_maps.

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

  Class StrictlyOrderPreserving := strictly_order_preserving
    : forall x y, (x < y -> f x < f y).

  Class StrictlyOrderReflecting := strictly_order_reflecting
    : forall x y, (f x < f y -> x < y).

  Class StrictOrderEmbedding :=
    { strict_order_embedding_preserving : StrictlyOrderPreserving
    ; strict_order_embedding_reflecting : StrictlyOrderReflecting }.
  #[export] Existing Instances strict_order_embedding_preserving strict_order_embedding_reflecting.
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 : forall x y, x ≤ y -> exists z, y = x + z
  ; srorder_plus : forall z, OrderEmbedding (z +)
  ; nonneg_mult_compat : forall x y, PropHolds (0 ≤ x) -> PropHolds (0 ≤ y) ->
                                PropHolds (0 ≤ x * y) }.
#[export] Existing Instances srorder_po srorder_plus.

Class StrictSemiRingOrder `{Plus A} `{Mult A}
    `{Zero A} `{One A} (Alt : Lt A) :=
  { strict_srorder_so : StrictOrder Alt
  ; strict_srorder_partial_minus : forall x y, x < y -> exists z, y = x + z
  ; strict_srorder_plus : forall z, StrictOrderEmbedding (z +)
  ; pos_mult_compat : forall x y, PropHolds (0 < x) -> PropHolds (0 < y) ->
                             PropHolds (0 < x * y) }.
#[export] Existing Instances strict_srorder_so strict_srorder_plus.

Class PseudoSemiRingOrder `{Apart A} `{Plus A}
    `{Mult A} `{Zero A} `{One A} (Alt : Lt A) :=
  { pseudo_srorder_strict : PseudoOrder Alt
  ; pseudo_srorder_partial_minus : forall x y, ~(y < x) -> exists z, y = x + z
  ; pseudo_srorder_plus : forall z, StrictOrderEmbedding (z +)
  ; pseudo_srorder_mult_ext : StrongBinaryExtensionality (.*.)
  ; pseudo_srorder_pos_mult_compat : forall x y, PropHolds (0 < x) -> PropHolds (0 < y) ->
                                            PropHolds (0 < x * y) }.
#[export] Existing Instances pseudo_srorder_strict pseudo_srorder_plus pseudo_srorder_mult_ext.

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 : forall x y, x ≤ y <-> ~(y < x) }.
#[export] Existing Instances full_pseudo_srorder_le_hprop full_pseudo_srorder_pso.

(* 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 _ _ _
  }.
#[export] Existing Instances
  ordered_field_field
  ordered_field_lattice
  ordered_field_fssro.