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.
    Proof.
      intros [_ H].
      apply Inf.mor_ref; auto.
    Qed.
  End DEF.

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

  Lemma compose_mor {A B C : cdlattice} (g : B → C) (f : A → B) :
    Morphism f →
    Morphism g →
    Morphism (fun a ⇒ g (f a)).
  Proof.
    split.
    - intros I x Hx. rewrite (mor_sup f), (mor_sup g); auto.
    - apply Inf.compose_mor; typeclasses eauto.
  Qed.

End Lazy.

Module LBot.

We construct the extended the lattice with a new ⊥ by using sets with at most one element.

  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.
  Proof.
    destruct x; auto.
  Qed.

  Lemma opt_eq {A} (x y : opt A) :
    (∀ a, is x a ↔ is y a) → x = y.
  Proof.
    destruct x as [x Hx], y as [y Hy]. cbn. intros H.
    cut (x = y).
    - intro. subst. f_equal. apply proof_irrelevance.
    - apply functional_extensionality. intro.
      apply propositional_extensionality; auto.
  Qed.

  Section DEF.
    Context {L M : cdlattice}.

Poset


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

    Next Obligation.
      split.
      - firstorder.
      - intros [x Hx] [y Hy] [z Hz] Hxy Hyz l Hl. cbn in ×.
        destruct (Hxy l) as (m & Hm & Hlm); auto.
        destruct (Hyz m) as (n & Hn & Hmn); auto.
        ∃ n. split; auto. transitivity m; auto.
    Qed.

    Next Obligation.
      intros [x Hx] [y Hy] Hxy Hyx. cbn in ×.
      apply opt_eq. intros l. split.
      - intros Hl.
        destruct (Hxy l) as (m & Hm & Hlm); auto.
        destruct (Hyx m) as (n & Hn & Hmn); auto.
        assert (n = l) by auto; subst.
        assert (m = l) by (apply antisymmetry; auto); subst.
        assumption.
      - intros Hl.
        destruct (Hyx l) as (m & Hm & Hlm); auto.
        destruct (Hxy m) as (n & Hn & Hmn); auto.
        assert (n = l) by auto; subst.
        assert (m = l) by (apply antisymmetry; auto); subst.
        assumption.
    Qed.

Lattice structure


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

    Lemma proj_is x l :
      is x l → proj x = l.
    Proof.
      intros Hl. apply antisymmetry.
      - apply fsup_lub. intros m Hm.
        assert (m = l) by eauto using is_unique. rauto.
      - eapply fsup_at; eauto. reflexivity.
    Qed.

    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.
    Proof.
      split.
      - intros [Hx Hl]. split.
        + firstorder.
        + subst. rewrite sup_inf. reflexivity.
      - intros [Hx Hl]. split.
        + destruct (classic (∀ i, ∃ j, ¬ ∃ li, is (x i j) li)).
          × exfalso.
            admit.
          × apply not_all_ex_not in H as (i & H). ∃ i. intro j.
            apply not_ex_not_all with _ _ j in H. auto.
        + subst. rewrite sup_inf. reflexivity.
    Admitted.

    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) _;
      |}.

sup, inf are singletons.

    Next Obligation.
      firstorder congruence.
    Qed.
    Next Obligation.
      firstorder congruence.
    Qed.

