Require Import base.

Module Pro.
  Polymorphic Cumulative Record mixin_of (T : Type) := Mixin {
    rel : T -> T -> Prop;
    _ : forall x, rel x x; (*reflexive rel;*)
    _ : forall x y z, rel x y -> rel y z -> rel x z (*transitive rel*)
  }.
  Notation class_of := mixin_of.

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

    Variable (T : Type) (cT : type).
    Definition class := let: Pack _ c _ := cT return class_of cT in c.

    Definition pack c := @Pack T c T.
    Definition clone c of phant_id class c := @Pack T c T.
  End ClassDef.

  Module Exports.
    Coercion sort : type >-> Sortclass.
    Notation proType := type.
    Notation ProMixin := Mixin.
    Notation ProType T m := (@pack T m).

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

Polymorphic Definition ord_op T := Pro.rel (Pro.class T).
Arguments ord_op {T} x y.

Delimit Scope ord_scope with ORD.
Open Scope ord_scope.

Notation "x ≤ y" := (ord_op x%ORD y%ORD)
  (at level 99, y at next level, no associativity) : ord_scope.
Notation "x ≤ y :> T" := ((x:T) ≤ (y:T))
  (at level 99, y at next level, no associativity) : ord_scope.

Section PreorderLemmas.
  Variable (T : proType).
  Implicit Types (x y z : T).

  Lemma le_refl x : x ≤ x.
  Proof. by case: T x => ?[]. Qed.

  Lemma le_trans x y z : (x ≤ y) -> (y ≤ z) -> (x ≤ z).
  Proof. by case: T x y z => ?[]. Qed.
End PreorderLemmas.

Arguments le_refl {T x}.
Arguments le_trans {T x} y {z} le_x_y le_y_z.
Hint Resolve le_refl.

Instance ord_op_rew (T : proType) : RewriteRelation (@ord_op T).
Instance ord_op_refl (T : proType) : Reflexive (@ord_op T) := @le_refl T.
Instance ord_op_trans (T : proType) : Transitive (@ord_op T) := @le_trans T.
Instance ord_op_preord (T : proType) : PreOrder (@ord_op T).
Proof. constructor; exact _. Qed.

Section InducedPreorder.
  Variable (T : Type) (X : proType) (f : T -> X).
  Implicit Types (x y z : T).

  Definition induced_le x y := f x ≤ f y.

  Lemma induced_le_refl x : induced_le x x. exact: le_refl. Qed.
  Lemma induced_le_trans : transitive induced_le. move=> x y z. exact: le_trans. Qed.

  Canonical induced_proMixin := ProMixin induced_le_refl induced_le_trans.
  Definition pack_induced_proType := Eval hnf in ProType T induced_proMixin.
End InducedPreorder.
Notation InducedProType T f := (@pack_induced_proType T _ f).

Definition reverse R : Type := R.

Section ReversePreorder.
  Variable (T : proType).
  Implicit Types (x y : reverse T).

  Definition rev_le x y := y ≤ x.

  Lemma reverse_le_refl x : rev_le x x. exact: le_refl. Qed.
  Lemma reverse_le_trans x y z : rev_le x y -> rev_le y z -> rev_le x z.
  Proof. move=> le_y_x le_z_y. exact: le_trans le_z_y le_y_x. Qed.

  Canonical reverse_proMixin := ProMixin reverse_le_refl reverse_le_trans.
  Canonical reverse_proType := Eval hnf in ProType (reverse T) reverse_proMixin.
End ReversePreorder.

Notation "T ^r" := (reverse T) (at level 2, format "T ^r") : type_scope.

Lemma rev_leE (T : proType) (x y : T^r) :
  (x ≤ y :> T^r) = (y ≤ x :> T).
Proof. by []. Qed.

Section LubPreorder.
  Variables (T : Type) (X : proType) (f : T -> X).

  Definition is_ub x := forall i, f i ≤ x.
  Definition is_lub x := forall y, (x ≤ y) <-> is_ub y.

  Lemma ubP x i : is_ub x -> f i ≤ x. exact. Qed.

  Lemma lub_ub x : is_lub x -> is_ub x.
  Proof. move=> lub i. by apply lub. Qed.
  Coercion lub_ub : is_lub >-> is_ub.

  Lemma lubP x y : is_lub x -> is_ub y -> x ≤ y.
  Proof. by move=> lub /lub. Qed.

  Lemma lubE x y : is_lub x -> (x ≤ y) = is_ub y.
  Proof. move=> h. apply: pext; by apply h. Qed.

  Lemma mk_lub x :
    is_ub x -> (forall y, is_ub y -> x ≤ y) -> is_lub x.
  Proof.
    move=> h1 h2 y; split; last by exact: h2. move=> le_x_y i.
    apply: le_trans le_x_y. exact: h1.
  Qed.
End LubPreorder.

Section GlbPreorder.
  Variables (T : Type) (X : proType) (f : T -> X).

  Definition is_lb x := forall i, x ≤ f i.
  Definition is_glb x := forall y, (y ≤ x) <-> is_lb y.

  Let Y := [proType of X^r].

  Lemma lbP x i : is_lb x -> x ≤ f i. exact: (@ubP T Y). Qed.

  Lemma glb_lb x : is_glb x -> is_lb x. exact: (@lub_ub T Y). Qed.
  Coercion glb_lb : is_glb >-> is_lb.

  Lemma glbP x y : is_glb x -> is_lb y -> y ≤ x. exact: (@lubP T Y). Qed.

  Lemma glbE x y : is_glb x -> (y ≤ x) = is_lb y. exact: (@lubE T Y). Qed.

  Lemma mk_glb x : is_lb x -> (forall y, is_lb y -> y ≤ x) -> is_glb x.
  Proof. exact: (@mk_lub T Y). Qed.
End GlbPreorder.