Ord.clat

Require Import base order adjunction jlat mlat lat.

Module CLat.
  Record mixin_of (X : lat) := Mixin {
    sup : forall (T : Type), (T -> X) -> X;
    inf : forall (T : Type), (T -> X) -> X;
    _ : forall T (F : T -> X), is_lub F (sup F);
    _ : forall T (F : T -> X), is_glb F (inf F)
  }.

  Section ClassDef.
    Record class_of (T : Type) := Class {
      base : Lat.class_of T;
      mixin : mixin_of (Lat.Pack base T)
    }. Set Printing All.
    Local Coercion base : class_of >-> Lat.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 b0 (m0 : mixin_of (@Lat.Pack T b0 T)) :=
      fun bT b & phant_id (Lat.class bT) b =>
      fun m & phant_id m0 m => Pack (@Class T b m) 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.
    Definition lat := @Lat.Pack cT xclass xT.
  End ClassDef.

  Module Exports.
    Coercion base : class_of >-> Lat.class_of.
    Coercion mixin : class_of >-> mixin_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 lat : type >-> Lat.type.
    Canonical lat.

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

Definition sup {X : clat} {T : Type} (F : T -> X) : X := CLat.sup (CLat.class X) F.
Definition inf {X : clat} {T : Type} (F : T -> X) : X := CLat.inf (CLat.class X) F.

Section CLatAxioms.
  Variable (X : clat).

  Lemma sup_axiom T (F : T -> X) : is_lub F (sup F).
  Proof. by case: X F => [?[?[]]]. Qed.

  Lemma inf_axiom T (F : T -> X) : is_glb F (inf F).
  Proof. by case: X F => [?[?[]]]. Qed.
End CLatAxioms.
Arguments sup_axiom {X T F} y.
Arguments inf_axiom {X T F} y.

Notation "\sup_ i F" := (sup (fun i => F%ORD))
  (at level 36, F at level 36, i at level 0,
           format "'[' \sup_ i '/ ' F ']'") : ord_scope.
Notation "\sup_ ( i : t ) F" := (sup (fun (i : t) => F%ORD))
  (at level 36, F at level 36, i at level 50,
           only parsing) : ord_scope.
Notation "\sup_ ( i | P ) F" := (\sup_i \sup_(_ : P) F%ORD)
  (at level 36, F at level 36, i at level 50,
           format "'[' \sup_ ( i | P ) '/ ' F ']'") : ord_scope.
Notation "\sup_ ( i : t | P ) F" := (\sup_(i : t) \sup_(_ : P) F%ORD)
  (at level 36, F at level 36, i at level 50,
           only parsing) : ord_scope.

Notation "\inf_ i F" := (inf (fun i => F%ORD))
  (at level 36, F at level 36, i at level 0,
           format "'[' \inf_ i '/ ' F ']'") : ord_scope.
Notation "\inf_ ( i : t ) F" := (inf (fun (i : t) => F%ORD))
  (at level 36, F at level 36, i at level 50,
           only parsing) : ord_scope.
Notation "\inf_ ( i | P ) F" := (\inf_i \inf_(_ : P) F%ORD)
  (at level 36, F at level 36, i at level 50,
           format "'[' \inf_ ( i | P ) '/ ' F ']'") : ord_scope.
Notation "\inf_ ( i : t | P ) F" := (\inf_(i : t) \inf_(_ : P) F%ORD)
  (at level 36, F at level 36, i at level 50,
           only parsing) : ord_scope.