sup is the least upper bound

    Next Obligation.
      eexists; split; eauto.
      apply (sup_at i). cbn.
      erewrite proj_is by eauto. rauto.
    Qed.

    Next Obligation.
      destruct H0 as [(i & li & Hli) Hl]. subst. cbn.
      destruct (H i li Hli) as (m & Hm & _). clear i li Hli.
      ∃ m. split; auto.
      apply sup_lub. intros i.
      apply fsup_lub. intros li Hli.
      destruct (H i li Hli) as (m' & Hm' & LE).
      assert (m' = m) by eauto using is_unique. congruence.
    Qed.

inf is the greatest lower bound

    Next Obligation.
      destruct H as [H Hl]. subst.
      destruct (H i) as (l & Hl).
      ∃ l; split; auto. cbn.
      apply (inf_at i). rewrite (proj_is (x i) l) by auto.
      reflexivity.
    Qed.

    Next Obligation.
      eexists; split.
      - split; [ | auto].
        intros i. destruct (H i l) as (m & Hm & Hlm); eauto.
      - apply inf_glb. intros i. cbn.
        edestruct (H i) as (m & Hm & Hlm); eauto.
        erewrite proj_is; eauto.
    Qed.

Distributivity

    Next Obligation.
      apply opt_eq. intros l. cbn.
      transitivity (sup_inf_of x l).
      {
        unfold sup_of, inf_of, sup_inf_of, proj; cbn.
        split; intros [Hx Hl]; subst.
        - split.
          + firstorder.
          + apply antisymmetry.
            × apply sup_lub. intros i. apply (sup_at i).
              destruct (classic (∀ j, ∃ lij, is (x i j) lij)).
              -- eapply fsup_at; eauto. reflexivity.
              -- apply not_all_ex_not in H as (j & Hj).
                 apply (inf_at j). apply fsup_lub. firstorder.
            × apply sup_lub. intros i. apply (sup_at i).
              apply fsup_lub. intros _ [H [ ]].
              reflexivity.
        - split.
          + destruct Hx as [i Hi]. eauto.
          + apply antisymmetry.
            × apply sup_lub. intros i. apply (sup_at i).
              apply fsup_lub. intros _ [Hi [ ]].
              reflexivity.
            × apply sup_lub. intros i. apply (sup_at i).
              destruct (classic (∀ j, ∃ lij, is (x i j) lij)).
              -- eapply fsup_at; eauto. reflexivity.
              -- apply not_all_ex_not in H as (j & Hj).
                 apply (inf_at j). apply fsup_lub. firstorder.
      }
      rewrite sup_inf_of_cd.
      {
        unfold sup_of, inf_of, inf_sup_of, proj; cbn.
        split; intros [Hx Hl]; subst.
        - split.
          + intros f. destruct (Hx f) as (i & l & Hl). eauto.
          + f_equal. apply functional_extensionality. intros f.
            apply antisymmetry.
            × apply fsup_lub. intros _ [(i & l & Hl) [ ]]. reflexivity.
            × eapply fsup_at; eauto. reflexivity.
        - split.
          + intros f. destruct (Hx f) as (i & l & Hl). eauto.
          + f_equal. apply functional_extensionality. intros f.
            apply antisymmetry.
            × apply sup_lub. intros i. apply fsup_lub. intros l Hl.
              eapply fsup_at; eauto. eapply sup_at, fsup_at; eauto. reflexivity.
            × apply fsup_lub. intros _ [(i & l & Hl) [ ]]. reflexivity.
      }
    Qed.

Adjunction


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

    Global Instance emb_mor :
      Lazy.Morphism emb.
    Proof.
      split.
      - red. intros I x [i]. apply antisymmetry.
        + intros l Hl. cbn in ×. subst.
          eexists; split; [ | reflexivity]. red; cbn.
          split. ∃ i. eauto. unfold proj; cbn.
          apply antisymmetry.
          × apply sup_lub. intros j.
            apply fsup_lub. intros _ [ ].
            apply (sup_at j). reflexivity.
          × apply sup_lub. intros j. apply (sup_at j). cbn.
            eapply fsup_at; eauto. reflexivity.
        + apply sup_lub. cbn. intros j _ [ ].
          eexists; split; [reflexivity | ].
          apply sup_ub.
      - red. intros I x. apply antisymmetry.
        + cbn. intros _ [ ].
          eexists; split; [constructor; cbn; eauto | ].
          eapply inf_glb. intros i. apply (inf_at i).
          unfold proj; cbn. eapply fsup_at; eauto. reflexivity.
        + cbn. intros _ [? [ ]]. cbn in ×.
          eexists; split; [reflexivity | ].
          eapply inf_glb. intros i. unfold proj; cbn.
          apply (inf_at i). apply fsup_lub. intros _ [ ]. reflexivity.
    Qed.


    Lemma cases x :
      x = bot ∨ ∃ l, x = emb l.
    Proof.
      destruct (classic (ex (is x))) as [[l Hl] | H].
      - right. ∃ l.
        destruct x as [x Hx]; cbn in ×.
        apply opt_eq. intros l'.
        cbn. split; auto. congruence.
      - left. apply antisymmetry.
        + intros l Hl. elim H; eauto.
        + apply bot_lb.
    Qed.

    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).
    Proof.
      destruct (classic (∀ i, x i = bot)).
      - left. split; auto.
        apply antisymmetry; auto using bot_lb.
        apply sup_lub. intros i.
        intros l Hl. rewrite H in Hl. elim Hl.
        intros ([ ] & _).
      - right. apply not_all_ex_not in H as (i & Hi).
        split.
        unfold fsup. rewrite (Lazy.mor_sup emb).
        + cbn. apply opt_eq. intros l. cbn. split.
          × intros [(j & m & Hm)].
            econstructor.
    Admitted.

    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.
    Proof.
      apply antisymmetry; try apply bot_lb.
      unfold ext. apply fsup_lub. Local Transparent bot. cbn.
      intros i [? ?]. destruct H as [[ ]].
    Qed.

    Lemma ext_ana :
      (∀ x, ext f (emb x) = f x).
    Proof.
      intros x. unfold ext, emb. cbn.
      apply antisymmetry.
      - apply fsup_lub. intros _ [ ]. reflexivity.
      - apply fsup_ub. reflexivity.
    Qed.

    Instance ext_mor :
      CDL.Morphism (ext f).
    Proof.
      split.
      - red. intros I x.
        destruct (sup_cases x) as [[Hsup H] | [Hsup H]]; rewrite Hsup.
        + rewrite ext_bot. transitivity (sup i:I, ext f bot).
          × apply antisymmetry; try apply bot_lb.
            apply sup_lub. intros _. rewrite ext_bot. reflexivity.
          × f_equal. apply functional_extensionality. intro. rewrite H. reflexivity.
        + rewrite ext_ana. unfold fsup. rewrite (Lazy.mor_sup f).
          × apply antisymmetry.
            -- apply sup_lub. intros (l & i & Hli). cbn.
               apply (sup_at i). eapply fsup_at; eauto. reflexivity.
            -- apply sup_lub. intros i. apply fsup_lub. intros l Hli. cbn.
               admit.
          × admit.
      - admit.
    Admitted.

    Lemma ext_unique (g : F → M) `{Hg : !CDL.Morphism g} :
      (∀ x, g (emb x) = f x) → ∀ x, g x = ext f x.
    Proof.
      intros Hgf l. destruct (cases l) as [? | [y Hy]]; subst.
      - rewrite (Downset.Sup.mor_bot (f := g)).
        rewrite (Downset.Sup.mor_bot (f := ext f)).
        reflexivity.
      - rewrite ext_ana. auto.
    Qed.

  End DEF.

End LBot.