Library profinite


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

Delimit Scope plt_scope with plt.
Open Scope plt_scope.

Categories of profinite domains, expressed as Plotkin orders

Here we define both the category PLT of effective Plotkin orders, and the category ∂PLT of partial Plotkin orders. PLT is is equivalant to the category of profinite domains via ideal completion, and ∂PLT is equivalant to the category of pointed profinite domains with strict continuous functions.
The objects of PLT are the effective Plotkin orders, and the arrows are approximable relations. The objects and characteristic operations are provided for the unit, empty, product, sum and function space.
PLT is DCPO-enriched, which means that each homset is equipped with a DCPO. In addition the composition operation is continuous in both arguments.

Module PLT.
Section PLT.
  Variable hf:bool.

  Record class_of (A:Type) :=
    Class
    { cls_preord : Preord.mixin_of A
    ; cls_ord := Preord.Pack A cls_preord
    ; cls_effective : effective_order cls_ord
    ; cls_plotkin : plotkin_order hf cls_ord
    }.

  Record ob := Ob { carrier :> Type; class : class_of carrier }.

  Definition effective (X:ob) := cls_effective _ (class X).
  Definition plotkin (X:ob) := cls_plotkin _ (class X).
  Definition ord (X:ob) := cls_ord _ (class X).

  Canonical Structure ord.
  Canonical Structure dec (X:ob) := eff_to_ord_dec (ord X) (effective X).

  Record hom (A B:ob) :=
    Hom
    { hom_rel :> erel (ord A) (ord B)
    ; hom_order : forall x x' y y', x x' -> y' y ->
         (x,y) hom_rel -> (x',y') hom_rel
    ; hom_directed : directed_rel hf (ord A) (ord B) (effective A) hom_rel
    }.

  Program Definition hom_ord_mixin (A B:ob) : Preord.mixin_of (hom A B) :=
    Preord.Mixin (hom A B) (fun f g => hom_rel f hom_rel g) _ _.
  Solve Obligations of hom_ord_mixin using (intros; eauto).

  Canonical Structure hom_ord (A B:ob) := Preord.Pack (hom A B) (hom_ord_mixin A B).

  Definition hom_eq_mixin (A B:ob) := Preord.ord_eq (hom_ord A B).
  Canonical Structure hom_eq (A B:ob) := Eq.Pack (hom A B) (hom_eq_mixin A B).

  Definition ident (A:ob) : hom A A :=
    Hom A A
       (ident_rel (effective A))
       (ident_ordering (ord A) (effective A))
       (ident_image_dir hf (ord A) (effective A)).

  Program Definition compose (A B C:ob) (g:hom B C) (f:hom A B) : hom A C :=
    Hom A C (compose_rel (effective B) g f) _ _.

  Definition comp_mixin : Comp.mixin_of ob hom
    := Comp.Mixin ob hom ident compose.
  Canonical Structure comp : Comp.type := Comp.Pack ob hom comp_mixin.

  Lemma compose_mono (X Y Z:ob) (f f':hom X Y) (g g':hom Y Z) :
    f f' -> g g' -> g f g' f'.

  Lemma cat_axioms : Category.axioms ob hom hom_eq_mixin comp_mixin.

  Canonical Structure PLT : category :=
    Category ob hom hom_eq_mixin comp_mixin cat_axioms.

  Program Definition empty : ob :=
    Ob False
      (Class _
        (Preord.mixin emptypo)
        effective_empty
        (empty_plotkin hf)).

  Program Definition unit : ob :=
    Ob unit
      (Class _
        (Preord.mixin unitpo)
        effective_unit
        (unit_plotkin hf)).

  Definition prod (A B:ob) : ob :=
    Ob (carrier A * carrier B)
       (Class _
         (Preord.mixin (ord A × ord B))
         (effective_prod (effective A) (effective B))
         (plotkin_prod hf (ord A) (ord B) (effective A) (effective B) (plotkin A) (plotkin B))).
  Canonical Structure prod.

  Definition sum (A B:ob) : ob :=
    Ob (sum_preord (ord A) (ord B))
       (Class _
         (Preord.mixin (sum_preord (ord A) (ord B)))
         (effective_sum (effective A) (effective B))
         (plotkin_sum hf (ord A) (ord B) (effective A) (effective B)
             (plotkin A) (plotkin B))
         ).
  Canonical Structure sum.

  Definition exp (A B:ob) : ob :=
    Ob (joinable_relation hf (ord A) (ord B))
       (Class _
         (joinable_rel_ord_mixin hf (ord A) (ord B))
         (joinable_rel_effective hf (ord A) (ord B) (effective A) (effective B) (plotkin A))
         (joinable_rel_plt hf (ord A) (ord B) (effective A) (plotkin A) (effective B) (plotkin B))).
  Canonical Structure exp.

  Program Definition initiate A : empty A :=
    Hom empty A (esets.empty (prod_preord (ord empty) (ord A))) _ _.

  Program Definition terminate A : A unit :=
    Hom A unit (eprod (eff_enum _ (effective A)) (eff_enum _ (effective unit))) _ _.

  Definition iota1 A B : A (sum A B) :=
    Hom A (sum A B)
      (iota1_rel (ord A) (ord B) (effective A))
      (iota1_ordering (ord A) (ord B) (effective A))
      (iota1_dir (ord A) (ord B) (effective A) hf).

  Definition iota2 A B : B (sum A B) :=
    Hom B (sum A B)
      (iota2_rel (ord A) (ord B) (effective B))
      (iota2_ordering (ord A) (ord B) (effective B))
      (iota2_dir (ord A) (ord B) (effective B) hf).

  Definition sum_cases {C A B} (f:A C) (g:B C) : (sum A B) C :=
    Hom (sum A B) C
      (sum_cases (ord C) (ord A) (ord B) f g)
      (sum_cases_ordering (ord C) (ord A) (ord B) f g
           (hom_order _ _ f) (hom_order _ _ g))
      (sum_cases_dir (ord C) (ord A) (ord B)
          (effective A) (effective B) hf f g
          (hom_directed _ _ f) (hom_directed _ _ g)).

  Definition app {A B} : (prod (exp A B) A) B :=
    Hom (prod (exp A B) A) B
      (apply_rel hf (ord A) (ord B) (effective A) (effective B) (plotkin A))
      (apply_rel_ordering hf (ord A) (ord B) (effective A) (effective B) (plotkin A))
      (apply_rel_dir hf (ord A) (ord B) (effective A) (effective B) (plotkin A)).

  Definition curry {C A B} (f:(prod C A) B) : C (exp A B) :=
    Hom C (exp A B)
      (curry_rel hf (ord A) (ord B) (ord C)
        (effective A) (effective B) (effective C) (plotkin A) f)
      (curry_rel_ordering hf (ord A) (ord B) (ord C)
        (effective A) (effective B) (effective C) (plotkin A)
        f (hom_order _ _ f))
      (curry_rel_dir hf (ord A) (ord B) (ord C)
        (effective A) (effective B) (effective C) (plotkin A)
        f (hom_order _ _ f) (hom_directed _ _ f)
        (plotkin B)).

  Definition pair {C A B} (f:C A) (g:C B) : C (prod A B) :=
    Hom C (prod A B)
      (pair_rel (effective C) f g)
      (pair_rel_ordering _ _ _ (effective C) f g (hom_order _ _ f) (hom_order _ _ g))
      (pair_rel_dir _ _ _ _ (effective C) f g
        (hom_order _ _ f) (hom_order _ _ g)
        (hom_directed _ _ f) (hom_directed _ _ g)).

  Definition pi1 {A B} : (prod A B) A :=
    Hom (prod A B) A
      (pi1_rel (effective A) (effective B))
      (pi1_rel_ordering _ _ (effective A) (effective B))
      (pi1_rel_dir _ _ _ (effective A) (effective B)).

  Definition pi2 {A B} : (prod A B) B :=
    Hom (prod A B) B
      (pi2_rel (effective A) (effective B))
      (pi2_rel_ordering _ _ (effective A) (effective B))
      (pi2_rel_dir _ _ _ (effective A) (effective B)).

  Definition pair_map {A B C D} (f:A C) (g:B D) : (prod A B) (prod C D) :=
    pair (f pi1) (g pi2).

  Program Definition pair_map' {A B C D} (f:A C) (g:B D) : (prod A B) (prod C D) :=
    Hom (prod A B) (prod C D) (pair_rel' f g) _ _.

  Lemma pair_map_eq {A B C D} (f:A C) (g:B D) :
    pair_map f g pair_map' f g.

  Theorem initiate_univ A (f:empty A) :
    f initiate A.

  Theorem terminate_le_univ A (f:A unit) :
    f terminate A.

  Theorem iota1_cases_commute C A B (f:A C) (g:B C) :
    sum_cases f g iota1 A B f.

  Theorem iota2_cases_commute C A B (f:A C) (g:B C) :
    sum_cases f g iota2 A B g.

  Theorem sum_cases_universal C A B (f:A C) (g:B C) (CASES:(sum A B) C) :
    CASES iota1 A B f -> CASES iota2 A B g -> CASES sum_cases f g.

  Theorem pair_universal C A B (f:C A) (g:C B) (PAIR:C (prod A B)) :
    pi1 PAIR f -> pi2 PAIR g -> PAIR pair f g.

  Theorem pair_universal_le C A B (f:C A) (g:C B) (PAIR:C (prod A B)) :
    pi1 PAIR f -> pi2 PAIR g -> PAIR pair f g.

  Theorem pair_le_commute1 C A B (f:C A) (g:C B) :
    pi1 pair f g f.

  Theorem pair_le_commute2 C A B (f:C A) (g:C B) :
    pi2 pair f g g.

  Theorem pair_compose_commute A B C D
    (f:C A) (g:C B) (h:D C) :
    PLT.pair f g h PLT.pair (f h) (g h).

  Theorem curry_apply A B C (f:(prod C A) B) :
    app pair_map (curry f) id f.

  Theorem pair_mono (C A B:ob) (f f':C A) (g g':C B) :
    f f' -> g g' -> pair f g pair f' g'.

  Theorem pair_eq (C A B:ob) (f f':C A) (g g':C B) :
    f f' -> g g' -> pair f g pair f' g'.

  Theorem sum_cases_mono (C A B:ob) (f f':A C) (g g':B C) :
    f f' -> g g' -> sum_cases f g sum_cases f' g'.

  Theorem sum_cases_eq (C A B:ob) (f f':A C) (g g':B C) :
    f f' -> g g' -> sum_cases f g sum_cases f' g'.

  Theorem curry_mono (C A B:ob) (f f':prod C A B) :
    f f' -> curry f curry f'.

  Theorem curry_eq (C A B:ob) (f f':prod C A B) :
    f f' -> curry f curry f'.

  Theorem pair_map_pair C X Y Z W (f1:C X) (f2:X Y) (g1:C Z) (g2:Z W) :
    pair (f2 f1) (g2 g1) pair_map f2 g2 pair f1 g1.

  Theorem curry_apply2 A B C (f:(prod C A) B) (g:C A) :
    app pair (curry f) g f pair id g.

  Theorem curry_apply3 A B C D (f:(prod D A) B) (h:C D) (g:C A) :
    app pair (curry f h) g f pair h g.

  Theorem curry_universal A B C (f:(prod C A) B) (CURRY:C (exp A B)) :
    app pair_map CURRY id f -> CURRY curry f.

  Theorem curry_compose_commute A B C D (f:(prod C A) B) (h:D C) :
    curry f h curry (f pair_map h id).

  Definition initialized_mixin :=
    Initialized.Mixin ob hom hom_eq_mixin empty initiate initiate_univ.

  Program Definition cocartesian_mixin :=
    Cocartesian.Mixin ob hom hom_eq_mixin comp_mixin sum iota1 iota2 (@sum_cases) _.

  Definition cocartesian :=
    Cocartesian ob hom hom_eq_mixin comp_mixin cat_axioms initialized_mixin cocartesian_mixin.

  Lemma compose_hom_rel : forall (A B C:PLT) (f:A B) (g:B C) x z,
    (x,z) PLT.hom_rel (g f) <->
    exists y, (x,y) PLT.hom_rel f /\ (y,z) PLT.hom_rel g.

  Lemma pair_hom_rel : forall (A B C:PLT) (f:C A) (g:C B) c a b ,
    (c,(a,b)) hom_rel (pair f g) <-> (c,a) hom_rel f /\ (c,b) hom_rel g.

  Lemma sum_cases_hom_rel : forall (A B C:PLT) (f:A C) (g:B C) c z,
    (z,c) hom_rel (sum_cases f g) <->
        match z with
        | inl a => (a,c) hom_rel f
        | inr b => (b,c) hom_rel g
        end.

  Lemma curry_hom_rel : forall (A B C:PLT) (f:prod C A B) c R,
    (c,R) hom_rel (curry f) <->
    (forall a b, (a,b) proj1_sig R -> ((c,a),b) hom_rel f).

  Lemma app_hom_rel : forall (A B:PLT) R x y,
    ((R,x),y) hom_rel (@app A B) <->
    exists x' y', (x',y') proj1_sig R /\ x' x /\ y y'.

  Global Opaque compose.
  Global Opaque pair.
  Global Opaque sum_cases.
  Global Opaque curry.
  Global Opaque app.

  Section homset_cpo.
    Variables A B:ob.

    Program Definition hom_rel' : hom_ord A B erel (ord A) (ord B) :=
      Preord.Hom (hom_ord A B) (erel (ord A) (ord B)) (@hom_rel A B) _.

    Program Definition homset_sup (M:cl_eset (directed_hf_cl hf) (hom_ord A B))
      : hom A B := Hom A B (∪(image hom_rel' M)) _ _.

    Program Definition homset_cpo_mixin :
      CPO.mixin_of (directed_hf_cl hf) (hom_ord A B)
      := CPO.Mixin _ _ homset_sup _ _.

    Definition homset_cpo : CPO.type (directed_hf_cl hf) :=
      CPO.Pack _ (hom A B) (hom_ord_mixin A B) homset_cpo_mixin.
  End homset_cpo.
End PLT.

Theorem pair_commute1 (C A B:PLT false) (f:C A) (g:C B) :
  pi1 false pair false f g f.

Theorem pair_commute2 (C A B:PLT false) (f:C A) (g:C B) :
  pi2 false pair false f g g.

Program Definition terminated_mixin
  := Terminated.Mixin (ob false) (hom false)
       (hom_eq_mixin false)
       (unit false) (terminate false) _.

Program Definition cartesian_mixin
  := Cartesian.Mixin (ob false) (hom false)
       (hom_eq_mixin false) (comp_mixin false)
       (prod false) (@pi1 false) (@pi2 false)
       (@pair false) _.

Program Definition cartesian_closed_mixin
  := CartesianClosed.Mixin (ob false) (hom false)
       (hom_eq_mixin false) (comp_mixin false)
       (cat_axioms false)
       terminated_mixin
       cartesian_mixin
       (exp false) (@curry false) (@app false)
       _.

Definition terminated :=
  Terminated (ob false) (hom false)
       (hom_eq_mixin false) (comp_mixin false)
       (cat_axioms false)
       terminated_mixin.
Definition cartesian :=
  Cartesian (ob false) (hom false)
       (hom_eq_mixin false) (comp_mixin false)
       (cat_axioms false)
       terminated_mixin
       cartesian_mixin.
Definition cartesian_closed :=
  CartesianClosed (ob false) (hom false)
       (hom_eq_mixin false) (comp_mixin false)
       (cat_axioms false)
       cartesian_mixin
       terminated_mixin
       cartesian_closed_mixin.

End PLT.

Canonical Structure PLT.PLT.
Canonical Structure PLT.ord.
Canonical Structure PLT.dec.
Canonical Structure PLT.hom_ord.
Canonical Structure PLT.hom_eq.
Canonical Structure PLT.comp.
Canonical Structure PLT.homset_cpo.
Canonical Structure PLT.cocartesian.
Canonical Structure PLT.terminated.
Canonical Structure PLT.cartesian.
Canonical Structure PLT.cartesian_closed.


Coercion PLT.ord : PLT.ob >-> preord.
Coercion PLT.carrier : PLT.ob >-> Sortclass.

Global Close Scope category_ops_scope.

Notation PLT := (PLT.PLT false).
Notation "'∂PLT'" := (PLT.PLT true).

Notation "0" := (PLT.empty _) : plt_scope.
Notation "1" := (PLT.unit _) : plt_scope.
Notation "'Λ' f" := (PLT.curry f) : plt_scope.
Notation apply := (@PLT.app _ _ _).

Notation "〈 f , g 〉" := (@PLT.pair false _ _ _ (f)%plt (g)%plt) : plt_scope.
Notation "A × B" := (@PLT.prod false (A)%plt (B)%plt) : plt_scope.
Notation "A ⇒ B" := (@PLT.exp false (A)%plt (B)%plt) : plt_scope.
Notation "A + B" := (@PLT.sum false (A)%plt (B)%plt) : plt_scope.

Notation "《 f , g 》" := (@PLT.pair true _ _ _ (f)%plt (g)%plt) : plt_scope.
Notation "A ⊗ B" := (@PLT.prod true (A)%plt (B)%plt) : plt_scope.
Notation "A ⊸ B" := (@PLT.exp true (A)%plt (B)%plt) : plt_scope.
Notation "A ⊕ B" := (@PLT.sum true (A)%plt (B)%plt) : plt_scope.

Notation "'π₁'" := (@PLT.pi1 _ _ _) : plt_scope.
Notation "'π₂'" := (@PLT.pi2 _ _ _) : plt_scope.
Notation "'ι₁'" := (@PLT.iota1 _ _ _) : plt_scope.
Notation "'ι₂'" := (@PLT.iota2 _ _ _) : plt_scope.

Add Parametric Morphism (hf:bool) (C A B:PLT.ob hf) :
    (@PLT.pair hf C A B)
    with signature (Preord.ord_op (PLT.hom_ord hf C A)) ==>
                   (Preord.ord_op (PLT.hom_ord hf C B)) ==>
                   (Preord.ord_op (PLT.hom_ord hf C (PLT.prod A B)))
     as plt_le_pair_morphism.

Add Parametric Morphism (hf:bool) (C A B:PLT.ob hf) :
    (@PLT.sum_cases hf C A B)
    with signature (Preord.ord_op (PLT.hom_ord hf A C)) ==>
                   (Preord.ord_op (PLT.hom_ord hf B C)) ==>
                   (Preord.ord_op (PLT.hom_ord hf (PLT.sum A B) C))
     as plt_le_cases_morphism.

Add Parametric Morphism (hf:bool) (C A B:PLT.ob hf) :
    (@PLT.pair hf C A B)
    with signature (eq_op (PLT.hom_eq hf C A)) ==>
                   (eq_op (PLT.hom_eq hf C B)) ==>
                   (eq_op (PLT.hom_eq hf C (PLT.prod A B)))
     as plt_pair_morphism.

Add Parametric Morphism (hf:bool) (C A B:PLT.ob hf) :
    (@PLT.sum_cases hf C A B)
    with signature (eq_op (PLT.hom_eq hf A C)) ==>
                   (eq_op (PLT.hom_eq hf B C)) ==>
                   (eq_op (PLT.hom_eq hf (PLT.sum A B) C))
     as plt_cases_morphism.

Add Parametric Morphism (hf:bool) (C A B:PLT.ob hf) :
    (@PLT.curry hf C A B)
    with signature (Preord.ord_op (PLT.hom_ord hf (PLT.prod C A) B)) ==>
                   (Preord.ord_op (PLT.hom_ord hf C (PLT.exp A B)))
     as plt_le_curry_morphism.

Add Parametric Morphism (hf:bool) (C A B:PLT.ob hf) :
    (@PLT.curry hf C A B)
    with signature (eq_op (PLT.hom_eq hf (PLT.prod C A) B)) ==>
                   (eq_op (PLT.hom_eq hf C (PLT.exp A B)))
     as plt_curry_morphism.

Lemma plt_terminate_univ : forall (A:PLT) (f:A 1),
  f PLT.terminate false A.

Lemma hom_rel_pair_map hf (A B C D:PLT.PLT hf) (f:A C) (g:B D) x y x' y' :
  (x,y,(x',y')) PLT.hom_rel (PLT.pair_map f g) <->
  ((x,x') PLT.hom_rel f /\ (y,y') PLT.hom_rel g).

Lemma terminate_le_cancel (hf:bool) (A B:PLT.PLT hf) (f g:1 B) (a:A) :
  f PLT.terminate hf A g PLT.terminate hf A ->
  f g.

Lemma terminate_cancel (hf:bool) (A B:PLT.PLT hf) (f g:1 B) (a:A) :
  f PLT.terminate hf A g PLT.terminate hf A ->
  f g.

Section plt_const.
  Variable hf:bool.
  Variables A B:PLT.PLT hf.
  Variable b:B.

  Definition plt_const_rel :=
    eprod (eff_enum A (PLT.effective A))
                       (esubset_dec B (fun x => x b)
                          (fun x => eff_ord_dec B (PLT.effective B) x b)
                          (eff_enum B (PLT.effective B))).

  Lemma plt_const_rel_elem : forall a b',
    (a,b') plt_const_rel <-> b' b.

  Program Definition plt_const :=
    PLT.Hom hf A B plt_const_rel _ _.
End plt_const.

Theorem pair_bottom1 (C A B:ob PLT) (f:C A) :
   f, : C B .

Theorem pair_bottom2 (C A B:ob PLT) (g:C B) :
   : C A, g .

Theorem pi1_greatest (A B:ob PLT) (proj:AB A) :
  (forall C (f:C A) (g:C B), proj f, g f) ->
  proj π.

Theorem pi2_greatest (A B:ob PLT) (proj:AB B) :
  (forall C (f:C A) (g:C B), proj f, g g) ->
  proj π.

Definition antistrict (A B:PLT) (f:A B) :=
  forall a, exists b, (a,b) PLT.hom_rel f.

Definition nonbottom (A B:PLT) (f:A B) :=
  exists x, x PLT.hom_rel f.

Lemma antistrict_nonbottom (A B C:PLT) (f:A B) :
  antistrict f <-> (forall C (g:C A), nonbottom g -> nonbottom (f g)).

Theorem antistrict_pair_commute1 (C B:PLT) (g:C B) :
  antistrict g <-> forall A (f:C A), π f,g f.

Theorem antistrict_pair_commute2 (C A:PLT) (f:C A) :
  antistrict f <-> forall B (g:C B), π f, g g.