Section CLatLemmas.
  Variable (X : clat).

  Lemma supE T (F : T -> X) (x : X) :
    (forall i, F i <= x) -> sup F <= x.
  Proof. exact: lubP sup_axiom. Qed.

  Lemma infI T (F : T -> X) (x : X) :
    (forall i, x <= F i) -> x <= inf F.
  Proof. exact: glbP inf_axiom. Qed.

  Lemma supI T (F : T -> X) (x : X) (i : T) :
    x <= F i -> x <= sup F.
  Proof. move->. apply: ubP sup_axiom. Qed.

  Lemma infE T (F : T -> X) (x : X) (i : T) :
    F i <= x -> inf F <= x.
  Proof. move<-. apply: lbP inf_axiom. Qed.

  Lemma supEc T (F : T -> X) (P : T -> Prop) (x : X) :
    (forall i, P i -> F i <= x) -> \sup_(i | P i) F i <= x.
  Proof.
    move=> h. apply: supE => i. apply: supE => p. exact: h.
  Qed.

  Lemma infIc T (F : T -> X) (P : T -> Prop) (x : X) :
    (forall i, P i -> x <= F i) -> x <= \inf_(i | P i) F i.
  Proof.
    move=> h. apply: infI => i. apply: infI => p. exact: h.
  Qed.

  Lemma supIc T (F : T -> X) (P : T -> Prop) (x : X) (i : T) :
    P i -> x <= F i -> x <= \sup_(i | P i) F i.
  Proof.
    move=> p ->. apply: supI (i) _. exact: supI p _.
  Qed.

  Lemma infEc T (F : T -> X) (P : T -> Prop) (x : X) (i : T) :
    P i -> F i <= x -> \inf_(i | P i) F i <= x.
  Proof.
    move=> p <-. apply: infE (i) _. exact: infE p _.
  Qed.
End CLatLemmas.
Arguments supI {X T} F {x} i le_x_fi : rename.
Arguments supIc {X T} F P {x} i pi le_x_fi : rename.
Arguments infE {X T} F {x} i le_fi_x : rename.
Arguments infEc {X T} F P {x} i pi le_fi_x : rename.

Instance sup_monotone (T : Type) (X : clat) : monotone (@sup X T).
Proof. move=> f g le_f_g. apply: supE => i. exact: supI (i) _. Qed.

Instance inf_monotone (T : Type) (X : clat) : monotone (@inf X T).
Proof. move=> f g le_f_g. apply: infI => i. exact: infE (i) _. Qed.

(* cuts for faster type class inference *)
Instance sup_le_proper (T : Type) (X : clat) :
  Proper (ord_op ++> ord_op) (@sup X T).
Proof. exact _. Qed.

Instance inf_le_proper (T : Type) (X : clat) :
  Proper (ord_op ++> ord_op) (@sup X T).
Proof. exact _. Qed.

Instance sup_proper (T : Type) (X : clat) :
  Proper (pointwise_relation T eq ==> eq) (@sup X T).
Proof.
  move=> F G e. congr sup. apply: fext => i. exact: e.
Qed.

Instance inf_proper (T : Type) (X : clat) :
  Proper (pointwise_relation T eq ==> eq) (@inf X T).
Proof.
  move=> F G e. congr inf. apply: fext => i. exact: e.
Qed.

