Library joinable


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.

Joinable relations

Joinable relations represent the compact elements of the continuous function space, and form the exponential object for profinite domains.
Here we carry out the techincal proofs required to show the joinable relations form an effective Plotkin preorder.
This definition of joinable relations is a minor modification of a definition given by Samson Abramsky. It is more obviously effective than the definition given by Carl Gunter in his dissertation.
Definition is_joinable_relation {A B:preord} hf (R:finset (A × B)) :=
  inh hf R /\
  forall (G:finset (A × B)) (HGinh:inh hf G), G R ->
    forall x, minimal_upper_bound x (image π G) ->
      exists y, (x,y) R /\ upper_bound y (image π G).

Definition joinable_relation hf (A B:preord)
  := { R:finset (A × B) | is_joinable_relation hf R }.

Definition joinable_rel_ord hf (A B:preord) (R S:joinable_relation hf A B) :=
  forall a b, (a,b) proj1_sig R ->
    exists a' b', (a',b') proj1_sig S /\ a' a /\ b b'.

Program Definition joinable_rel_ord_mixin hf (A B:preord) :
  Preord.mixin_of (joinable_relation hf A B) :=
  Preord.Mixin (joinable_relation hf A B) (joinable_rel_ord hf A B) _ _.

Canonical Structure joinable_rel_order hf (A B:preord) : preord :=
  Preord.Pack (joinable_relation hf A B) (joinable_rel_ord_mixin hf A B).

The ordering relation between joinable relations is decidable.
Lemma joinable_ord_dec
  hf
  (A B:preord)
  (HAeff : effective_order A)
  (HBeff : effective_order B)
  (R S:joinable_relation hf A B) :
  { R S }+{ R S }.

Given a finite relation, we can decide if it is joinable or not. If not, we can find evidence demonstrating where the relation is insufficently complete.
Lemma is_joinable_rel_dec0 hf
  (A B:preord)
  (HAeff : effective_order A)
  (HBeff : effective_order B)
  (HAplt : plotkin_order hf A)
  (R:finset (A × B)) (Rinh : inh hf R) :
  { is_joinable_relation hf R } +
  { exists (G:finset (A×B)), inh hf G /\ G R /\ exists z : A,
     minimal_upper_bound z (image π G) /\
     (forall q : B, (z, q) R -> ~ upper_bound q (image π G)) }.

Lemma is_joinable_rel_dec hf
  (A B:preord)
  (HAeff : effective_order A)
  (HBeff : effective_order B)
  (HAplt : plotkin_order hf A)
  (R:finset (A × B)) (Rinh : inh hf R) :
  { is_joinable_relation hf R } + { ~is_joinable_relation hf R }.

Lemma is_joinable_rel_dec' hf
  (A B:preord)
  (HAeff : effective_order A)
  (HBeff : effective_order B)
  (HAplt : plotkin_order hf A)
  (R:finset (A × B)) :
  { is_joinable_relation hf R } + { ~is_joinable_relation hf R }.

Joinable relations form an effective preorder. We can enumerate the joinable relations by first enumerating all the finite relations between A and B and selecting those that are joinable.
Program Definition joinable_rel_effective hf
  (A B:preord)
  (HAeff : effective_order A)
  (HBeff : effective_order B)
  (HAplt : plotkin_order hf A) :
  effective_order (joinable_rel_order hf A B)
  := EffectiveOrder _ _ _ _.

