Ord.lat

Require Import base order adjunction jlat mlat.

Module Lat.
  Section ClassDef.
    Record class_of (T : Type) := Class {
      base : Ord.class_of T;
      jmixin : JLat.mixin_of (Ord.Pack base T);
      mmixin : MLat.mixin_of (Ord.Pack base T)
    }.
    Local Coercion base : class_of >-> Ord.class_of.

    Definition jmixin_of T (c : class_of T) : JLat.class_of T :=
      @JLat.Class T (base c) (jmixin c).
    Local Coercion jmixin_of : class_of >-> JLat.class_of.

    Definition mmixin_of T (c : class_of T) : MLat.class_of T :=
      @MLat.Class T (base c) (mmixin c).
    Local Coercion mmixin_of : class_of >-> MLat.class_of.

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

    Variables (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 :=
      fun (b : ordType) & phant_id (Ord.sort b) T =>
      fun (bc : Ord.class_of _) & phant_id (Ord.class b) bc =>
      fun (jm : JLat.mixin_of (@Ord.Pack T bc T)) =>
      fun (mm : MLat.mixin_of (@Ord.Pack T bc T)) => Pack (@Class T bc jm mm) T.

    Definition proType := @Pro.Pack cT xclass xT.
    Definition ordType := @Ord.Pack cT xclass xT.
    Definition jlat := @JLat.Pack cT xclass xT.
    Definition mlat := @MLat.Pack cT xclass xT.
  End ClassDef.

  Module Exports.
    Coercion base : class_of >-> Ord.class_of.
    Coercion sort : type >-> Sortclass.

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

    Coercion ordType : type >-> Ord.type.
    Canonical ordType.

    Coercion jlat : type >-> JLat.type.
    Canonical jlat.

    Coercion mlat : type >-> MLat.type.
    Canonical mlat.

    Coercion jmixin_of : class_of >-> JLat.class_of.
    Coercion mmixin_of : class_of >-> MLat.class_of.

    Notation lat := type.
    Notation Lat T j m := (@pack T _ id _ id j m).
    Notation "[ 'lat' 'of' T ]" := (@clone T _ _ id)
      (at level 0, format "[ 'lat' 'of' T ]") : form_scope.
  End Exports.
End Lat.
Export Lat.Exports.

Section LatticeLaws.
  Variable (X : lat).
  Implicit Types (x y z : X).

  Lemma meetxK x y : x \cap (y \cup x) = x.
  Proof. apply: le_eq. exact: meetEl. apply: meetI => //. exact: joinIr. Qed.

  Lemma meetKx x y : x \cap (x \cup y) = x.
  Proof. rewrite joinC. exact: meetxK. Qed.

  Lemma joinxK x y : x \cup (y \cap x) = x.
  Proof. apply: le_eq. apply: joinE => //. exact: meetEr. exact: joinIl. Qed.

  Lemma joinKx x y : x \cup (x \cap y) = x.
  Proof. rewrite meetC. exact: joinxK. Qed.

  Lemma joinTx x : (top : X) \cup x = top.
  Proof. apply: top_eq. exact: joinIl. Qed.

  Lemma joinxT x : x \cup top = top.
  Proof. by rewrite joinC joinTx. Qed.

  Lemma meetBx x : (bot : X) \cap x = bot.
  Proof. apply: bot_eq. exact: meetEl. Qed.

  Lemma meetxB x : x \cap bot = bot.
  Proof. by rewrite meetC meetBx. Qed.

  (* the one direction of distributivity which holds in an arbitrary lattice *)
  (*
  Lemma join_dist_le x y z :
    x \cup (y \cap z) <= (x \cup y) \cap (x \cup z).
  Proof.
    apply: joinP. apply: meetP; exact: joinL.
    apply: meetP. apply: meetL. exact: joinR. apply: meetR. exact: joinR.
  Qed.
  *)
End LatticeLaws.

(*
Example mono_anti_const {X : Lat} {Y : ordType} (f : {mono X -> Y}) :
  antitone f -> forall x y, f x = f y.
Proof.
  move=> af. suff: forall x y, f x <= f y. move=> h x y. apply: le_eq; exact: h.
  move=> x y. rewrite (@join_left _ x y) -{2}(@meet_right _ x y). apply: af.
  rewrite rev_leE. apply: joinL. exact: meetL.
Qed.
 *)

Canonical reverse_lat (T : lat) :=
  Eval hnf in Lat T^r (reverse_jlatMixin T) (reverse_mlatMixin T).

Canonical prop_lat := Eval hnf in Lat Prop prop_jlatMixin prop_mlatMixin.

Canonical pair_lat (X Y : lat) :=
  Eval hnf in Lat (X * Y) (pair_jlatMixin X Y) (pair_mlatMixin X Y).

Canonical iprod_lat (T : Type) (F : T -> lat) :=
  Eval hnf in Lat (iprod F) (iprod_jlatMixin F) (iprod_mlatMixin F).

Canonical prod_lat (T : Type) (X : lat) :=
  Eval hnf in Lat (T -> X) (@iprod_jlatMixin T (fun _ => X)) (@iprod_mlatMixin T (fun _ => X)).

Canonical mfun_lat (X : proType) (Y : lat) :=
  Eval hnf in Lat {mono X -> Y} (mfun_jlatMixin X Y) (mfun_mlatMixin X Y).

Instance is_adjunction_bot {X Y : lat} : is_adjunction (bot : X -> Y) (top : Y -> X).
Proof. move=> x y. split=> h. exact: topI. exact: botE. Qed.

Instance is_adjunction_join {X Y : lat} (f g : X -> Y) {fr gr : Y -> X}
         {fP : is_adjunction f fr} {gP : is_adjunction g gr} :
  is_adjunction (f \cup g) (fr \cap gr).
Proof.
  move=> x y. split=> [<-|->].
  - apply: meetI; rewrite -adjP. exact: joinIl. exact: joinIr.
  - apply: joinE; rewrite adjP. exact: meetEl. exact: meetEr.
Qed.

Section AdjunctionJLat.
  Variables (X Y : lat).
  Implicit Types (f g : {adj X -> Y}).

  Definition adj_bot : {adj X -> Y} := adj bot.
  Definition adj_join f g : {adj X -> Y} := adj ((f : X -> Y) \cup g).

  Lemma adj_le_bot f : adj_bot <= f.
  Proof. move => x /=. exact: botE. Qed.

  Lemma adj_le_join f g : is_lub (pairb f g) (adj_join f g).
  Proof.
    apply: mk_join. exact: joinIl. exact: joinIr. move=> /= h l1 l2. exact: joinE.
  Qed.

  Canonical adj_jlatMixin := JLatMixin adj_le_bot adj_le_join.
  Canonical adj_jlat := Eval hnf in JLat {adj X -> Y} adj_jlatMixin.
End AdjunctionJLat.