Section BigopLemmas.
  Variable (X : clat).
  Implicit Types (x y z : X).

  Lemma sup_sup T (P : T -> Type) (F : forall i, P i -> X) :
    \sup_i \sup_(j : P i) F i j = \sup_p F (tag p) (tagged p).
  Proof.
    apply: le_eq. apply: supE => i. apply: supE => j.
    exact: supI (existT _ i j) _. apply: supE => -[i j]/=.
    exact/supI/supI.
  Qed.

  Lemma inf_inf T (P : T -> Type) (F : forall i, P i -> X) :
    \inf_i \inf_(j : P i) F i j = \inf_p F (tag p) (tagged p).
  Proof.
    apply: le_eq. apply: infI => -[i pi]/=. exact/infE/infE.
    apply: infI => i. apply: infI => pi. exact: infE (existT _ i pi) _.
  Qed.

  Lemma supK T (x : X) (i : T) : \sup_(i : T) x = x.
  Proof. apply: le_eq. exact: supE. exact: supI. Qed.

  Lemma supKc T (P : T -> Prop) (x : X) (i : T) :
    P i -> \sup_(i | P i) x = x.
  Proof. move=> p. rewrite sup_sup supK //. by exists i. Qed.

  Lemma supB T : \sup_(i : T) bot = bot :> X.
  Proof. apply: bot_eq. exact: supE. Qed.

  Lemma supBc T (P : T -> Prop) : \sup_(i | P i) bot = bot :> X.
  Proof. by rewrite sup_sup supB. Qed.

  Lemma supJ T (F G : T -> X) :
    \sup_i (F i \cup G i) = sup F \cup sup G.
  Proof.
    apply: le_eq. apply: supE => i. apply: joinE. apply: joinIl. exact: supI.
    apply: joinIr. exact: supI. apply: joinE; apply: supE => i; apply: supI (i) _.
    exact: joinIl. exact: joinIr.
  Qed.

  Lemma supJc T (P : T -> Prop) (F G : T -> X) :
    \sup_(i | P i) (F i \cup G i) = (\sup_(i | P i) F i) \cup (\sup_(i | P i) G i).
  Proof. by rewrite !sup_sup supJ. Qed.

  Lemma supJl T (F : T -> X) (x : X) (i : T) :
    \sup_i (x \cup F i) = x \cup sup F.
  Proof. by rewrite supJ supK. Qed.

  Lemma supJr T (F : T -> X) (x : X) (i : T) :
    \sup_i (F i \cup x) = sup F \cup x.
  Proof. by rewrite supJ supK. Qed.

  Lemma supJcl T (P : T -> Prop) (F : T -> X) (x : X) (i : T) :
    P i -> \sup_(i | P i) (x \cup F i) = x \cup \sup_(i | P i) F i.
  Proof. move=> p. by rewrite supJc (supKc x p). Qed.

  Lemma supJcr T (P : T -> Prop) (F : T -> X) (x : X) (i : T) :
    P i -> \sup_(i | P i) (F i \cup x) = (\sup_(i | P i) F i) \cup x.
  Proof. move=> p. by rewrite supJc (supKc x p). Qed.

  (* The above for inf *)
  Lemma infK T (x : X) (i : T) : \inf_(i : T) x = x.
  Proof. apply: le_eq. exact: infE. exact: infI. Qed.

  Lemma infKc T (P : T -> Prop) (x : X) (i : T) :
    P i -> \inf_(i | P i) x = x.
  Proof. move=> p. rewrite inf_inf infK //. by exists i. Qed.

  Lemma infT T : \inf_(i : T) top = top :> X.
  Proof. apply: top_eq. exact: infI. Qed.

  Lemma infTc T (P : T -> Prop) : \inf_(i | P i) top = top :> X.
  Proof. by rewrite inf_inf infT. Qed.

  Lemma infM T (F G : T -> X) :
    \inf_i (F i \cap G i) = inf F \cap inf G.
  Proof.
    apply: le_eq. apply: meetI; apply: infI => i; apply: infE (i) _.
    exact: meetEl. exact: meetEr. apply: infI => i. apply: meetI.
    apply: meetEl. exact: infE. apply: meetEr. exact: infE.
  Qed.

  Lemma infMc T (P : T -> Prop) (F G : T -> X) :
    \inf_(i | P i) (F i \cap G i) = (\inf_(i | P i) F i) \cap (\inf_(i | P i) G i).
  Proof. by rewrite !inf_inf infM. Qed.

  Lemma infMl T (F : T -> X) (x : X) (i : T) :
    \inf_i (x \cap F i) = x \cap inf F.
  Proof. by rewrite infM infK. Qed.

  Lemma infMr T (F : T -> X) (x : X) (i : T) :
    \inf_i (F i \cap x) = inf F \cap x.
  Proof. by rewrite infM infK. Qed.

  Lemma infMcl T (P : T -> Prop) (F : T -> X) (x : X) (i : T) :
    P i -> \inf_(i | P i) (x \cap F i) = x \cap \inf_(i | P i) F i.
  Proof. move=> p. by rewrite infMc (infKc x p). Qed.

  Lemma infMcr T (P : T -> Prop) (F : T -> X) (x : X) (i : T) :
    P i -> \inf_(i | P i) (F i \cap x) = (\inf_(i | P i) F i) \cap x.
  Proof. move=> p. by rewrite infMc (infKc x p). Qed.

  Lemma sup_le I J (F : I -> X) (G : J -> X) :
    (forall i, exists j, F i <= G j) -> sup F <= sup G.
  Proof.
    move=> h. apply: supE => i. case: (h i) => j le_fi_gj. exact: supI (j) _.
  Qed.

  Lemma sup_lec I J (P : I -> Prop) (Q : J -> Prop) (F : I -> X) (G : J -> X) :
    (forall i, P i -> exists j, Q j /\ F i <= G j) ->
    \sup_(i | P i) F i <= \sup_(j | Q j) G j.
  Proof.
    move=> h. rewrite !sup_sup. apply: sup_le => -[i pi] /=.
    case: (h i pi) => j [qj le_fi_gj]. by exists (existT Q j qj).
  Qed.

  Lemma sup_eqc I (P Q : I -> Prop) (F G : I -> X) :
    (forall i, P i <-> Q i) ->
    (forall i, P i -> F i = G i) ->
    \sup_(i | P i) F i = \sup_(i | Q i) G i.
  Proof.
    move=> h1 h2. apply: le_eq. apply: sup_lec => i pi. exists i. split.
    exact/h1. by rewrite h2. apply: sup_lec => i qi. exists i. split.
    exact/h1. rewrite h2 //. exact/h1.
  Qed.

  Lemma inf_le I J (F : I -> X) (G : J -> X) :
    (forall j, exists i, F i <= G j) -> inf F <= inf G.
  Proof.
    move=> h. apply: infI => j. case: (h j) => i le_fi_gj. exact: infE (i) _.
  Qed.

  Lemma inf_lec I J (P : I -> Prop) (Q : J -> Prop) (F : I -> X) (G : J -> X) :
    (forall j, Q j -> exists i, P i /\ F i <= G j) ->
    \inf_(i | P i) F i <= \inf_(j | Q j) G j.
  Proof.
    move=> h. rewrite !inf_inf. apply: inf_le => -[j qj] /=.
    case: (h j qj) => i [pi le_fi_gj]. by exists (existT P i pi).
  Qed.

  Lemma inf_eqc I (P Q : I -> Prop) (F G : I -> X) :
    (forall i, P i <-> Q i) ->
    (forall i, Q i -> F i = G i) ->
    \inf_(i | P i) F i = \inf_(i | Q i) G i.
  Proof.
    move=> h1 h2. apply: le_eq. apply: inf_lec => i pi. exists i. split.
    exact/h1. by rewrite h2. apply: inf_lec => i qi. exists i. split.
    exact/h1. rewrite h2 //. exact/h1.
  Qed.

  Lemma suplat_join x y :
    x \cup y = \sup_(b : bool) (if b then x else y).
  Proof.
    apply: le_eq. apply: joinE. exact: supI true _. exact: supI false _.
    apply: supE => -[] /=. exact: joinIl. exact: joinIr.
  Qed.

  Lemma suplat_meet x y :
    x \cap y = \sup_(z | z <= x /\ z <= y) z.
  Proof.
    apply: le_eq.
    - apply: supIc (x \cap y) _ _ => //; split. exact: meetEl. exact: meetEr.
    - apply: supEc => z [le_z_x le_z_y]. exact: meetI.
  Qed.

  Lemma suplat_inf T (F : T -> X) :
    inf F = \sup_(x | is_lb F x) x.
  Proof.
    apply: le_eq. apply: supIc (inf F) _ _ => //. exact: inf_axiom.
    apply: supEc => s. exact: infI.
  Qed.

  Lemma suplat_infc T (P : T -> Prop) (F : T -> X) :
    \inf_(i | P i) F i = \sup_(x | forall i, P i -> x <= F i) x.
  Proof.
    rewrite inf_inf suplat_inf. apply: sup_eqc => // i.
    split=> [h j pj|h [j pj]/=]. exact: (h (existT P j pj)). exact: h.
  Qed.

  Lemma suplat_top : top = \sup_x x :> X.
  Proof. symmetry. apply: top_eq. exact: supI. Qed.

  Lemma suplat_bot : bot = \sup_(b : False) (match b with end) :> X.
  Proof. symmetry. apply: bot_eq. exact: supE. Qed.

  Lemma inflat_meet x y :
    x \cap y = \inf_(b : bool) (if b then x else y).
  Proof.
    apply: le_eq. apply: infI => -[]. exact: meetEl. exact: meetEr.
    apply: meetI. exact: infE true _. exact: infE false _.
  Qed.

  Lemma inflat_join x y :
    x \cup y = \inf_(z | x <= z /\ y <= z) z.
  Proof.
    apply: le_eq.
    - apply: infIc => z [le_x_z le_y_z]. exact: joinE.
    - apply: infEc (x \cup y) _ _ => //; split. exact: joinIl. exact: joinIr.
  Qed.

  Lemma inflat_sup T (F : T -> X) :
    sup F = \inf_(x | is_ub F x) x.
  Proof.
    apply: le_eq. apply: infIc => x lb. exact: supE.
    apply: infEc (sup F) _ _ => //. exact: sup_axiom.
  Qed.

  Lemma inflat_supc T (P : T -> Prop) (F : T -> X) :
    \sup_(i | P i) F i = \inf_(x | forall i, P i -> F i <= x) x.
  Proof.
    rewrite sup_sup inflat_sup. apply: inf_eqc => // j.
    split=> [h i pi|h [i pi]/=]. exact: (h (existT P i pi)). exact: h.
  Qed.

  Lemma inflat_bot : bot = \inf_x x :> X.
  Proof. symmetry. apply: bot_eq. exact: infE. Qed.

  Lemma inflat_top : top = \inf_(b : False) (match b with end) :> X.
  Proof. symmetry. apply: top_eq. exact: infI. Qed.
