semantics.ord.ordtype

Require Import base protype.

Module Ord.
  Polymorphic Cumulative Record mixin_of (T : proType) := Mixin {
    _ : forall x y : T, x ≤ y -> y ≤ x -> x = y (*antisymmetric (@ord_op T)*)
  }.

  Section ClassDef.
    Polymorphic Cumulative 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)) :=
      [find pt | Pro.sort pt ~ T | "is not a proType"]
      [find pe | Pro.class pt ~ pe]
      [find m | m ~ m0 | "is not the right mixin"]
      @Pack T (@Class T pe 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 _ 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 InducedOrder.
  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 (@pack_induced_proType T X f) induced_le_eq.
  Definition pack_induced_ordType :=
    [find pt | Pro.sort pt ~ T | "is not a proType"]
    [find pe | Pro.class pt ~ pe]
    fun (_ : unify pe (@induced_proMixin T X f) (Some "is not an induced proType")) =>
    [find m | m ~ induced_ordMixin]
      @Ord.Pack T (@Ord.Class T pe m) T.
End InducedOrder.
Notation InducedOrdType T f_inj := (@pack_induced_ordType T _ _ f_inj _ idfun _ idfun idfun _ idfun).

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 T^r reverse_ordMixin.
End ReverseOrder.

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.