Library profinite_adj

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

Adjoint relation between the pointed and unpointed domains.

Here we define the lifing and forgetful functors between pointed and unpointed domains, and show that they are adjoint.
In addition, I show the counit of this adjunction has a partial inverse, which is a useful operation for "strictifying" a nonstrict hom.
NOTE!! The naming convention here is opposite that of the companion paper. Here the forgetful functor goes from unpointed domains to pointed domains, and the lifing functor goes from pointed domains to unpointed domains.

Program Definition plotkin_forget (A:preord)
  (Heff:effective_order A)
  (HA:plotkin_order false A) : plotkin_order true A

    := norm_plt A Heff true _.

Definition forgetPLT_ob (X:ob PLT) : ob PLT :=
  PLT.Ob _ (PLT.carrier _ X) (PLT.Class _ _
    (Preord.mixin (PLT.ord X))
    (PLT.effective X)
    (plotkin_forget _ (PLT.effective X) (PLT.plotkin X))).

Program Definition forgetPLT_map (X Y:ob PLT) (f:X Y)
  : forgetPLT_ob X forgetPLT_ob Y :=

  PLT.Hom _ (forgetPLT_ob X) (forgetPLT_ob Y)
    (@PLT.hom_rel _ X Y f) (PLT.hom_order _ X Y f) _.

Program Definition forgetPLT : functor PLT PLT :=
  Functor PLT PLT forgetPLT_ob forgetPLT_map _ _ _.
Solve Obligations of forgetPLT using auto.

Definition liftPPLT_ob (X:ob PLT) : ob PLT :=
  PLT.Ob _ (option (PLT.carrier _ X)) (PLT.Class _ _
    (lift_mixin (PLT.ord X))
    (effective_lift (PLT.effective X))
    (lift_plotkin _ _ _ (PLT.plotkin X) (PLT.effective X))).

Definition liftPPLT_rel (X Y:preord) (HX:effective_order X) (f:erel X Y)
  : erel (lift X) (lift Y) :=
  union2 (union2 (single (None,None))
    (image (mk_pair (liftup X) (const (@None Y))) (eff_enum X HX)))
    (image (pair_map (liftup X) (liftup Y)) f).

Lemma liftPPLT_rel_elem X Y HX f :
  forall x y, (x,y) liftPPLT_rel X Y HX f <->
    (y None \/ exists a b, (a,b) f /\ x Some a /\ y Some b).

Program Definition liftPPLT_map (X Y:ob PLT) (f:X Y)
  : liftPPLT_ob X liftPPLT_ob Y :=

  PLT.Hom _ (liftPPLT_ob X) (liftPPLT_ob Y)
     (liftPPLT_rel (PLT.ord X) (PLT.ord Y) (PLT.effective X) (@PLT.hom_rel _ X Y f))
      _ _.

Program Definition liftPPLT : functor PLT PLT :=
  Functor PLT PLT liftPPLT_ob liftPPLT_map _ _ _.

Definition adj_unit_rel (X:preord) (HX:effective_order X) : erel X (lift X) :=
    (image (mk_pair (id(X)) (const None)) (eff_enum X HX))
    (image (pair_map (id(X)) (liftup X))
      (esubset_dec _ (fun q => fst q snd q)
                  (fun q => eff_ord_dec X HX (snd q) (fst q))
                  (eprod (eff_enum X HX)
                         (eff_enum X HX)))).

