Library lattices.AdjoinBot

Require Import FunctionalExtensionality.
Require Import PropExtensionality.
Require Import Classical.
Require Import ClassicalChoice.
Require Import structures.Category.
Require Import structures.Lattice.
Require Import structures.Completion.
Require Import lattices.Upset.
Require Import lattices.FCD.

Module Lazy <: LatticeCategory.

  Section DEF.
    Context {L M : cdlattice} (f : L → M).

    Class NSupMorphism :=
      mor_sup: ∀ {I} (x : I → L), inhabited I → f (lsup x) = lsup (f @ x).

    Class Morphism := mor : NSupMorphism ∧ Inf.Morphism f.
    Global Instance cmor_sup : Morphism → NSupMorphism := @proj1 _ _.
    Global Instance cmor_inf : Morphism → Inf.Morphism f := @proj2 _ _.

    Global Instance mor_ref :
      Morphism → PosetMorphism f.
  End DEF.

  Lemma id_mor (L : cdlattice) :
    Morphism (fun x:L ⇒ x).

  Lemma compose_mor {A B C : cdlattice} (g : B → C) (f : A → B) :
    Morphism f →
    Morphism g →
    Morphism (fun a ⇒ g (f a)).

End Lazy.

Module LBot.

  Inductive opt {A} :=
    mkopt (s : A → Prop) (Hs : ∀ a b, s a → s b → a = b).

  Arguments opt : clear implicits.
  Definition is {A} : opt A → A → Prop := fun '(mkopt a _) ⇒ a.

  Lemma is_unique {A} (x : opt A) (a b : A) :
    is x a → is x b → a = b.

  Lemma opt_eq {A} (x y : opt A) :
    (∀ a, is x a ↔ is y a) → x = y.

  Section DEF.
    Context {L M : cdlattice}.

    Program Definition Fposet : poset :=
      {|
        poset_carrier := opt L;
        ref x y := ∀ l, is x l → ∃ m, is y m ∧ ref l m;
      |}.

    Definition proj (x : opt L) : L :=
      sup {l | is x l}, l.

    Lemma proj_is x l :
      is x l → proj x = l.

    Definition sup_of {I} (x : I → opt L) (l : L) :=
      (∃ i, ∃ li, is (x i) li) ∧
      sup i, proj (x i) = l.

    Definition inf_of {I} (x : I → opt L) (l : L) :=
      (∀ i, ∃ li, is (x i) li) ∧
      inf i, proj (x i) = l.

    Definition sup_inf_of {I J} (x : ∀ i:I, J i → opt L) (l : L) :=
      (∃ i, ∀ j, ∃ li, is (x i j) li) ∧
      sup i, inf j, proj (x i j) = l.

    Definition inf_sup_of {I J} (x : ∀ i:I, J i → opt L) (l : L) :=
      (∀ i, ∃ j, ∃ li, is (x i j) li) ∧
      inf i, sup j, proj (x i j) = l.

    Lemma sup_inf_of_cd {I J} (x : ∀ i:I, J i → opt L) (l : L) :
      sup_inf_of x l ↔
      inf_sup_of (fun f i ⇒ x i (f i)) l.

    Hint Unfold sup_of inf_of.

    Program Definition F : cdlattice :=
      {|
        cdl_poset := Fposet;
        lsup I x := mkopt (sup_of x) _;
        linf I x := mkopt (inf_of x) _;
      |}.

    Program Definition emb (l : L) : F := mkopt (eq l) _.

    Global Instance emb_mor :
      Lazy.Morphism emb.

    (*
    Lemma emb_mor c1 c2 :
      emb c1 ⊑ emb c2 -> c1 ⊑ c2.
    Proof.
      unfold emb. cbn.
      split.
      - intros H. destruct (H c1) as (? & ? & ?); auto. congruence.
      - intros H l Hl. subst. eauto.
    Qed.
     *)

    Lemma cases x :
      x = bot ∨ ∃ l, x = emb l.

    Lemma sup_cases {I} (x : I → F) :
      (lsup x = bot ∧
       ∀ i, x i = bot) ∨
      (lsup x = emb (sup {l | ∃ i, is (x i) l}, l) ∧
       ∃ i l, is (x i) l).

    Definition ext (f : L → M) (x : F) : M :=
      sup {l | is x l}, f l.

    Context {f : L → M} `{Hf : !Lazy.Morphism f}.

    Lemma ext_bot :
      ext f bot = bot.
Local Transparent bot.
    Lemma ext_ana :
      (∀ x, ext f (emb x) = f x).

    Instance ext_mor :
      CDL.Morphism (ext f).

    Lemma ext_unique (g : F → M) `{Hg : !CDL.Morphism g} :
      (∀ x, g (emb x) = f x) → ∀ x, g x = ext f x.

  End DEF.

End LBot.