Library approx_rels


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.

Constructions of approximable relations for the category PLT.

In this module we construct approxmiable relations to be used in the construction of the category PLT in profinite.v.
These include : identity, composition, pairing, pair projection, sum injection, sum case analysis, and the curry and apply operations.
All these relations work uniformly in both the category of pointed and unpointed effective Plotkin orders.

Definition ident_rel {A:preord} (HAeff:effective_order A) : erel A A :=
  esubset_dec _ (fun x => snd x fst x) (fun x => eff_ord_dec _ HAeff (snd x) (fst x))
    (eprod (eff_enum _ HAeff) (eff_enum _ HAeff)).

Definition compose_rel {A B C:preord} (HBeff:effective_order B)
  (S:erel B C) (R:erel A B) : erel A C :=
  image (mk_pair (π π) (π π))
   (esubset_dec _ (fun x => fst (snd x) snd (fst x))
            (fun x => eff_ord_dec _ HBeff (fst (snd x)) (snd (fst x)))
    (eprod R S)).

Lemma ident_elem A (HAeff:effective_order A) :
  forall x y, (x,y) ident_rel HAeff <-> y x.

Lemma compose_elem A B C (HBeff:effective_order B) (S:erel B C) (R:erel A B) :
  (forall x x' y y', x x' -> y' y -> (x,y) R -> (x',y') R) ->
  forall x z, (x,z) compose_rel HBeff S R <-> (exists y, (x,y) R /\ (y,z) S).

Lemma ident_ordering A (HAeff:effective_order A) :
  forall x x' y y', x x' -> y' y ->
    (x,y) ident_rel HAeff -> (x',y') ident_rel HAeff.

Definition directed_rel hf A B (HAeff:effective_order A) (R:erel A B):=
  forall x, directed hf (erel_image A B (OrdDec A (eff_ord_dec A HAeff)) R x).

Lemma ident_image_dir hf A (HAeff:effective_order A) : directed_rel hf A A HAeff (ident_rel HAeff).

Lemma compose_ordering A B C (HBeff:effective_order B) (S:erel B C) (R:erel A B) :
  (forall x x' y y', x x' -> y' y -> (x,y) R -> (x',y') R) ->
  (forall x x' y y', x x' -> y' y -> (x,y) S -> (x',y') S) ->
  (forall x x' y y', x x' -> y' y ->
    (x,y) compose_rel HBeff S R -> (x',y') compose_rel HBeff S R).

Lemma compose_directed hf A B C (HAeff:effective_order A) (HBeff:effective_order B) (S:erel B C) (R:erel A B) :
  (forall x x' y y', x x' -> y' y -> (x,y) R -> (x',y') R) ->
  (forall x x' y y', x x' -> y' y -> (x,y) S -> (x',y') S) ->
  directed_rel hf B C HBeff S ->
  directed_rel hf A B HAeff R ->
  directed_rel hf A C HAeff (compose_rel HBeff S R).

Lemma compose_assoc A B C D (HBeff:effective_order B) (HCeff:effective_order C)
  (T:erel C D) (S:erel B C) (R:erel A B) :
  compose_rel HCeff T (compose_rel HBeff S R)
  compose_rel HBeff (compose_rel HCeff T S) R.

Lemma compose_ident_rel2 : forall A B HBeff (f:erel A B),
  (forall x x' y y', x x' -> y' y -> (x,y) f -> (x',y') f) ->
  compose_rel HBeff f (ident_rel HBeff) f.

Lemma compose_ident_rel1 : forall A B HAeff (f:erel A B),
  (forall x x' y y', x x' -> y' y -> (x,y) f -> (x',y') f) ->
  compose_rel HAeff (ident_rel HAeff) f f.


Program Definition iota1_rel (A B:preord)
  (HA:effective_order A) : erel A (sum_preord A B) :=
  image (Preord.Hom (A×A) (A×sum_preord A B) (fun x => (fst x, inl (snd x))) _)
  (esubset_dec
    (A×A) (fun x => fst x snd x)
    (fun x => eff_ord_dec A HA (snd x) (fst x))
    (eprod (eff_enum A HA) (eff_enum A HA))).

Program Definition iota2_rel (A B:preord)
  (HB:effective_order B) : erel B (sum_preord A B) :=
  image (Preord.Hom (B×B) (B×sum_preord A B) (fun x => (fst x, inr (snd x))) _)
  (esubset_dec
    (B×B) (fun x => fst x snd x)
    (fun x => eff_ord_dec B HB (snd x) (fst x))
    (eprod (eff_enum B HB) (eff_enum B HB))).