End BigopLemmas.

Section CLatMFun.
  Variable (X Y : clat) (f : X -> Y).
  Context {fP : monotone f}.

  Lemma mono_sup T (F : T -> X) : \sup_i f (F i) <= f (sup F).
  Proof. apply: supE => i. apply: mono. exact: supI. Qed.

  Lemma mono_supc T (P : T -> Prop) (F : T -> X) :
    \sup_(i | P i) f (F i) <= f (\sup_(i | P i) F i).
  Proof. by rewrite !sup_sup mono_sup. Qed.

  Lemma mono_inf T (F : T -> X) : f (inf F) <= \inf_i f (F i).
  Proof. apply: infI => i. apply: mono. exact: infE. Qed.

  Lemma mono_infc T (P : T -> Prop) (F : T -> X) :
    f (\inf_(i | P i) F i) <= \inf_(i | P i) f (F i).
  Proof. by rewrite !inf_inf mono_inf. Qed.
End CLatMFun.

Section CLatAdjunction.
  Variable (X Y : clat) (f : X -> Y).
  Context {g : Y -> X} {fP : is_adjunction f g}.

  Lemma adj_sup T (F : T -> X) :
    f (sup F) = \sup_i f (F i).
  Proof.
    apply: lub_uniq sup_axiom. apply: adj_lub. exact: sup_axiom.
  Qed.

  Lemma adj_inf T (F : T -> Y) : f^* (inf F) = \inf_i f^* (F i).
  Proof.
    apply: glb_uniq inf_axiom. apply: adj_glb. exact: inf_axiom.
  Qed.

  Lemma adj_supc T (F : T -> X) (P : T -> Prop) :
    f (\sup_(i | P i) F i) = \sup_(i | P i) f (F i).
  Proof. by rewrite !sup_sup adj_sup. Qed.

  Lemma adj_infc T (F : T -> Y) (P : T -> Prop) :
    f^* (\inf_(i | P i) F i) = \inf_(i | P i) f^* (F i).
  Proof. by rewrite !inf_inf adj_inf. Qed.