Lemma adj_unit_rel_elem X HX x x' :
  (x,x') adj_unit_rel X HX <-> Some x x'.

Program Definition adj_unit_hom (X:ob PLT)
  : X (liftPPLT (forgetPLT X))

  := PLT.Hom _ X (liftPPLT (forgetPLT X)) (adj_unit_rel (PLT.ord X) (PLT.effective X)) _ _.

Program Definition adj_unit : nt id(PLT) (liftPPLT forgetPLT)
  := NT id(PLT) (liftPPLT forgetPLT) adj_unit_hom _.

Definition adj_counit_rel (Y:ob PLT)
  : erel (forgetPLT (liftPPLT Y)) Y :=

    (image (pair_map (liftup Y) (id(PLT.ord Y)))
      (esubset_dec _ (fun q => fst q snd q)
                  (fun q => eff_ord_dec Y (PLT.effective Y) (snd q) (fst q))
                  (eprod (eff_enum Y (PLT.effective Y))
                         (eff_enum Y (PLT.effective Y))))).

Lemma adj_counit_rel_elem Y : forall y y',
  (y,y') adj_counit_rel Y <-> y Some y'.

Program Definition adj_counit_hom Y : forgetPLT (liftPPLT Y) Y :=
  PLT.Hom _ (forgetPLT (liftPPLT Y)) Y (adj_counit_rel Y) _ _.

Program Definition adj_counit : nt (forgetPLT liftPPLT) id(PLT)
  := NT (forgetPLT liftPPLT) id(PLT) adj_counit_hom _.

Program Definition adj_counit_inv_hom Y : Y forgetPLT (liftPPLT Y) :=
  PLT.Hom _ Y (forgetPLT (liftPPLT Y)) (adj_unit_rel (PLT.ord Y) (PLT.effective Y)) _ _.

Lemma adj_counit_inv_ntish : forall A B f,
  adj_counit_inv_hom B f forgetPLT·liftPPLT·f adj_counit_inv_hom A.

Lemma adj_counit_inv_le Y : adj_counit_inv_hom Y adj_counit Y id.

Lemma adj_counit_inv_largest Y : forall f,
  f adj_counit Y id -> f adj_counit_inv_hom Y.

Lemma adj_counit_inv_eq Y : adj_counit Y adj_counit_inv_hom Y id.

Lemma adj_inv_eq : forall A B (f:A liftPPLT B),
  (forall a, exists b, (a, Some b) PLT.hom_rel f) ->
  adj_counit_inv_hom B adj_counit B forgetPLT·f forgetPLT·f.

Lemma adj_inv_eq_converse : forall A B (f:A liftPPLT B),
  adj_counit_inv_hom B adj_counit B forgetPLT·f forgetPLT·f ->
  (forall a, exists b, (a, Some b) PLT.hom_rel f).

Program Definition PLT_adjoint : adjunction forgetPLT liftPPLT :=
  Adjunction forgetPLT liftPPLT adj_unit adj_counit _ _.

Notation U := liftPPLT.
Notation L := forgetPLT.
Notation ε := (adj_counit _).
Notation η := (adj_unit _).
Notation γ := (adj_counit_inv_hom _).

Definition plt_hom_adj (X:PLT) (Y:PLT) (f:X U Y) : L X Y
  := ε L·f.

Definition plt_hom_adj' (X:PLT) (Y:PLT) (f:L X Y) : X U Y
  := U·f η.

Notation Ψ := plt_hom_adj.
Notation "Ψ⁻¹" := plt_hom_adj'.

Lemma plt_hom_adj1 (X:PLT) (Y:PLT) (f:X U Y) : Ψ⁻¹ (Ψ f) f.

Lemma plt_hom_adj2 (X:PLT) (Y:PLT) (f:L X Y) : Ψ (Ψ⁻¹ f) f.

Lemma U_mono : forall (X Y:ob PLT) (f f':X Y),
  f f' -> U·f U·f'.

Lemma U_reflects : forall (X Y:ob PLT) (f f':X Y),
  U·f U·f' -> f f'.

Lemma L_mono : forall (X Y:ob PLT) (f f':X Y),
  f f' -> L·f L·f'.

Lemma L_reflects : forall (X Y:ob PLT) (f f':X Y),
  L·f L·f' -> f f'.

Lemma Psi_mono (X:PLT) (Y:PLT) (f g:X U Y) :
  f g -> Ψ f Ψ g.

Lemma Psi_inv_mono (X:PLT) (Y:PLT) (f g:L X Y) :
  f g -> Ψ⁻¹ f Ψ⁻¹ g.

Lemma Psi_reflects (X:PLT) (Y:PLT) (f g:X U Y) :
  Ψ f Ψ g -> f g.

Lemma Psi_inv_reflects (X:PLT) (Y:PLT) (f g:L X Y) :
  Ψ⁻¹ f Ψ⁻¹ g -> f g.

Lemma U_bottom_least (X:PLT) (Y:PLT) (f:X U Y) :
  Ψ⁻¹ f.

Instance lift_plt_pointed (X:PLT) (Y:PLT) :
  pointed (PLT.homset_cpo _ X (liftPPLT Y)) :=
  { bottom := Ψ⁻¹
  ; bottom_least := U_bottom_least X Y

Program Definition lift_unit : 1 L 1
  := PLT.Hom true 1 (L 1) (ident_rel effective_unit) _ _.

Program Definition lift_unit' : L 1 1
  := PLT.Hom true (L 1) 1 (ident_rel effective_unit) _ _.

Lemma lift_unit_id1 : lift_unit lift_unit' id.

Lemma lift_unit_id2 : lift_unit' lift_unit id.

Program Definition lift_prod (A B:PLT) : (L A L B) L (A × B)
  := PLT.Hom true (L A L B) (L (A × B))
          (ident_rel (effective_prod (PLT.effective A) (PLT.effective B)))
          _ _.

Program Definition lift_prod' (A B:PLT) : L (A × B) L A L B
  := PLT.Hom true (L (A × B)) (L A L B)
          (ident_rel (effective_prod (PLT.effective A) (PLT.effective B)))
          _ _.

Lemma lift_prod_id1 A B : lift_prod A B lift_prod' A B id.

Lemma lift_prod_id2 A B : lift_prod' A B lift_prod A B id.

Local Transparent PLT.pair.

Lemma lift_prod_pair C A B (f:C A) (g:C B) :
  lift_prod A B L·f, L·g L·f, g.

Lemma lift_prod_pair' C A B (f:C A) (g:C B) :
  L·f, L·g lift_prod' A B L·f, g.

Lemma lift_prod_natural A B C D (f:A B) (g:C D) :
  lift_prod B D PLT.pair_map (L·f) (L·g) L·(PLT.pair_map f g) lift_prod A C.

Lemma lift_prod'_natural A B C D (f:A B) (g:C D) :
   PLT.pair_map (L·f) (L·g) lift_prod' _ _ lift_prod' _ _ L·(PLT.pair_map f g).

Section strictify.
  Variables X Y:ob PLT.
  Variable f: U X U Y.

  Let strictify := ε L·f γ.

  Lemma f_explode : U·(ε L·f) η f.

  Lemma strictify_le : U·strictify f.

  Lemma strictify_largest : forall q, U·q f -> q strictify.
End strictify.

Lemma U_hom_rel (A B:PLT) (f:A B) (a:U A) (b:U B) :
  (a,b) PLT.hom_rel (U·f) <->
  (b = None \/ exists a' b', (a',b') PLT.hom_rel f /\ a = Some a' /\ b = Some b').

Lemma L_hom_rel (A B:PLT) (f:A B) (a:L A) (b:L B) :
  (a,b) PLT.hom_rel (L·f) <-> (a,b) PLT.hom_rel f.

Definition lift (X:PLT) : PLT := U (L X).
Definition colift (X:PLT) : PLT := L (U X).

Definition smash_prod (A B:PLT) : U A × U B U (A B)
  := U·(PLT.pair_map ε ε lift_prod') η.

Definition unsmash_prod (A B:PLT) : U (A B) U A × U B
  := U·π, U·π .

Inductive smash_prod_spec (A B:PLT) : U A × U B -> U (A B) -> Prop :=
  | smash_some : forall x x' y y',
         x' x -> y' y ->
         smash_prod_spec A B (Some x, Some y) (Some (x',y'))
  | smash_none : forall m, smash_prod_spec A B m None.

Lemma smash_prod_iff (A B:PLT) m n :
  (m,n) PLT.hom_rel (smash_prod A B) <-> smash_prod_spec A B m n.

Lemma smash_unsmash (A B:PLT) :
  smash_prod A B unsmash_prod A B id.

Lemma unsmash_smash (A B:PLT) :
  unsmash_prod A B smash_prod A B id.

Global Opaque liftPPLT.
Global Opaque forgetPLT.