In this section, we show that, given an arbitrary finite relation M and an approximable relation R above M, we can "swell up" M into a joinable relation M' where M ⊆ M' ⊆ R.
This is done by a recursive procedure that, at each step, asks if M is joinable. If so, we are done. If not, there is some subset of M lacking the necessary upper bound. We add a new pair to M to fix the deficiency and recurse. The termination of this procedure relies critically on the fact that the MUB closure of a finite set is finite in Plotkin orders. Thus, at some point we will run out of elements that could possibly be added to M, and the procedure must terminate giving the desired joinable relation.
Then we can then show that the set of joinable relations below some approximable relation is directed; this will be important later for the proof that currying is an approximable relation.
Section directed_joinables.
  Variable hf:bool.
  Variables A B:preord.
  Variable HAeff : effective_order A.
  Variable HAplt : plotkin_order hf A.
  Variable HBeff : effective_order B.
  Variable HBplt : plotkin_order hf B.

  Let OD := OrdDec A (eff_ord_dec A HAeff).

  Variable R:erel A B.
  Hypothesis HR : forall x x' y y', x x' -> y' y -> (x,y) R -> (x',y') R.
  Hypothesis HRdir : forall a, directed hf (erel_image A B OD R a).

  Section swell.

  Variable RS : finset (A×B).
  Hypothesis RSinh : inh hf RS.

  Let RS' := finprod
     (mub_closure HAplt (image π RS))
     (mub_closure HBplt (image π RS)).

  Section swell_relation.
    Variable G:finset (A×B).
    Hypothesis HG : G R.
    Hypothesis HG' : G RS'.

    Variable G0:finset (A×B).
    Hypothesis HG0 : G0 G.
    Hypothesis G0inh : inh hf G0.

    Variable z:A.
    Hypothesis Hz : minimal_upper_bound z (image π G0).

    Lemma swell_row :
      exists q,
        (z,q) RS' /\ (z,q) R /\
        upper_bound q (image π G0).

    Variable XS : finset (A×B).
    Hypothesis HXS : forall x, x XS <-> x RS' /\ x G.

    Let ODAB := OrdDec (A×B) (eff_ord_dec _ (effective_prod HAeff HBeff)).

    Hypothesis noub : forall q, (z,q) G -> ~upper_bound q (image π G0).

    Lemma swell_relation :
      exists G':finset (A×B), exists XS':finset (A×B),
        length XS' < length XS /\
        G G' /\ G' R /\ G' RS' /\
        (forall x, x XS' <-> x RS' /\ x G').
  End swell_relation.

  Lemma swell_inductive_step
    (G:finset (A×B))
    (Ginh : inh hf G)
    (HG : G R) (HG': G RS')
    (XS:finset (A×B))
    (HXS: forall x, x XS <-> x RS' /\ x G) :

    is_joinable_relation hf G \/
    exists G':finset (A×B), exists XS':finset (A×B),
        length XS' < length XS /\
        G G' /\ G' R /\ G' RS' /\
        (forall x, x XS' <-> x RS' /\ x G').

  Lemma swell_aux (n:nat) : forall
    (G:finset (A×B))
    (Ginh : inh hf G)
    (HG : G R)
    (HG': G RS')
    (XS : finset (A×B))
    (HXS: forall x, x XS <-> x RS' /\ x G)
    (Hn : n = length XS),
    exists G':finset (A×B),
      G G' /\ G' R /\ is_joinable_relation hf G'.

  Hypothesis HRS : RS R.

  Lemma swell : exists G:finset (A×B),
    RS G /\ G R /\ is_joinable_relation hf G.

  End swell.

  Variable M:finset (joinable_rel_order hf A B).
  Hypothesis Minh : inh hf M.
  Hypothesis HM : forall S, S M -> proj1_sig S R.
  Let RS := concat _ (List.map (fun R => proj1_sig R) M) : finset (A×B).

  Lemma RS_elem :
    forall a, a RS -> (exists S, S M /\ a proj1_sig S).

  Lemma RS_elem' : forall S a, List.In S M -> a proj1_sig S -> a RS.

  Theorem directed_joinables :
    exists Q, upper_bound Q M /\ proj1_sig Q R.
End directed_joinables.

Section joinable_plt.
  Variable hf:bool.
  Variables A B:preord.
  Variable HAeff : effective_order A.
  Variable HAplt : plotkin_order hf A.
  Variable HBeff : effective_order B.
  Variable HBplt : plotkin_order hf B.

The intersection of an approximable relation with the cartesian product of MUB closed sets is a joinable relation.
  Lemma intersect_approx
    (R:A×B -> Prop)
    (Hdec : forall x, {R x}+{~R x})
    (HR : forall a a' b b', a a' -> b' b -> R (a,b) -> R (a',b'))
    (HRdir : forall a (M:finset B) (HMinh:inh hf M),
      (forall b, b M -> R (a,b)) ->
      exists z, R (a,z) /\ upper_bound z M)
    (P:finset A) (Q:finset B)
    (Hinh : if hf then exists x y, x P /\ y Q /\ R (x,y) else True)
    (HP:mub_closed hf A P) (HQ:mub_closed hf B Q) :
    is_joinable_relation hf (finsubset (A×B) R Hdec (finprod P Q)).

  Definition mkrel (R:joinable_relation hf A B) (x:A×B) :=
    exists a b, (a,b) proj1_sig R /\ a fst x /\ snd x b.

  Lemma mkrel_dec R : forall x, {mkrel R x}+{~mkrel R x}.

  Lemma mkrel_dir R :
    forall a (M:finset B) (HMinh:inh hf M), (forall b, b M -> mkrel R (a,b)) ->
      exists z, mkrel R (a,z) /\ upper_bound z M.

  Lemma mkrel_ord R : forall a a' b b', a a' -> b' b -> mkrel R (a,b) -> mkrel R (a',b').

  Lemma mkrel_mono : forall R S, R S ->
    forall x, mkrel R x -> mkrel S x.

  Lemma mkrel_mono' : forall (R S:joinable_relation hf A B),
    (forall x, x proj1_sig R -> mkrel S x) -> R S.

Joinable relations have normal sets. In particular, the set of all joinable relations that are subsets of the cartesian product of two MUB-closed sets is a normal set.
  Section join_rel_normal.
    Variable (P:finset A).
    Variable (Q:finset B).
    Variable (HP:mub_closed hf A P).
    Variable (HQ:mub_closed hf B Q).

    Fixpoint select_jrels (l:finset (finset (A×B))) : finset (joinable_rel_order hf A B) :=
      match l with
      | nil => nil
      | cons R l' =>
         match is_joinable_rel_dec' hf A B HAeff HBeff HAplt R with
         | left H => cons (exist _ R H) (select_jrels l')
         | right _ => select_jrels l'
         end
      end.

    Lemma select_jrels_elem1 : forall R (H:is_joinable_relation hf R) XS,
      R XS -> (exist _ R H : joinable_rel_order hf A B) select_jrels XS.

    Lemma select_jrels_elem2 : forall R XS,
      R select_jrels XS -> exists R', R R' /\ proj1_sig R' XS.

    Definition all_jrels := select_jrels (list_finsubsets (finprod P Q)).

    Lemma all_jrels_complete : forall R,
      R all_jrels <->
        exists R', R R' /\ (proj1_sig R' finprod P Q).

    Lemma all_jrels_inh' : forall x y, hf = true -> x P -> y Q -> exists R, R all_jrels.

    Lemma all_jrels_inh : inh hf P -> inh hf Q -> inh hf all_jrels.

    Lemma joinable_rels_normal :
      inh hf P -> inh hf Q ->
      normal_set (joinable_rel_order hf A B) (joinable_rel_effective hf A B HAeff HBeff HAplt) hf
        all_jrels.
  End join_rel_normal.

The joinable relations have normal sets
The joinable relations form a Plotkin order
  Definition joinable_rel_plt : plotkin_order hf (joinable_rel_order hf A B)
    := norm_plt
         (joinable_rel_order hf A B)
         (joinable_rel_effective hf A B HAeff HBeff HAplt)
         hf
         (joinable_rel_has_normals).

End joinable_plt.