End CLatAdjunction.

Section SupAdjunction.
  Variable (X Y : clat) (f : X -> Y).
  Hypothesis fS : forall I (F : I -> X), f (sup F) <= \sup_i f (F i).
  Context {fP : monotone f}.

  Definition aceil (y : Y) : X := \sup_(x | f x <= y) x.

  Lemma aceilP : is_adjunction f aceil.
  Proof.
    split=> h. exact: supIc (x) h _.
    rewrite h /aceil sup_sup fS. by apply: supE => -[].
  Qed.
End SupAdjunction.

Section InfAdjunction.
  Variable (X Y : clat) (f : X -> Y).
  Hypothesis fI : forall I (F : I -> X), \inf_i f (F i) <= f (inf F).
  Context {fP : monotone f}.

  Definition afloor (y : Y) : X := \inf_(x | y <= f x) x.

  Lemma afloorP : is_adjunction afloor f.
  Proof.
    split=> h; last by exact: infEc (y) h _.
    rewrite -h /afloor inf_inf -fI. by apply: infI => -[].
  Qed.
End InfAdjunction.

Section CLatClosure.
  Variable (X : clat) (c : X -> X).
  Context {cP : is_closure c}.

  Lemma closure_sup T (F : T -> X) :
    c (\sup_i c (F i)) = c (sup F).
  Proof.
    apply: closure_lub sup_axiom. exact: sup_axiom.
  Qed.

  Lemma closure_supc T (P : T -> Prop) (F : T -> X) :
    c (\sup_(i | P i) c (F i)) = c (\sup_(i | P i) (F i)).
  Proof. by rewrite !sup_sup closure_sup. Qed.

  Lemma closure_inf T (F : T -> X) :
    c (\inf_i c (F i)) = \inf_i c (F i).
  Proof. exact: closure_glb inf_axiom. Qed.

  Lemma closure_infc T (P : T -> Prop) (F : T -> X) :
    c (\inf_(i | P i) c (F i)) = \inf_(i | P i) c (F i).
  Proof. by rewrite !inf_inf closure_inf. Qed.
