Library embed

Require Import Setoid.

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 approx_rels.
Require Import profinite.

Basis embeddings and EP-pairs

Here we define the category of embeddings over PLT. These are used to construct the solutions to recursive domain equations. Here we show that the category of basis embeddings is equivalant to the more usual category of embedding-projection pairs. Basis embeddings are considerably more convenient to work with than EP-pairs, so we prefer them for building bilimits and proving functors continuous.
Basis embeddings form a category with the effective Plotkin orders as objects. To avoid notational confusion, we use the symbol ⇀ to refer to embeddings, reserving → for the homs of PLT.

Record embedding (hf:bool) (A B:PLT.ob hf) :=
  { embed_map :> A -> B
  ; embed_mono : forall a a', a a' -> embed_map a embed_map a'
  ; embed_reflects : forall a a', embed_map a embed_map a' -> a a'
  ; embed_directed0 : forall y,
      if hf then True else exists x, embed_map x y
  ; embed_directed2 : forall y a b,
      embed_map a y ->
      embed_map b y ->
      exists c, embed_map c y /\ a c /\ b c

Program Definition embed_ident (hf:bool) (A:PLT.ob hf) : embedding hf A A :=
  Embedding hf A A (fun x => x) _ _ _ _.
Solve Obligations using (intros; auto).

Program Definition embed_compose (hf:bool) A B C
  (g:embedding hf B C) (f:embedding hf A B) : embedding hf A C :=
  Embedding hf A C (fun x => embed_map g (embed_map f x)) _ _ _ _.

Definition embed_order hf A B (E G:embedding hf A B) :=
  forall x, embed_map E x embed_map G x.

Program Definition embed_order_mixin hf A B : Preord.mixin_of (embedding hf A B) :=
  Preord.Mixin (embedding hf A B) (embed_order hf A B) _ _ .
Solve Obligations using (unfold embed_order; intros; eauto).

Canonical Structure embed_ord hf A B :=
  Preord.Pack (embedding hf A B) (embed_order_mixin hf A B).

Definition embed_comp_mixin hf :=
    (Comp.Mixin _ _ (embed_ident hf) (embed_compose hf)).

Canonical Structure embed_comp hf :=
  Comp.Pack (PLT.ob hf) (embedding hf) (embed_comp_mixin hf).

Program Definition embed_func {hf A B} (E:embedding hf A B) : PLT.ord A PLT.ord B :=
  Preord.Hom A B (embed_map E) (embed_mono E).
Coercion embed_func : embedding >-> hom.

Definition embed_eq_mixin hf A B := Preord.ord_eq (embed_ord hf A B).

Lemma embed_cat_axioms hf :
  Category.axioms (PLT.ob hf) (embedding hf) (embed_eq_mixin hf) (embed_comp_mixin hf).

Definition EMBED hf :=
  Category (PLT.ob hf) (embedding hf) _ _ (embed_cat_axioms hf).

Notation "A ⇀ B" := (hom (EMBED _) A B) (at level 70, no associativity).

Add Parametric Morphism hf A B :
  (@embed_map hf A B) with signature
        (@Preord.ord_op (embed_ord hf A B)) ==>
        (@Preord.ord_op A) ==>
        (@Preord.ord_op B)
    as embed_map_morphism.

Add Parametric Morphism hf A B :
  (@embed_map hf A B) with signature
        (@eq_op (CAT_EQ (EMBED hf) A B)) ==>
        (@eq_op (Preord_Eq A)) ==>
        (@eq_op (Preord_Eq B))
    as embed_map_eq_morphism.

Lemma embed_unlift hf (A B:PLT.ob hf) (f g:A B) x :
  f g -> f x g x.

Lemma embed_unlift' hf (A B:PLT.ob hf) (f g:A B) x :
  f g -> f x g x.

Lemma embed_lift hf (A B:PLT.ob hf) (f g:A B) :
  (forall x, f x g x) -> f g.

Lemma embed_lift' hf (A B:PLT.ob hf) (f g:A B) :
  (forall x, f x g x) -> f g.

The category of embeddings over partial plotkin orders has an initial object. The category of embeddings over total plotkin orders, however, does not.
Program Definition embed_initiate X : PLT.empty true X :=
  Embedding true (PLT.empty true) X (fun x => False_rect _ x) _ _ _ _.

Program Definition PPLT_EMBED_initialized_mixin :=
    (PLT.ob true)
    (embedding true)
    (embed_eq_mixin true)
    (PLT.empty true)

Canonical Structure PPLT_EMBED_initialized :=
    (PLT.ob true) (embedding true)
    (embed_eq_mixin true)
    (embed_comp_mixin true)
    (embed_cat_axioms true)

Section ep_pairs.
  Variable hf:bool.

  Notation PLT := (PLT.PLT hf).

  Record is_ep_pair (X Y:ob PLT) (e:X Y) (p:Y X) :=
  { pe_ident : p e id
  ; ep_ident : e p id

  Record ep_pair (X Y:ob PLT) :=
  { embed : X Y
  ; project : Y X
  ; ep_correct : is_ep_pair X Y embed project

  Program Definition ep_id (X:ob PLT) : ep_pair X X :=
    EpPair X X id id _.

  Program Definition ep_compose (X Y Z:ob PLT) (g:ep_pair Y Z) (f:ep_pair X Y) :=
    EpPair X Z (embed g embed f) (project f project g) _.

  Lemma ep_pair_embed_eq_proj_eq : forall X Y e e' p p',
    is_ep_pair X Y e p ->
    is_ep_pair X Y e' p' ->
    e e' -> p p'.

  Program Definition ep_pair_eq_mixin X Y : Eq.mixin_of (ep_pair X Y) :=
    Eq.Mixin _ (fun f g => embed f embed g) _ _ _.

  Definition ep_pair_comp_mixin : Comp.mixin_of (PLT.ob hf) ep_pair :=
    Comp.Mixin _ ep_pair ep_id ep_compose.

  Canonical Structure ep_pair_eq X Y := Eq.Pack (ep_pair X Y) (ep_pair_eq_mixin X Y).
  Canonical Structure ep_pair_comp := Comp.Pack _ ep_pair ep_pair_comp_mixin.

  Lemma ep_cat_axioms :
    Category.axioms _ ep_pair ep_pair_eq_mixin ep_pair_comp_mixin.

  Canonical Structure PLT_EP :=
    Category (PLT.ob hf) ep_pair ep_pair_eq_mixin ep_pair_comp_mixin ep_cat_axioms.

  Definition find_inhabitant' : forall A (P:eset A) (H:einhabited P),
    { a:A | a P }.

  Definition choose' A P H := proj1_sig (find_inhabitant' A P H).

  Section ep_pair_embed_func.
    Variables X Y:ob PLT.
    Variable ep : ep_pair X Y.

    Let e := embed ep.
    Let p := project ep.
    Let Hep := ep_correct X Y ep.

    Section embed_func.
      Variable x:X.

      Lemma ep_semidec : forall y, semidec ((x,y) PLT.hom_rel e /\ (y,x) PLT.hom_rel p).

      Definition embed_image :=
        esubset (fun y => (x,y) PLT.hom_rel e /\ (y,x) PLT.hom_rel p)
           (eff_enum (PLT.ord Y) (PLT.effective Y)).

      Lemma embed_image_inhabited : einhabited embed_image.
    End embed_func.

    Program Definition ep_embed : Preord.hom (PLT.ord X) (PLT.ord Y) :=
      Preord.Hom X Y
        (fun x => choose' (PLT.ord Y) (embed_image x) (embed_image_inhabited x)) _.

    Lemma embed_func_reflects : forall x x',
      ep_embed#x ep_embed#x' -> x x'.

    Lemma embed_func_directed0 : forall y,
      if hf then True else exists x, ep_embed#x y.

    Lemma embed_func_directed2 : forall y, forall a b,
      ep_embed#a y ->
      ep_embed#b y ->
      exists c, ep_embed#c y /\ a c /\ b c.

    Definition ep_embedding : embedding hf X Y :=
      Embedding hf X Y
        ( _ _ ep_embed)
        (Preord.axiom _ _ ep_embed)

  End ep_pair_embed_func.

  Section embed_func_ep_pair.
    Variables X Y:ob PLT.
    Variable embed : embedding hf X Y.

    Definition project_rel :=
      esubset_dec (PLT.ord Y × PLT.ord X)%cat_ob
         (fun yx => fst yx embed#(snd yx))
         (fun yx => eff_ord_dec Y (PLT.effective Y) (embed#(snd yx)) (fst yx))
         (eprod (eff_enum Y (PLT.effective Y)) (eff_enum X (PLT.effective X))).

    Lemma project_rel_elem : forall y x,
      embed#x y <-> (y,x) project_rel.

    Program Definition project_hom : Y X :=
      PLT.Hom hf Y X project_rel _ _.

    Definition embed_rel :=
      esubset_dec (PLT.ord X×PLT.ord Y)%cat_ob
         (fun xy => embed#(fst xy) snd xy)
         (fun xy => eff_ord_dec Y (PLT.effective Y) (snd xy) (embed#(fst xy)))
         (eprod (eff_enum X (PLT.effective X)) (eff_enum Y (PLT.effective Y))).

    Lemma embed_rel_elem : forall y x,
      embed#x y <-> (x,y) embed_rel.

    Program Definition embed_hom : X Y :=
      PLT.Hom hf X Y embed_rel _ _.

    Lemma embed_func_is_ep_pair : is_ep_pair X Y embed_hom project_hom.

    Definition embed_ep_pair :=
      EpPair X Y embed_hom project_hom embed_func_is_ep_pair.

  End embed_func_ep_pair.

  Lemma embed_ep_roundtrip1 : forall X Y (ep:ep_pair X Y),
    embed_ep_pair (ep_embedding ep) ep.

  Lemma embed_ep_roundtrip2 : forall X Y (e : X Y),
    e ep_embedding (embed_ep_pair e).
End ep_pairs.

Canonical Structure PLT_EP.
Canonical Structure ep_pair_eq.
Canonical Structure ep_pair_comp.

Program Definition embedForget hf : functor (EMBED hf) (PLT.PLT hf) :=
  Functor (EMBED hf) (PLT.PLT hf) (fun X => X) (fun X Y f => embed_hom hf X Y f) _ _ _.