Program Definition sum_cases (C A B:preord)
  (f: erel A C) (g:erel B C) : erel (sum_preord A B) C :=
  union2
    (image (Preord.Hom (A×C) (sum_preord A B × C) (fun x => (inl (fst x), snd x)) _) f)
    (image (Preord.Hom (B×C) (sum_preord A B × C) (fun x => (inr (fst x), snd x)) _) g).

Lemma sum_cases_elem (C A B:preord) (f:erel A C) (g:erel B C) x y :
  (x,y) sum_cases C A B f g <->
  match x with
  | inl a => (a,y) f
  | inr b => (b,y) g
  end.

Lemma iota1_elem : forall A B HA x y,
  (x,y) iota1_rel A B HA <-> exists x', y inl x' /\ x' x.

Lemma iota2_elem : forall A B HB x y,
  (x,y) iota2_rel A B HB <-> exists x', y inr x' /\ x' x.

Lemma iota1_ordering (A B:preord)
  (HAeff:effective_order A) :
  forall a a' b b',
    a a' ->
    b' b ->
    (a,b) iota1_rel A B HAeff ->
    (a',b') iota1_rel A B HAeff.

Lemma iota2_ordering (A B:preord)
  (HBeff:effective_order B) :
  forall a a' b b',
    a a' ->
    b' b ->
    (a,b) iota2_rel A B HBeff ->
    (a',b') iota2_rel A B HBeff.

Lemma sum_cases_ordering (C A B:preord) (f:erel A C) (g:erel B C) :
  (forall a a' b b', a a' -> b' b -> (a,b) f -> (a',b') f) ->
  (forall a a' b b', a a' -> b' b -> (a,b) g -> (a',b') g) ->
  (forall a a' b b', a a' -> b' b ->
    (a,b) sum_cases C A B f g -> (a',b') sum_cases C A B f g).

Lemma iota1_dir A B HAeff hf :
  directed_rel hf A (sum_preord A B) HAeff (iota1_rel A B HAeff).

Lemma iota2_dir A B HBeff hf :
  directed_rel hf B (sum_preord A B) HBeff (iota2_rel A B HBeff).

Lemma sum_cases_dir C A B HAeff HBeff hf (f:erel A C) (g:erel B C) :
  directed_rel hf A C HAeff f ->
  directed_rel hf B C HBeff g ->
  directed_rel hf (sum_preord A B) C (effective_sum HAeff HBeff) (sum_cases C A B f g).

Lemma iota1_cases_commute C A B HAeff HBeff (f:erel A C) (g:erel B C) :
  (forall a a' b b', a a' -> b' b -> (a,b) f -> (a',b') f) ->
  compose_rel (effective_sum HAeff HBeff)
      (sum_cases C A B f g) (iota1_rel A B HAeff) f.

Lemma iota2_cases_commute C A B HAeff HBeff (f:erel A C) (g:erel B C) :
  (forall a a' b b', a a' -> b' b -> (a,b) g -> (a',b') g) ->
  compose_rel (effective_sum HAeff HBeff)
      (sum_cases C A B f g) (iota2_rel A B HBeff) g.

Lemma sum_cases_univ C A B HAeff HBeff (f:erel A C) (g:erel B C) (h:erel (sum_preord A B) C):
  (forall a a' b b', a a' -> b' b -> (a,b) h -> (a',b') h) ->
  compose_rel (effective_sum HAeff HBeff) h (iota1_rel A B HAeff) f ->
  compose_rel (effective_sum HAeff HBeff) h (iota2_rel A B HBeff) g ->
  sum_cases C A B f g h.

Definition apply_acceptable hf (A B:preord)
  (tuple:(joinable_rel_order hf A B × A) × B) :=
  match tuple with
  | ((R,a),b) => exists a' b', (a',b') proj1_sig R /\ a' a /\ b b'
  end.

Lemma apply_acceptable_dec hf (A B:preord)
  (HAeff:effective_order A)
  (HBeff:effective_order B) :
  forall t, {apply_acceptable hf A B t} + { ~apply_acceptable hf A B t}.

Lemma apply_acceptable_ok hf (A B:preord) :
  forall x y, x y -> apply_acceptable hf A B x -> apply_acceptable hf A B y.

Definition apply_rel hf (A B:preord)
  (HAeff:effective_order A)
  (HBeff:effective_order B)
  (HAplt:plotkin_order hf A)
  : erel (joinable_rel_order hf A B × A) B :=
      esubset_dec _ (apply_acceptable hf A B) (apply_acceptable_dec hf A B HAeff HBeff)
         (eprod
             (eprod (eff_enum _ (joinable_rel_effective hf A B HAeff HBeff HAplt))
                    (eff_enum A HAeff))
             (eff_enum B HBeff)).