End CLatClosure.

Section CLatKernel.
  Variable (X : clat) (k : X -> X).
  Context {kP : is_kernel k}.

  Lemma kernel_inf T (F : T -> X) :
    k (\inf_i k (F i)) = k (inf F).
  Proof.
    apply: kernel_glb inf_axiom. exact: inf_axiom.
  Qed.

  Lemma kernel_infc T (F : T -> X) (P : T -> Prop) :
    k (\inf_(i | P i) k (F i)) = k (\inf_(i | P i) (F i)).
  Proof. by rewrite !inf_inf kernel_inf. Qed.
End CLatKernel.

Canonical reverse_clatMixin (X : clat) :=
  @CLatMixin (reverse_lat X) (@inf X) (@sup X) (@inf_axiom X) (@sup_axiom X).
Canonical reverse_clat (X : clat) := Eval hnf in CLat X^r (reverse_clatMixin X).

Section PropCLat.
  Variables (T : Type) (F : T -> Prop).

  Definition prop_sup := exists x, F x.
  Definition prop_inf := forall x, F x.

  Lemma prop_le_sup : is_lub F prop_sup. by firstorder. Qed.
  Lemma prop_le_inf : is_glb F prop_inf. by firstorder. Qed.
End PropCLat.

Canonical prop_clatMixin := CLatMixin (@prop_le_sup) (@prop_le_inf).
Canonical prop_clat := Eval hnf in CLat Prop prop_clatMixin.

Section PairCLat.
  Variables (X Y : clat).

  Definition pair_sup T (F : T -> X * Y) := (sup (fst \o F), sup (snd \o F)).
  Definition pair_inf T (F : T -> X * Y) := (inf (fst \o F), inf (snd \o F)).

  Lemma pair_le_sup T (F : T -> X * Y) : is_lub F (pair_sup F).
  Proof.
    apply: mk_lub => [i|[x y] ub]. split; apply: supI; exact: le_refl.
    split; apply: supE => i /=; by case: (ub i).
  Qed.

  Lemma pair_le_inf T (F : T -> X * Y) : is_glb F (pair_inf F).
  Proof.
    apply: mk_glb => [i|[x y] lb]. split; apply: infE; exact: le_refl.
    split; apply: infI => i /=; by case: (lb i).
  Qed.

  Canonical pair_clatMixin := CLatMixin pair_le_sup pair_le_inf.
  Canonical pair_clat := Eval hnf in CLat (X * Y) pair_clatMixin.
End PairCLat.

