Library lattices.Upset

Require Import FunctionalExtensionality.
Require Import coqrel.LogicalRelations.
Require Import structures.Lattice.
Require Import structures.Completion.
Require Import lattices.Downset.

Interface

The upset lattice over a poset is a completely distributive completion that is meet dense and completely meet prime. We use it as an intermediate step in the construction of the free completely distributive lattice (see Morris, 2005).

Module Inf <: LatticeCategory.

  Class Morphism {L M : cdlattice} (f : L → M) :=
    mor : ∀ {I} (x : I → L), f (linf x) = inf i , f (x i).

  Lemma mor_meet `{Morphism} x y :
    f (x && y) = f x && f y.
    Local Transparent meet.
  Lemma mor_ref {L M : cdlattice} (f : L → M) :
    Morphism f →
    PosetMorphism f.

  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)).

  Hint Immediate mor_ref : typeclass_instances.

End Inf.

Construction

Module Upset : LatticeCompletion Inf.

Opposite order

To avoid redundancies, we define the opposite order and lattice, and construct upsets by dualizing the Downset completion. This may or may not result in a lower complexity than copy-and-pasting, so we should evaluate once the Downset proofs are completed.

  Program Definition opp_poset (C : poset) : poset :=
    {|
      poset_carrier := C;
      ref x y := y [= x;
    |}.

  Program Definition opp_cdlat (L : cdlattice) : cdlattice :=
    {|
      cdl_poset := opp_poset L;
      lsup I x := linf x;
      linf I x := lsup x;
    |}.

  (*
  Definition opp_map {A B} (f : A -> B) : opp A -> opp B :=
    fun '(opp_in a) => opp_in (f a).

  Instance opp_map_ref {A B} `{Poset A} `{Poset B} (f : A -> B) :
    PosetMorphism f ->
    PosetMorphism (opp_map f).
  Proof.
    intros Hf. split. intros x y Hxy. cbn in *. rauto.
  Qed.
   *)

Upsets

  Definition F (C : poset) := opp_cdlat (downset (opp_poset C)).

  Section DEFS.
    Context {C : poset}.

    Definition emb (c : C) : F C :=
      Downset.emb (c : opp_poset C).

    Lemma emb_mor c1 c2 : emb c1 [= emb c2 ↔ c1 [= c2.

    Context {L : cdlattice}.

    Definition ext (f : C → L) (x : F C) : L :=
      Downset.ext (f : opp_poset C → opp_cdlat L) (x : downset (opp_poset C)).

    Context {f : C → L} `{Hf : !PosetMorphism f}.

    Instance ext_mor :
      Inf.Morphism (ext f).

    Lemma ext_ana :
      (∀ x, ext f (emb x) = f x).

    Lemma ext_unique (g : F C → L) `{Hg : !Inf.Morphism g} :
      (∀ x, g (emb x) = f x ) → ∀ x, g x = ext f x.
  End DEFS.

  Include (LatticeCompletionDefs Inf).

End Upset.

Notation upset := Upset.F.
Notation up := Upset.emb.