Lemma apply_rel_elem hf A B HAeff HBeff HAplt :
  forall x y R,
    ((R,x),y) apply_rel hf A B HAeff HBeff HAplt <->
    exists x', exists y', (x',y') proj1_sig R /\ x' x /\ y y'.

Lemma apply_rel_ordering hf (A B:preord)
  (HAeff:effective_order A)
  (HBeff:effective_order B)
  (HAplt:plotkin_order hf A) :
  forall R R' b b',
    R R' ->
    b' b ->
    (R,b) apply_rel hf A B HAeff HBeff HAplt ->
    (R',b') apply_rel hf A B HAeff HBeff HAplt.

Lemma apply_rel_dir hf (A B:preord)
  (HAeff:effective_order A)
  (HBeff:effective_order B)
  (HAplt:plotkin_order hf A) :
  directed_rel hf
    ((joinable_rel_order hf A BA) B
    (effective_prod (joinable_rel_effective hf A B HAeff HBeff HAplt) HAeff)
    (apply_rel hf A B HAeff HBeff HAplt).

Definition pair_rel {A B C:preord} (HCeff:effective_order C)
  (R:erel C A) (S:erel C B) : erel C (A×B) :=
  image (mk_pair (π π) (mk_pair (π π) (π π)))
   (esubset_dec _ (fun x => fst (fst x) fst (snd x))
            (fun x => PREORD_EQ_DEC _ (OrdDec _ (eff_ord_dec _ HCeff)) (fst (fst x)) (fst (snd x)))
    (eprod R S)).

Definition pi1_rel {A B:preord}
  (HA:effective_order A) (HB:effective_order B)
  : erel (A×B) A :=
  esubset_dec
    ((A×BA) (fun x => fst (fst x) snd x)
    (fun x => eff_ord_dec A HA (snd x) (fst (fst x)))
  (eprod (eprod (eff_enum A HA) (eff_enum B HB)) (eff_enum A HA)).

Definition pi2_rel {A B:preord}
  (HA:effective_order A) (HB:effective_order B)
  : erel (A×B) B :=
  esubset_dec
    ((A×BB) (fun x => snd (fst x) snd x)
    (fun x => eff_ord_dec B HB (snd x) (snd (fst x)))
  (eprod (eprod (eff_enum A HA) (eff_enum B HB)) (eff_enum B HB)).

Lemma pi1_rel_elem A B (HA:effective_order A) (HB:effective_order B) :
  forall a b a', ((a,b),a') pi1_rel HA HB <-> a a'.

Lemma pi2_rel_elem A B (HA:effective_order A) (HB:effective_order B) :
  forall a b b', ((a,b),b') pi2_rel HA HB <-> b b'.

Lemma pair_rel_elem A B C (HCeff:effective_order C)
  (R:erel C A) (S:erel C B) :
  forall c x y, (c,(x,y)) pair_rel HCeff R S <-> ((c,x) R /\ (c,y) S).

Lemma pi1_rel_ordering A B (HA:effective_order A) (HB:effective_order B) :
  forall x x' y y', x x' -> y' y ->
    (x,y) pi1_rel HA HB -> (x',y') pi1_rel HA HB.

Lemma pi2_rel_ordering A B (HA:effective_order A) (HB:effective_order B) :
  forall x x' y y', x x' -> y' y ->
    (x,y) pi2_rel HA HB -> (x',y') pi2_rel HA HB.

Lemma pair_rel_ordering A B C (HCeff:effective_order C)
  (R:erel C A) (S:erel C B)
  (HR:forall x x' y y', x x' -> y' y -> (x,y) R -> (x',y') R)
  (HS:forall x x' y y', x x' -> y' y -> (x,y) S -> (x',y') S) :
  forall x x' y y', x x' -> y' y ->
    (x,y) pair_rel HCeff R S -> (x',y') pair_rel HCeff R S.

Lemma pi1_rel_dir hf A B (HA:effective_order A) (HB:effective_order B) :
  directed_rel hf (A×B) A (effective_prod HA HB) (pi1_rel HA HB).

Lemma pi2_rel_dir hf A B (HA:effective_order A) (HB:effective_order B) :
  directed_rel hf (A×B) B (effective_prod HA HB) (pi2_rel HA HB).

Lemma pair_rel_dir hf
 A B C (HCeff:effective_order C)
  (R:erel C A) (S:erel C B)
  (HR:forall x x' y y', x x' -> y' y -> (x,y) R -> (x',y') R)
  (HS:forall x x' y y', x x' -> y' y -> (x,y) S -> (x',y') S) :
  directed_rel hf C A HCeff R -> directed_rel hf C B HCeff S ->
  directed_rel hf C (A×B) HCeff (pair_rel HCeff R S).

Lemma pair_proj_commute1_le C A B
  (HA:effective_order A) (HB:effective_order B) (HC:effective_order C)
  (R:erel C A) (S:erel C B)
  (HR:forall x x' y y', x x' -> y' y -> (x,y) R -> (x',y') R)
  (HS:forall x x' y y', x x' -> y' y -> (x,y) S -> (x',y') S) :
  compose_rel (effective_prod HA HB) (pi1_rel HA HB) (pair_rel HC R S) R.

Lemma pair_proj_commute1 C A B
  (HA:effective_order A) (HB:effective_order B) (HC:effective_order C)
  (R:erel C A) (S:erel C B)
  (HR:forall x x' y y', x x' -> y' y -> (x,y) R -> (x',y') R)
  (HS:forall x x' y y', x x' -> y' y -> (x,y) S -> (x',y') S)
  (HSdir:directed_rel false C B HC S) :
  compose_rel (effective_prod HA HB) (pi1_rel HA HB) (pair_rel HC R S) R.

Lemma pair_proj_commute2_le C A B
  (HA:effective_order A) (HB:effective_order B) (HC:effective_order C)
  (R:erel C A) (S:erel C B)
  (HR:forall x x' y y', x x' -> y' y -> (x,y) R -> (x',y') R)
  (HS:forall x x' y y', x x' -> y' y -> (x,y) S -> (x',y') S) :
  compose_rel (effective_prod HA HB) (pi2_rel HA HB) (pair_rel HC R S) S.

Lemma pair_proj_commute2 C A B
  (HA:effective_order A) (HB:effective_order B) (HC:effective_order C)
  (R:erel C A) (S:erel C B)
  (HR:forall x x' y y', x x' -> y' y -> (x,y) R -> (x',y') R)
  (HS:forall x x' y y', x x' -> y' y -> (x,y) S -> (x',y') S)
  (HRdir:directed_rel false C A HC R) :
  compose_rel (effective_prod HA HB) (pi2_rel HA HB) (pair_rel HC R S) S.

Lemma pair_rel_universal_le C A B
  (HA:effective_order A) (HB:effective_order B) (HC:effective_order C)
  (R:erel C A) (S:erel C B)
  (HR:forall x x' y y', x x' -> y' y -> (x,y) R -> (x',y') R)
  (HS:forall x x' y y', x x' -> y' y -> (x,y) S -> (x',y') S)
  (PAIR:erel C (A×B))
  (HPAIR :
   forall (x x' : C) (y y' : A × B),
     x x' -> y' y -> (x, y) PAIR -> (x', y') PAIR)
  (HCOMM1 : compose_rel (effective_prod HA HB) (pi1_rel HA HB) PAIR R)
  (HCOMM2 : compose_rel (effective_prod HA HB) (pi2_rel HA HB) PAIR S) :
  PAIR pair_rel HC R S.

Lemma pair_rel_universal hf C A B
  (HA:effective_order A) (HB:effective_order B) (HC:effective_order C)
  (R:erel C A) (S:erel C B)
  (HR:forall x x' y y', x x' -> y' y -> (x,y) R -> (x',y') R)
  (HS:forall x x' y y', x x' -> y' y -> (x,y) S -> (x',y') S)
  (PAIR:erel C (A×B))
  (HPAIR :
   forall (x x' : C) (y y' : A × B),
     x x' -> y' y -> (x, y) PAIR -> (x', y') PAIR)
  (HPAIRdir : directed_rel hf C (A×B) HC PAIR)
  (HCOMM1 : compose_rel (effective_prod HA HB) (pi1_rel HA HB) PAIR R)
  (HCOMM2 : compose_rel (effective_prod HA HB) (pi2_rel HA HB) PAIR S) :
  PAIR pair_rel HC R S.


Definition pair_rel' {A B C D:preord}
  (R:erel A B) (S:erel C D) : erel (A×C) (B×D) :=
  image (mk_pair
          (mk_pair (π π) (π π))
          (mk_pair (π π) (π π)))
    (eprod R S).

Lemma pair_rel_elem' A B C D (R:erel A B) (S:erel C D)
  (HR:forall x x' y y', x x' -> y' y -> (x,y) R -> (x',y') R)
  (HS:forall x x' y y', x x' -> y' y -> (x,y) S -> (x',y') S) :
  forall a b c d, ((a,b),(c,d)) pair_rel' R S <->
    ((a,c) R /\ (b,d) S).

Lemma pair_rel_order' A B C D (R:erel A B) (S:erel C D)
  (HR:forall x x' y y', x x' -> y' y -> (x,y) R -> (x',y') R)
  (HS:forall x x' y y', x x' -> y' y -> (x,y) S -> (x',y') S) :
   forall x x' y y',
   x x' ->
   y' y ->
   (x, y) pair_rel' R S ->
   (x', y') pair_rel' R S.

Lemma pair_rel_eq
 A B C D (R:erel A B) (S:erel C D)
  (HA:effective_order A) (HC:effective_order C)
  (HR:forall x x' y y', x x' -> y' y -> (x,y) R -> (x',y') R)
  (HS:forall x x' y y', x x' -> y' y -> (x,y) S -> (x',y') S) :
  pair_rel' R S
  pair_rel (effective_prod HA HC)
    (compose_rel HA R (pi1_rel HA HC)) (compose_rel HC S (pi2_rel HA HC)).


Lemma all_finset_setdec_elem : forall A P X a
  (HP:forall x y a, x y -> a P x -> a P y),
  (a all_finset_setdec A P X <->
   (forall x, x X -> a P x)).

Section curry.
  Variable hf:bool.
  Variables A B C:preord.
  Variable HAeff:effective_order A.
  Variable HBeff:effective_order B.
  Variable HCeff:effective_order C.
  Variable HAplt:plotkin_order hf A.

  Variable R:erel (C×A) B.
  Hypothesis HR :
    forall x x' y y', x x' -> y' y -> (x,y) R -> (x',y') R.

  Definition curry_acceptable (tuple:C×(joinable_rel_order hf A B)) :=
    match tuple with
    | (c,R') => forall ab, ab proj1_sig R' -> ((c,fst ab),snd ab) R
    end.

  Let Reff : effective_order ((C×AB) :=
    effective_prod (effective_prod HCeff HAeff) HBeff.

  Definition inset_decset (A:preord) (HA:effective_order A) (X:eset A) (x:A)
    : eset unitpo :=
    image (const tt) (esubset_dec _ _
      (PREORD_EQ_DEC _ (OrdDec _ (eff_ord_dec _ HA)) x) X).

  Lemma curry_acceptable_semidec :
    forall x, semidec (curry_acceptable x).

  Definition curry_rel : erel C (joinable_rel_order hf A B) :=
    esubset _ curry_acceptable_semidec
      (eprod (eff_enum C HCeff)
             (eff_enum _ (joinable_rel_effective hf A B HAeff HBeff HAplt))).

  Lemma curry_rel_elem : forall c (R':joinable_relation hf A B),
    (c,R') curry_rel <-> (forall a b, (a,b) proj1_sig R' -> ((c,a),b) R).

  Lemma curry_rel_ordering :
    forall x x' y y',
      x x' ->
      y' y ->
      (x,y) curry_rel ->
      (x',y') curry_rel.

  Hypothesis HRdir : directed_rel hf (C×A) B (effective_prod HCeff HAeff) R.
  Variable HBplt:plotkin_order hf B.

  Let R' c :=
    image (mk_pair (π π) π)
    (esubset_dec ((C×AB) (fun q => fst (fst q) c)
    (fun q =>
      PREORD_EQ_DEC _ (OrdDec C (eff_ord_dec C HCeff)) (fst (fst q)) c)
    R).

  Lemma R'_R : forall a b c,
    ((c,a),b) R <-> (a,b) R' c.

  Lemma curry_rel_dir :
    directed_rel hf C (joinable_rel_order hf A B) HCeff curry_rel.

  Lemma curry_universal
    (CURRY:erel C (joinable_rel_order hf A B))
    (HC : forall x x' y y',
      x x' -> y' y ->
      (x,y) CURRY -> (x',y') CURRY)
    (HCdir : directed_rel hf C (joinable_rel_order hf A B) HCeff CURRY) :
    (compose_rel (effective_prod (joinable_rel_effective hf A B HAeff HBeff HAplt) HAeff)
           (apply_rel hf A B HAeff HBeff HAplt)
           (pair_rel' CURRY (ident_rel HAeff)))
     R ->
    CURRY curry_rel.

  Lemma curry_apply :
    (compose_rel (effective_prod (joinable_rel_effective hf A B HAeff HBeff HAplt) HAeff)
           (apply_rel hf A B HAeff HBeff HAplt)
           (pair_rel' curry_rel (ident_rel HAeff)))
     R.
End curry.