Section IProdCLat.
  Variable (A : Type) (B : A -> clat).

  Definition iprod_sup T (F : T -> iprod B) : iprod B :=
    fun x => sup (F^~ x).
  Definition iprod_inf T (F : T -> iprod B) : iprod B :=
    fun x => inf (F^~ x).

  Lemma iprod_le_sup T (F : T -> iprod B) : is_lub F (iprod_sup F).
  Proof.
    apply: mk_lub => [i x|f ub x]. exact: supI. apply: supE => i. exact: ub.
  Qed.

  Lemma iprod_le_inf T (F : T -> iprod B) : is_glb F (iprod_inf F).
  Proof.
    apply: mk_glb => [i x|f lb x]. exact: infE. apply: infI => i. exact: lb.
  Qed.

  Canonical iprod_clatMixin := CLatMixin iprod_le_sup iprod_le_inf.
  Canonical iprod_clat := Eval hnf in CLat (iprod B) iprod_clatMixin.
End IProdCLat.

Canonical prod_clatType (A : Type) (B : clat) :=
  Eval hnf in CLat (A -> B) (@iprod_clatMixin A (fun _ => B)).

Instance sup_monotone_prod (T : Type) (X : proType) (Y : clat) (F : T -> X -> Y ) :
  (forall i, monotone (F i)) -> monotone (sup F).
Proof.
  move=> h x y le_x_y /=. apply: supE => i. apply: supI (i) _. exact: mono.
Qed.

Instance inf_monotone_prod (T : Type) (X : proType) (Y : clat) (F : T -> X -> Y) :
  (forall i, monotone (F i)) -> monotone (inf F).
Proof.
  move=> h x y le_x_y /=. apply: infI => i. apply: infE (i) _. exact: mono.
Qed.

Section MFunCLat.
  Variable (A : proType) (B : clat).

  Definition mfun_sup T (F : T -> {mono A -> B}) : {mono A -> B} :=
    mfun (sup (F : T -> A -> B)).

  Definition mfun_inf T (F : T -> {mono A -> B}) : {mono A -> B} :=
    mfun (inf (F : T -> A -> B)).

  Lemma mfun_le_sup T (F : T -> {mono A -> B}) : is_lub F (mfun_sup F).
  Proof. exact: iprod_le_sup. Qed.

  Lemma mfun_le_inf T (F : T -> {mono A -> B}) : is_glb F (mfun_inf F).
  Proof. exact: iprod_le_inf. Qed.

  Canonical mfun_clatMixin := CLatMixin mfun_le_sup mfun_le_inf.
  Canonical mfun_clat := Eval hnf in CLat {mono A -> B} mfun_clatMixin.
End MFunCLat.

Definition prop_emb {X : clat} (P : Prop) : X := \sup_(p : P) top.

Instance prop_emb_adjunction {X : clat} : is_adjunction (@prop_emb X) (ord_op top).
Proof.
  move=>/= P x. split=> [lex p|h].
  - rewrite -lex. exact: supI.
  - apply: supE => p. exact: h.
Qed.

Notation "'{{' P '}}'" := (prop_emb P) : ord_scope.

Lemma embI (X : clat) (P : Prop) (x : X) : P -> x <= {{P}}.
Proof. move=> p. apply: supI => //. exact: topI. Qed.

Lemma embE (X : clat) (P : Prop) (x : X) : (P -> top <= x) -> {{P}} <= x.
Proof. move=> np. exact: supE. Qed.

Lemma embt (X : clat) (P : Prop) : P -> {{P}} = top :> X.
Proof. move=> p. apply: top_eq. exact: embI. Qed.

Lemma embf (X : clat) (P : Prop) : ~P -> {{P}} = bot :> X.
Proof. move=> np. apply: bot_eq. exact: embE. Qed.

Lemma embT (X : clat) : {{True}} = top :> X.
Proof. exact: embt. Qed.

Lemma embB (X : clat) : {{False}} = bot :> X.
Proof. exact: embf. Qed.

Lemma embJ (X : clat) (P Q : Prop) :
  {{P \/ Q}} = {{P}} \cup {{Q}} :> X.
Proof. exact: adjJ. Qed.

Lemma emb_sup (X : clat) T (P : T -> Prop) :
  {{exists i, P i}} = \sup_(i : T) {{P i}} :> X.
Proof. exact: adj_sup. Qed.

Lemma emb_supc (X : clat) T (P Q : T -> Prop) :
  {{exists i, P i /\ Q i}} = \sup_(i | P i) {{Q i}} :> X.
