Ord.order

Require Import base.
Require Export preorder.

Module Ord.
  Record mixin_of (T : proType) := Mixin {
    _ : antisymmetric (@ord_op T)
  }.

  Section ClassDef.
    Record class_of (T : Type) := Class {
      base : Pro.class_of T;
      mixin : mixin_of (Pro.Pack base T)
    }.
    Local Coercion base : class_of >-> Pro.class_of.

    Structure type := Pack {sort; _ : class_of sort; _ : Type }.
    Local Coercion sort : type >-> Sortclass.

    Variable (T : Type) (cT : type).
    Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
    Definition clone c of phant_id class c := @Pack T c T.
    Let xT := let: Pack T _ _ := cT in T.
    Notation xclass := (class : class_of xT).

    Definition pack b0 (m0 : mixin_of (@Pro.Pack T b0 T)) :=
      fun bT b & phant_id (Pro.class bT) b =>
      fun m & phant_id m0 m => Pack (@Class T b m) T.

    Definition proType := @Pro.Pack cT xclass xT.
  End ClassDef.

  Module Exports.
    Coercion base : class_of >-> Pro.class_of.
    Coercion mixin : class_of >-> mixin_of.
    Coercion sort : type >-> Sortclass.

    Coercion proType : type >-> Pro.type.
    Canonical proType.

    Notation ordType := type.
    Notation OrdMixin := Mixin.
    Notation OrdType T m := (@pack T _ m _ _ id _ id).

    Notation "[ 'ordMixin' 'of' T ]" := (class _ : mixin_of T)
      (at level 0, format "[ 'ordMixin' 'of' T ]") : form_scope.
    Notation "[ 'ordType' 'of' T 'for' C ]" := (@clone T C _ idfun)
      (at level 0, format "[ 'ordType' 'of' T 'for' C ]") : form_scope.
    Notation "[ 'ordType' 'of' T ]" := (@clone T _ _ id)
      (at level 0, format "[ 'ordType' 'of' T ]") : form_scope.
  End Exports.
End Ord.
Export Ord.Exports.

Lemma le_eq {T : ordType} {x y : T} : x <= y -> y <= x -> x = y.
Proof. by case: T x y => ?[?[]]. Qed.

Section SubtypeOrder.
  Variable (T : Type) (X : ordType) (f : T -> X).
  Hypothesis f_inj : injective f.
  Implicit Types (x y : T).

  Lemma induced_le_eq x y : induced_le f x y -> induced_le f y x -> x = y.
  Proof. move=> h1 h2. apply: f_inj. exact: le_eq h1 h2. Qed.

  Canonical induced_ordMixin := @OrdMixin (induced_proType T f) induced_le_eq.
  Definition induced_ordType := Ord.Pack (Ord.Class induced_ordMixin) T.
End SubtypeOrder.
Arguments induced_ordType T {X f} f_inj.

Section ReverseOrder.
  Variable (T : ordType).
  Implicit Types (x y : reverse T).

  Lemma reverse_le_eq x y : x <= y -> y <= x -> x = y.
  Proof. move=> le_y_x le_x_y. exact: le_eq le_x_y le_y_x. Qed.

  Canonical reverse_ordMixin := OrdMixin reverse_le_eq.
  Canonical reverse_ordType := Eval hnf in OrdType (reverse T) reverse_ordMixin.
End ReverseOrder.

Section NatOrder.
  Implicit Types (m n : nat).

  Lemma nat_le_eq m n : m <= n -> n <= m -> m = n.
  Proof.
    rewrite/ord_op/=/nat_le. move=> le_m_n le_n_k. apply: anti_leq.
      by rewrite le_m_n.
  Qed.

  Canonical nat_ordMixin := OrdMixin nat_le_eq.
  Canonical nat_ordType := Eval hnf in OrdType nat nat_ordMixin.
End NatOrder.

Section PropOrder.
  Implicit Types (P Q : Prop).

  Lemma prop_le_eq P Q : P <= Q -> Q <= P -> P = Q.
  Proof. exact: pext. Qed.

  Canonical prop_ordMixin := OrdMixin prop_le_eq.
  Canonical prop_ordType := Eval hnf in OrdType Prop prop_ordMixin.
End PropOrder.

Section PairOrder.
  Variable (X Y : ordType).
  Implicit Types (p q : X * Y).

  Lemma pair_le_eq p q : p <= q -> q <= p -> p = q.
  Proof.
    move: p q => [a1 b1] [a2 b2] [/=r1 s1] [/=r2 s2]. f_equal; exact: le_eq.
  Qed.

  Canonical pair_ordMixin := OrdMixin pair_le_eq.
  Canonical pair_ordType := Eval hnf in OrdType (X * Y) pair_ordMixin.
End PairOrder.

Section IProdOrder.
  Variables (T : Type) (F : T -> ordType).
  Implicit Types (f g : iprod F).

  Lemma iprod_le_eq f g : f <= g -> g <= f -> f = g.
  Proof. move=> le_f_g le_g_f. apply: fext => x. exact: le_eq. Qed.

  Canonical iprod_ordMixin := OrdMixin iprod_le_eq.
  Canonical iprod_ordType := Eval hnf in OrdType (iprod F) iprod_ordMixin.
End IProdOrder.

Canonical prod_ordType (T : Type) (X : ordType) :=
  Eval hnf in OrdType (T -> X) (@iprod_ordMixin T (fun _ => X)).

Canonical mfun_ordType (X : proType) (Y : ordType) :=
  Eval hnf in induced_ordType {mono X -> Y} (@mfun_eq X Y).

Section LubOrder.
  Variables (T : Type) (X : ordType) (f : T -> X).

  Lemma lub_uniq x y : is_lub f x -> is_lub f y -> x = y.
  Proof.
    move=> h1 h2. apply: le_eq; by [exact: lubP h1 h2|exact: lubP h2 h1].
  Qed.
End LubOrder.

Section GlbOrder.
  Variables (T : Type) (X : ordType) (f : T -> X).
  Let Y := [ordType of X^r].

  Lemma glb_uniq x y : is_glb f x -> is_glb f y -> x = y.
  Proof. exact: (@lub_uniq T Y). Qed.
End GlbOrder.