Library powerdom


Require Import Setoid.
Require Import List.

Require Import basics.
Require Import preord.
Require Import categories.
Require Import sets.
Require Import finsets.
Require Import esets.
Require Import effective.
Require Import directed.
Require Import plotkin.
Require Import joinable.
Require Import approx_rels.
Require Import profinite.
Require Import embed.

Powerdomains

Here we construct the lower, upper and convex powerdomains, and show that they form continuous functors in the category of embeddings.
Powerdomains over a domain X re defined as preorders consisting of finite h-inhabited subsets of X with the upper, lower and convex ordering, respectively.
Notibly, the convex powerdomain over unpointed domains has a representative for the empty set, which the convex powerdomain over unpointed domains lacks. This fact might be previously known (I am not actually sure), but it does not seem to be widely appreciated.

Inductive pdom_sort :=
  | Lower
  | Upper
  | Convex.

Module powerdom.
Section powerdom.
  Variable hf:bool.

  Record pdom_elem (X:preord) :=
    PdomElem
    { elem : finset X
    ; elem_inh : inh hf elem
    }.

  Section orders.
    Variable X:preord.

    Definition lower_ord (P Q:pdom_elem X) :=
      forall x, x elem P ->
        exists y, y elem Q /\ x y.

    Definition upper_ord (P Q:pdom_elem X) :=
      forall y, y elem Q ->
        exists x, x elem P /\ x y.

    Definition convex_ord (P Q:pdom_elem X) :=
      lower_ord P Q /\ upper_ord P Q.

    Lemma lower_ord_refl P : lower_ord P P.

    Lemma upper_ord_refl P : upper_ord P P.

    Lemma convex_ord_refl P : convex_ord P P.

    Lemma lower_ord_trans P Q R :
      lower_ord P Q -> lower_ord Q R -> lower_ord P R.

    Lemma upper_ord_trans P Q R :
      upper_ord P Q -> upper_ord Q R -> upper_ord P R.

    Lemma convex_ord_trans P Q R :
      convex_ord P Q -> convex_ord Q R -> convex_ord P R.

    Definition lower_preord_mixin :=
      Preord.Mixin (pdom_elem X) lower_ord lower_ord_refl lower_ord_trans.
    Definition upper_preord_mixin :=
      Preord.Mixin (pdom_elem X) upper_ord upper_ord_refl upper_ord_trans.
    Definition convex_preord_mixin :=
      Preord.Mixin (pdom_elem X) convex_ord convex_ord_refl convex_ord_trans.

    Hypothesis Xeff : effective_order X.

    Lemma lower_ord_dec : forall x y, {lower_ord x y}+{~lower_ord x y}.

    Lemma upper_ord_dec : forall x y, {upper_ord x y}+{~upper_ord x y}.

    Definition pdom_ord (sort:pdom_sort) :=
      Preord.Pack
        (pdom_elem X)
        match sort with
          | Lower => lower_preord_mixin
          | Upper => upper_preord_mixin
          | Convex => convex_preord_mixin
        end.

    Lemma pdom_ord_dec sort : forall (x y:pdom_ord sort), {xy}+{xy}.

    Lemma pdom_elem_eq_lower sort (x y:pdom_ord sort) :
      elem x elem y -> lower_ord x y.

    Lemma pdom_elem_eq_upper sort (x y:pdom_ord sort) :
      elem y elem x -> upper_ord x y.

    Lemma pdom_elem_eq_le sort (x y:pdom_ord sort) :
      elem x elem y -> x y.

    Lemma pdom_elem_eq_eq sort (x y:pdom_ord sort) :
      elem x elem y -> x y.

    Definition enum_elems sort : eset (pdom_ord sort)
      := fun n =>
           match finsubsets X (eff_enum X Xeff) n with
           | None => None
           | Some l =>
              match inh_dec X hf l with
              | left Hinh => Some (PdomElem X l Hinh)
              | right _ => None
              end
           end.

    Lemma enum_elems_complete sort (x:pdom_ord sort) :
      x enum_elems sort.

    Definition pdom_effective sort : effective_order (pdom_ord sort) :=
      EffectiveOrder
        (pdom_ord sort) (pdom_ord_dec sort)
        (enum_elems sort) (enum_elems_complete sort).

    Hypothesis Xplt : plotkin_order hf X.

    Definition all_tokens sort (M:finset (pdom_ord sort)) : finset X :=
      mub_closure Xplt (concat _ (map (@elem _) M)).

    Fixpoint select_pdom_elems sort (ls:finset (finset X)) : finset (pdom_ord sort) :=
      match ls with
      | nil => nil
      | x::xs =>
          match inh_dec X hf x with
          | left H => PdomElem X x H :: select_pdom_elems sort xs
          | right _ => select_pdom_elems sort xs
          end
      end.

    Lemma select_pdoms_in sort ls :
      forall x:pdom_ord sort,
        elem x ls -> x select_pdom_elems sort ls.

    Lemma select_pdoms_in' sort ls :
      forall x:pdom_ord sort,
        x select_pdom_elems sort ls ->
        exists x', x x' /\ elem x' ls.

    Definition normal_pdoms sort (M:finset (pdom_ord sort)) :=
      select_pdom_elems sort (list_finsubsets (all_tokens sort M)).

    Lemma normal_pdoms_in sort M :
      forall P:pdom_ord sort,
        (forall x, x elem P -> x all_tokens sort M) ->
        P normal_pdoms sort M.

    Lemma normal_pdoms_in' sort M :
      forall P:pdom_ord sort,
        P normal_pdoms sort M ->
        exists P', P P' /\
          (forall x, x elem P' -> x all_tokens sort M).

    Lemma pdom_has_normals sort :
      has_normals (pdom_ord sort) (pdom_effective sort) hf.

    Definition pdom_plt sort : plotkin_order hf (pdom_ord sort) :=
      norm_plt (pdom_ord sort) (pdom_effective sort) hf
               (pdom_has_normals sort).
  End orders.

  Program Definition single_elem (X:preord) (x:X) : pdom_elem X :=
    PdomElem X (x::nil) _.

  Program Definition union_elem (X:preord) (p q:pdom_elem X) :=
    PdomElem X (elem p ++ elem q) _.

  Program Definition concat_elem sort (X:preord)
    (xs:list (pdom_ord X sort)) (H:inh hf xs) :=
    PdomElem X (concat _ (map (@elem _) xs)) _.

  Definition powerdomain sort (X:PLT.PLT hf) :=
    PLT.Ob hf (pdom_elem X)
      (PLT.Class _ _
        (match sort with
          | Lower => lower_preord_mixin (PLT.ord X)
          | Upper => upper_preord_mixin (PLT.ord X)
          | Convex => convex_preord_mixin (PLT.ord X)
        end)
        (pdom_effective (PLT.ord X) (PLT.effective X) sort)
        (pdom_plt (PLT.ord X) (PLT.effective X) (PLT.plotkin X) sort)).

  Section powerdomain_fmap.
    Variables X Y:PLT.PLT hf.
    Variable f: X Y.

    Definition fmap_upper (x:pdom_elem X) (y:pdom_elem Y) :=
      forall a, a elem x -> exists b, b elem y /\ (a,b) PLT.hom_rel f.

    Definition fmap_lower (x:pdom_elem X) (y:pdom_elem Y) :=
      forall b, b elem y -> exists a, a elem x /\ (a,b) PLT.hom_rel f.

    Definition fmap_convex x y :=
      fmap_lower x y /\ fmap_upper x y.

    Lemma fmap_upper_semidec x y : semidec (fmap_upper x y).

    Lemma fmap_lower_semidec x y : semidec (fmap_lower x y).

    Lemma fmap_convex_semidec x y : semidec (fmap_convex x y).

    Definition fmap_lower_rel : erel (pdom_ord X Lower) (pdom_ord Y Lower) :=
      @esubset (prod_preord (pdom_ord X Lower) (pdom_ord Y Lower))
        (fun z => fmap_lower (fst z) (snd z))
        (fun z => fmap_lower_semidec (fst z) (snd z))
        (eff_enum _ (effective_prod (pdom_effective X (PLT.effective X) Lower)
                                    (pdom_effective Y (PLT.effective Y) Lower))).

    Definition fmap_upper_rel : erel (pdom_ord X Upper) (pdom_ord Y Upper) :=
      @esubset (prod_preord (pdom_ord X Upper) (pdom_ord Y Upper))
        (fun z => fmap_upper (fst z) (snd z))
        (fun z => fmap_upper_semidec (fst z) (snd z))
        (eff_enum _ (effective_prod (pdom_effective X (PLT.effective X) Upper)
                                    (pdom_effective Y (PLT.effective Y) Upper))).

    Definition fmap_convex_rel :=
      @esubset (prod_preord (pdom_ord X Convex) (pdom_ord Y Convex))
        (fun z => fmap_convex (fst z) (snd z))
        (fun z => fmap_convex_semidec (fst z) (snd z))
        (eff_enum _ (effective_prod (pdom_effective X (PLT.effective X) Convex)
                                    (pdom_effective Y (PLT.effective Y) Convex))).

    Definition fmap_rel sort :=
      match sort with
      | Lower => fmap_lower_rel
      | Upper => fmap_upper_rel
      | Convex => fmap_convex_rel
      end.

    Definition fmap_spec sort x y :=
      match sort with
      | Lower => fmap_lower x y
      | Upper => fmap_upper x y
      | Convex => fmap_convex x y
      end.

    Lemma fmap_convex_swell
      (z : powerdomain Convex X)
      (x y: powerdomain Convex Y) :
      fmap_spec Convex z x ->
      fmap_spec Convex z y ->
      exists z0:finset Y,
        (forall b, b z0 -> exists a, a elem z /\ (a,b) PLT.hom_rel f) /\
        (forall a, a elem z -> exists b, b z0 /\ (a,b) PLT.hom_rel f) /\

        (forall c, c elem x -> exists m, m z0 /\ c m) /\
        (forall d, d elem y -> exists m, m z0 /\ d m) /\

        (forall m, m z0 -> exists c, c elem x /\ c m) /\
        (forall m, m z0 -> exists d, d elem y /\ d m).

    Lemma fmap_rel_elem sort : forall x y,
      (x,y) fmap_rel sort <-> fmap_spec sort x y.

    Program Definition fmap sort
      : (powerdomain sort X) (powerdomain sort Y)
      := PLT.Hom hf (powerdomain sort X) (powerdomain sort Y)
           (fmap_rel sort) _ _.

  End powerdomain_fmap.

  Lemma pdom_fmap_id sort (A:PLT.PLT hf) :
    fmap A A id sort id.

  Lemma pdom_fmap_compose sort (A B C:PLT.PLT hf) (f:B C) (g:A B) :
    fmap A C (f g) sort fmap B C f sort fmap A B g sort.

  Lemma fmap_monotone sort X Y f f' :
    f f' -> fmap X Y f sort fmap X Y f' sort.

  Lemma fmap_respects sort X Y f f' :
    f f' -> fmap X Y f sort fmap X Y f' sort.

  Program Definition pdomain sort : functor (PLT.PLT hf) (PLT.PLT hf) :=
    Functor _ _ (powerdomain sort) (fun X Y f => fmap X Y f sort) _ _ _.

  Definition single_rel sort (X:PLT.PLT hf) : erel X (powerdomain sort X) :=
    esubset_dec _
      (fun xp => (single_elem X (fst xp) : pdom_ord X sort) snd xp)
      (fun x => pdom_ord_dec X (PLT.effective X) sort (snd x) (single_elem X (fst x)))
      (eprod (eff_enum _ (PLT.effective X)) (enum_elems X (PLT.effective X) sort)).

  Lemma single_rel_elem sort (X:PLT.PLT hf) x (p:pdom_ord X sort) :
    (x,p) single_rel sort X <-> p single_elem X x.

  Lemma single_elem_mono sort (X:preord) (x x':X) :
    x x' -> (single_elem X x:pdom_ord X sort) single_elem X x'.

  Program Definition single sort X : X powerdomain sort X :=
    PLT.Hom hf X (powerdomain sort X) (single_rel sort X) _ _.

  Definition union_rel sort (X:PLT.PLT hf)
    : erel (PLT.prod (powerdomain sort X) (powerdomain sort X)) (powerdomain sort X)
    := esubset_dec
         (PLT.prod (PLT.prod (powerdomain sort X) (powerdomain sort X)) (powerdomain sort X))
         (fun xyz => snd xyz union_elem X (fst (fst xyz)) (snd (fst xyz)))
         (fun xyz => pdom_ord_dec X (PLT.effective X) sort _ _)
         (eprod (eprod (enum_elems _ (PLT.effective X) sort)
                       (enum_elems _ (PLT.effective X) sort))
                (enum_elems _ (PLT.effective X) sort)).

  Lemma union_elem_lower_ord X (x x' y y':pdom_elem X) :
    lower_ord X x x' -> lower_ord X y y' ->
    lower_ord X (union_elem X x y) (union_elem X x' y').

  Lemma union_elem_upper_ord X (x x' y y':pdom_elem X) :
    upper_ord X x x' -> upper_ord X y y' ->
    upper_ord X (union_elem X x y) (union_elem X x' y').

  Lemma union_elem_convex_ord X (x x' y y':pdom_elem X) :
    convex_ord X x x' -> convex_ord X y y' ->
    convex_ord X (union_elem X x y) (union_elem X x' y').

  Lemma union_elem_pdom_ord sort X (x x' y y':pdom_ord X sort) :
    x x' -> y y' ->
    (union_elem X x y : pdom_ord X sort) union_elem X x' y'.

  Lemma union_rel_elem sort X x y z :
    ((x,y),z) union_rel sort X <-> union_elem X x y z.

  Program Definition union sort X :
    (PLT.prod (powerdomain sort X) (powerdomain sort X)) powerdomain sort X :=
    PLT.Hom _ _ _ (union_rel sort X) _ _.

  Definition join_rel sort X : erel (powerdomain sort (powerdomain sort X))
                                    (powerdomain sort X)
    := esubset_dec
         (PLT.prod (powerdomain sort (powerdomain sort X)) (powerdomain sort X))
         (fun xy => snd xy concat_elem sort X (elem (fst xy)) (elem_inh (fst xy)))
         (fun xy => pdom_ord_dec X (PLT.effective X) sort _ _)
         (eprod (enum_elems _ (PLT.effective (powerdomain sort X)) sort)
                (enum_elems _ (PLT.effective X) sort)).

  Lemma concat_in (A:Type) (xs:list (list A)) :
    forall x, In x (concat A xs) <->
      exists q, In q xs /\ In x q.

  Lemma concat_elem_mono sort X (a b:powerdomain sort (powerdomain sort X)) :
    a b ->
    (concat_elem sort X (elem a) (elem_inh a) : powerdomain sort X)
    concat_elem sort X (elem b) (elem_inh b).

  Lemma join_rel_elem sort X m n :
    (m,n) join_rel sort X <-> n concat_elem sort X (elem m) (elem_inh m).

  Program Definition join sort X :
    powerdomain sort (powerdomain sort X) powerdomain sort X :=
    PLT.Hom hf _ _ (join_rel sort X) _ _.

  Lemma single_natural sort (X Y:PLT.PLT hf) (f:X Y) :
    pdomain sort·f single sort X single sort Y f.

  Program Definition singleNT sort : nt id(PLT.PLT hf) (pdomain sort)
    := NT (id) (pdomain sort) (single sort) _.

  Lemma join_natural sort (X Y:PLT.PLT hf) (f:X Y) :
    pdomain sort·f join sort X join sort Y pdomain sort·pdomain sort·f.

  Program Definition joinNT sort : nt (pdomain sort pdomain sort) (pdomain sort)
    := NT (pdomain sort pdomain sort) (pdomain sort) (join sort) _.

  Lemma monad_unit1 sort :
    joinNT sort singleNT sortpdomain sort id.

  Lemma monad_unit2 sort :
    joinNT sort pdomain sortsingleNT sort id.

  Lemma monad_assoc sort :
    joinNT sort joinNT sortpdomain sort
    joinNT sort pdomain sortjoinNT sort.

End powerdom.

Definition empty_elem sort (X:PLT) : pdomain false sort X :=
  PdomElem false X nil I.

Definition empty_rel sort (X Y:PLT) : erel X (pdomain false sort Y) :=
  @esubset_dec (X × pdomain false sort Y)
    (fun xy => snd xy empty_elem sort Y)
    (fun xy => eff_ord_dec _ (PLT.effective (pdomain false sort Y)) _ _)
    (eprod (eff_enum _ (PLT.effective X))
           (eff_enum _ (PLT.effective (pdomain false sort Y)))).

Lemma empty_rel_elem sort (X Y:PLT) x y :
  (x,y) empty_rel sort X Y <-> y empty_elem sort Y.

Program Definition empty sort (X Y:PLT) : X pdomain false sort Y :=
  PLT.Hom false X (pdomain false sort Y) (empty_rel sort X Y) _ _ .

Lemma empty_natural sort (X Y Z:PLT) (f:Y Z) :
  pdomain false sort·f empty sort X Y empty sort X Z.

Lemma empty_unit sort (X Y:PLT) (f:X pdomain false sort Y) :
  f union false sort Y empty sort X Y, f .

Lemma empty_join1 sort (X Y:PLT) :
  join false sort Y empty sort X (pdomain false sort Y) empty sort X Y.

Lemma empty_join2 sort (X Y:PLT) :
  join false sort Y pdomain false sort·empty sort X Y
   empty sort (pdomain false sort X) Y.

Lemma union_commute_le hf sort (X Y:PLT.PLT hf) (f g:X pdomain hf sort Y) :
  union hf sort Y PLT.pair f g
  union hf sort Y PLT.pair g f.

Lemma union_commute hf sort (X Y:PLT.PLT hf) (f g:X pdomain hf sort Y) :
  union hf sort Y PLT.pair f g
  union hf sort Y PLT.pair g f.

Lemma union_assoc_le hf sort (X Y:PLT.PLT hf) (f g h:X pdomain hf sort Y) :
  union hf sort Y PLT.pair (union hf sort Y PLT.pair f g) h
  union hf sort Y PLT.pair f (union hf sort Y PLT.pair g h).

Lemma union_assoc hf sort (X Y:PLT.PLT hf) (f g h:X pdomain hf sort Y) :
  union hf sort Y PLT.pair (union hf sort Y PLT.pair f g) h
  union hf sort Y PLT.pair f (union hf sort Y PLT.pair g h).

Lemma empty_unit2 sort (X Y:PLT) (f:X pdomain false sort Y) :
  f union false sort Y f, empty sort X Y .

Lemma union_join hf sort (X:PLT.PLT hf) :
  join hf sort X union hf sort (pdomain hf sort X)
  union hf sort X PLT.pair_map (join hf sort X) (join hf sort X).

Lemma union_idem hf sort (X Y:PLT.PLT hf) (f:X pdomain hf sort Y) :
  union hf sort Y PLT.pair f f f.

Lemma union_lower (X Y:PLT) (f g:X pdomain false Lower Y) :
  f union false Lower Y PLT.pair f g.

Lemma union_upper hf (X Y:PLT.PLT hf) (f g:X pdomain hf Upper Y) :
  f union hf Upper Y PLT.pair f g.

Lemma lower_union_natural1 hf (X Y:PLT.PLT hf) (f:X Y) :
  union hf Lower Y PLT.pair_map (pdomain hf Lower·f) (pdomain hf Lower·f)
  
  pdomain hf Lower·f union hf Lower X.

Lemma lower_union_natural2 (X Y:PLT) (f:X Y) :
  pdomain false Lower·f union false Lower X
  union false Lower Y PLT.pair_map (pdomain false Lower·f) (pdomain false Lower·f).

Lemma upper_union_natural hf (X Y:PLT.PLT hf) (f:X Y) :
  pdomain hf Upper·f union hf Upper X
  union hf Upper Y PLT.pair_map (pdomain hf Upper·f) (pdomain hf Upper·f).

Lemma convex_union_natural hf (X Y:PLT.PLT hf) (f:X Y) :
  pdomain hf Convex·f union hf Convex X
  union hf Convex Y PLT.pair_map (pdomain hf Convex·f) (pdomain hf Convex·f).

End powerdom.

Notation powerdomain := powerdom.pdomain.

Section powerdom_functor.
  Variable hf:bool.
  Variable sort:pdom_sort.
  Variables X Y:PLT.PLT hf.

  Program Definition pdom_map (f:X Y)
    (x:powerdomain hf sort X) : powerdomain hf sort Y
    := powerdom.PdomElem hf Y (map f (powerdom.elem _ _ x)) _.

  Lemma pdom_map_lower_ord (f:XY) :
    forall a b,
      powerdom.lower_ord hf X a b <->
      powerdom.lower_ord hf Y (pdom_map f a) (pdom_map f b).

  Lemma pdom_map_upper_ord (f:XY) :
    forall a b,
      powerdom.upper_ord hf X a b <->
      powerdom.upper_ord hf Y (pdom_map f a) (pdom_map f b).

  Program Definition pdom_fmap (f:X Y) :
    powerdomain hf sort X powerdomain hf sort Y
    := Embedding hf _ _ (pdom_map f) _ _ _ _.
End powerdom_functor.

Program Definition powerdomainF (hf:bool) (sort:pdom_sort) :
  functor (EMBED hf) (EMBED hf) :=
  Functor (EMBED hf) (EMBED hf)
    (powerdomain hf sort)
    (pdom_fmap hf sort)
    _ _ _.

Require Import cont_functors.
Require Import bilimit.

Section powerdom_decompose.
  Variable hf:bool.
  Variable I:directed_preord.
  Variables DS : directed_system I (EMBED hf).
  Variable CC : cocone DS.

  Hypothesis decompose : forall x:cocone_point CC,
    { i:I & { a:ds_F DS i | cocone_spoke CC i a x }}.

  Lemma finset_decompose
    (X:finset (PLT.ord (cocone_point CC))) :
    { k:I & { Y:finset (PLT.ord (ds_F DS k)) |
       X map (cocone_spoke CC k) Y }}.
End powerdom_decompose.

Lemma powerdomain_continuous hf sort : continuous_functor (powerdomainF hf sort).