Proof.
  rewrite emb_sup. apply: le_eq; apply: mono => i.
  - apply: embE => -[pi qi]. apply: supI => //. exact: embI.
  - apply: supE => pi. apply: embE => qi. exact: embI.
Qed.

Lemma le_emb (X : clat) (P Q : Prop) : (P -> Q) -> {{P}} <= {{Q}} :> X.
Proof. move=> h. by apply: embE => /h/embt->. Qed.

(* Most of the nice reasoning principles for the brackets only hold in Frames,
   not in arbitrary complete lattices. The development above will be continued there. *)

Section SupLattice.
  Variable (X : ordType) (sup : forall T, (T -> X) -> X).
  Hypothesis supP : forall T (F : T -> X), is_lub F (sup F).
  Implicit Types (x y z : X).

  Definition clat_sup_bot := sup (fun b : False => match b with end).

  Lemma clat_sup_botP x : clat_sup_bot <= x.
  Proof. by apply/supP => -[]. Qed.

  Definition clat_sup_top := sup id.

  Lemma clat_sup_topP x : x <= clat_sup_top.
  Proof. apply: ubP. exact: supP. Qed.

  Definition clat_sup_join x y := sup (pairb x y).

  Lemma clat_sup_joinP x y : is_lub (pairb x y) (clat_sup_join x y).
  Proof. exact: supP. Qed.

  Definition clat_sup_inf T (F : T -> X) := @sup (sig (is_lb F)) sval.

  Lemma clat_sup_infP T (F : T -> X) :
    is_glb F (clat_sup_inf F).
  Proof.
    apply: mk_glb.
    - move=> x. apply/supP => -[y /=]. exact.
    - move=> y lb. rewrite/clat_sup_inf.
      change y with (sval (exist _ y lb)).
      apply: ubP. exact: supP.
  Qed.

  Definition clat_sup_meet x y := clat_sup_inf (pairb x y).

  Lemma clat_sup_meetP x y : is_glb (pairb x y) (clat_sup_meet x y).
  Proof. exact: clat_sup_infP. Qed.

  (* We need to package this structure together somehow... *)
  Canonical clat_sup_jlatMixin :=
    @JLatMixin (Ord.Pack (Ord.class X) X) _ _ clat_sup_botP clat_sup_joinP.
  Canonical clat_sup_mlatMixin :=
    @MLatMixin (Ord.Pack (Ord.class X) X) _ _ clat_sup_topP clat_sup_meetP.
  Definition supLat :=
    Eval hnf in Lat.Pack (Lat.Class clat_sup_jlatMixin clat_sup_mlatMixin) X.
  Canonical clat_sup_clatMixin :=
    @CLatMixin supLat sup clat_sup_inf supP clat_sup_infP.
  Definition supCLat :=
    Eval hnf in CLat.Pack (@CLat.Class X (Lat.class supLat) clat_sup_clatMixin) X.
End SupLattice.

Section InfLattice.
  Variable (X : ordType) (inf : forall T, (T -> X) -> X).
  Hypothesis infP : forall T (F : T -> X), is_glb F (inf F).
  Implicit Types (x y z : X).

  (*
  Definition inf_jlatMixin := @clat_sup_mlatMixin (reverse_ordType X) inf infP.
  Definition inf_mlatMixin := @clat_sup_jlatMixin (reverse_ordType X) inf infP.
  Definition inf_clatMixin := @clat_sup_clatMixin (reverse_ordType X) inf infP.
   *)
  (*
  Definition infLatClass :=
    (Lat.Class (@clat_sup_jlatMixin (reverse_ordType X) inf infP)
               (@clat_sup_mlatMixin (reverse_ordType X) inf infP)).
  Definition infLat  := Eval hnf in @Lat.Pack X
    (Lat.Class (@clat_sup_jlatMixin (reverse_ordType X) inf infP)
               (@clat_sup_mlatMixin (reverse_ordType X) inf infP)) X.
  Definition infCLatClass :=
    @CLat.Class X (Lat.class infLat) (@clat_sup_clatMixin (reverse_ordType X) inf infP).
  Definition infCLat := Eval hnf in @CLat.Pack X infCLatClass X.
   *)
End InfLattice.