Library models.IntStrat

Require Import Classical.
Require Import FunctionalExtensionality.
Require Import Program.Equality.
Require Import LogicalRelations.
Require Import Poset.
Require Import Lattice.
Require Import Downset.

Preliminaries

This instance is needed for rewrites under sup and inf to work.

Instance funext_subrel {A B} :
subrelation (pointwise_relation _ eq) (@eq (A → B)).

Helpful tactic for messy inversions

Ltac xsubst :=
  repeat progress
    (match goal with
     | H : ?x = ?x |- _ ⇒
         clear H
     | H : existT _ _ _ = existT _ _ _ |- _ ⇒
         apply inj_pair2 in H
     end ||
     subst ||
     discriminate).

Miscellaneous rewriting rules

Lemma all_eq_some {A} {P : A → Prop} (a:A) :
(∀ x, Some a = Some x → P x ) ↔ P a.

Lemma all_eq_none {A} {P : A → Prop} :
(∀ x, None = Some x → P x ) ↔ True.

§2 COMPOSITIONAL SEMANTICS FOR VERIFICATION

This section introduces the basic definitions below. However, for the most part it is a high-level overview of the framework which is formally defined in the following section. Note that we have formalized examples separately.

§2.2 Effect Signatures

Definition 2.1 (Effect signature)

Record esig :=
  {
    op :> Type;
    ar : op → Type;
  }.

Arguments ar {_}.
Declare Scope esig_scope.
Delimit Scope esig_scope with esig.
Bind Scope esig_scope with esig.

Signature homomorphisms

Although they are not defined explicitly in the paper, signature homomorphisms of the following kind capture the patterns in many basic strategies with a fixed shape similar to that of id. They correspond to natural transformations between the polynomial Set endofunctors associated with the signatures.

Defining such strategies based on their signature homomorphism representation is both more convenient and makes it easier to reason about them.

Definition

Although we could use sigT and define signature homomorphisms as terms of type ∀ q : op F, {m : op E & ar m → ar q}, the specialized version below is a little bit easier to use in some cases. It is essentially the Set endofunctor associated with E.

Record application (E : esig) (X : Type) :=
  econs {
    operator : op E;
    operand : ar operator → X;
  }.

Coercion application : esig >-> Funclass.
Arguments econs {E X}.
Arguments operator {E X}.
Arguments operand {E X}.

Definition emor (E F : esig) :=
  ∀ q : F, application E (ar q).

Declare Scope emor_scope.
Delimit Scope emor_scope with emor.
Bind Scope emor_scope with emor.
Open Scope emor_scope.

Compositional structure

Definition eid {E} : emor E E :=
  fun q ⇒ econs q (fun r ⇒ r).

Definition ecomp {E F G} (g : emor F G) (f : emor E F) : emor E G :=
  fun q ⇒
    econs (operator (f (operator (g q))))
          (fun v ⇒ operand _ (operand _ v)).

Lemma ecomp_eid_l {E F} (f : emor E F) :
  ecomp eid f = f.

Lemma ecomp_eid_r {E F} (f : emor E F) :
  ecomp f eid = f.

Lemma ecomp_assoc {E F G H} (f : emor E F) (g : emor F G) (h : emor G H) :
  ecomp (ecomp h g) f = ecomp h (ecomp g f).

Coercion eid : esig >-> emor.
Infix "∘" := ecomp : emor_scope.

§2.6 Combining Effect Signatures

Definition 2.9 (Sum of signatures)

We only formalize the binary and nullary cases.

Canonical Structure fcomp E F :=
  {|
    op := op E + op F;
    ar m := match m with inl m | inr m ⇒ ar m end;
  |}.

Infix "+" := fcomp : esig_scope.

Canonical Structure Empty_sig :=
  {|
    op := Empty_set;
    ar m := match m with end;
  |}.

Notation "0" := Empty_sig : esig_scope.

Monoidal structure with respect to emor

Functoriality of fcomp

Definition fcomp_emor {E1 F1 E2 F2} (f1: emor E1 F1) (f2: emor E2 F2): emor (E1 +E2) (F1 +F2) :=
  fun q ⇒
    match q with
      | inl q1 ⇒ econs (inl (operator (f1 q1))) (operand (f1 q1))
      | inr q2 ⇒ econs (inr (operator (f2 q2))) (operand (f2 q2))
    end.

Infix "+" := fcomp_emor : emor_scope.

Lemma fcomp_eid (E F : esig) :
  @eid E + @eid F = @eid (E + F).

Lemma fcomp_ecomp {E1 F1 G1 E2 F2 G2 : esig} :
  ∀ (f1 : emor E1 F1) (g1 : emor F1 G1) (f2 : emor E2 F2) (g2 : emor F2 G2),
    (g1 ∘ f1 ) + (g2 ∘ f2 ) = (g1 + g2 ) ∘ (f1 + f2 ).

Left (λ) and right (ρ) unitors and their inverses

Definition flu {E} : emor (0 + E) E :=
  fun q ⇒ econs (inr q) (fun r ⇒ r).

Definition flur {E} : emor E (0 + E) :=
  fun q ⇒ match q with
             | inl q ⇒ match q with end
             | inr q ⇒ econs q (fun r ⇒ r)
           end.

Lemma flu_flur {E} :
  ecomp (@flu E) (@flur E) = eid.

Lemma flur_flu {E} :
  ecomp (@flur E) (@flu E) = eid.

Definition fru {E} : emor (E + 0) E :=
  fun q ⇒ econs (inl q) (fun r ⇒ r).

Definition frur {E} : emor E (E + 0) :=
  fun q ⇒ match q with
             | inl q ⇒ econs q (fun r ⇒ r)
             | inr q ⇒ match q with end
           end.

Lemma fru_frur {E} :
  ecomp (@fru E) (@frur E) = eid.

Lemma frur_fru {E} :
  ecomp (@frur E) (@fru E) = eid.

Associator (α) and its inverse

Definition fassoc {E F G} : emor ((E + F ) + G) (E + (F + G )) :=
  fun q ⇒
    match q with
      | inl q1 ⇒ econs (inl (inl q1)) (fun r ⇒ r)
      | inr (inl q2) ⇒ econs (inl (inr q2)) (fun r ⇒ r)
      | inr (inr q3) ⇒ econs (inr q3) (fun r ⇒ r)
    end.

Definition fassocr {E F G} : emor (E + (F + G )) ((E + F ) + G) :=
  fun q ⇒
    match q with
      | inl (inl q1) ⇒ econs (inl q1) (fun r ⇒ r)
      | inl (inr q2) ⇒ econs (inr (inl q2)) (fun r ⇒ r)
      | inr q3 ⇒ econs (inr (inr q3)) (fun r ⇒ r)
    end.

Lemma fassocr_fassoc {E F G} :
  ecomp (@fassocr E F G) (@fassoc E F G) = eid.

Lemma fassoc_fassocr {E F G} :
  ecomp (@fassoc E F G) (@fassocr E F G) = eid.

Triangle and pentagon identities

Lemma flu_fassoc E F :
  (@eid E + @flu F ) ∘ fassoc = @fru E + @eid F.

Lemma fassoc_fassoc E F G H :
  @fassoc E F (G + H) ∘ @fassoc (E + F) G H =
  (@eid E + @fassoc F G H ) ∘ @fassoc E (F + G) H ∘ (@fassoc E F G + @eid H ).

Braiding (γ)

Definition fswap {E F} : emor (E + F) (F + E) :=
  fun q ⇒
    match q with
      | inl q ⇒ econs (inr q) (fun r ⇒ r)
      | inr q ⇒ econs (inl q) (fun r ⇒ r)
    end.

Unit coherence property

Lemma fswap_unit {E} :
flu ∘ (@fswap E 0) = fru.

Hexagon identity

Lemma fswap_assoc {E F G} :
(@eid F + @fswap E G ) ∘ @fassoc F E G ∘ (@fswap E F + @eid G ) =
@fassoc F G E ∘ @fswap E (F + G) ∘ @fassoc E F G.

The braiding is its own inverse

Lemma fswap_fswap {E F} :
@fswap F E ∘ @fswap E F = @eid (E + F).

Duplication and projections

Flat composition is the cartesian product with respect to effect signature homomorphisms. This will no longer be true when we move to our more sophisticated strategy construction, however the morphisms below remain useful as a way to duplicate or forget parts of a component's interface.

Terminal morphism

Definition fdrop {E} : emor E 0 :=
fun q ⇒ match q with end.

Lemma fdrop_uniq {E} (f : emor E 0) :
f = fdrop.

Left projection

Definition ffst {E F} : emor (E + F) E :=
fun q ⇒ econs (inl q) (fun r ⇒ r).

Lemma ffst_fdrop {E F} :
@ffst E F = fru ∘ (eid + fdrop ).

Right projection

Definition fsnd {E F} : emor (E + F) F :=
fun q ⇒ econs (inr q) (fun r ⇒ r).

Lemma fsnd_fdrop {E F} :
@fsnd E F = flu ∘ (fdrop + eid ).

Diagonal morphism

Definition fdup {E} : emor E (E + E) :=
  fun q ⇒ match q with
             | inl q ⇒ econs q (fun r ⇒ r)
             | inr q ⇒ econs q (fun r ⇒ r)
           end.

Lemma ffst_fdup {E} :
  ffst ∘ fdup = @eid E.

Lemma fsnd_fdup {E} :
  fsnd ∘ fdup = @eid E.

Tupling

Section FPAIR.
  Context {E F1 F2} (f1 : emor E F1) (f2 : emor E F2).

  Definition fpair : emor E (F1 + F2) :=
    fun q ⇒ match q with
               | inl q1 ⇒ f1 q1
               | inr q2 ⇒ f2 q2
             end.

  Lemma fpair_uniq (f : emor E (F1 + F2)) :
    ffst ∘ f = f1 →
    fsnd ∘ f = f2 →
    f = fpair.

  Lemma fpair_expand :
    fpair = (f1 + f2 ) ∘ fdup.
End FPAIR.

§3 STRATEGY MODEL

§3.1 Strategies

Section STRAT.
Context {E F : esig}.

Def 3.1 (Strategy)

  Variant position :=
    | ready
    | running (q : op F)
    | suspended (q : op F) (m : op E).

  Variant move : position → position → Type :=
    | oq (q : op F) : move ready (running q)
    | pq {q} (m : op E) : move (running q) (suspended q m)
    | oa {q m} (n : ar m) : move (suspended q m) (running q)
    | pa {q} (r : ar q) : move (running q) ready.

  Inductive play : position → Type :=
    | pnil_ready : play ready
    | pnil_suspended q m : play (suspended q m)
    | pcons {i j} : move i j → play j → play i.

  Inductive pref : ∀ {i : position}, relation (play i) :=
    | pnil_ready_pref t : pref pnil_ready t
    | pnil_suspended_pref {q m} t : pref (@pnil_suspended q m) t
    | pcons_pref {i j} (e : move i j) s t : pref s t → pref (pcons e s) (pcons e t).

  Lemma pref_refl i s :
    @pref i s s.

  Program Canonical Structure play_poset (p : position) : poset :=
    {|
      poset_carrier := play p;
      ref := pref;
    |}.

  Definition strat (p : position) :=
    poset_carrier (downset (play_poset p)).

Useful lemmas

  Lemma strat_closed {p} (σ : strat p) (s t : play p) :
    Downset.has σ t →
    pref s t →
    Downset.has σ s.

  Lemma strat_has_any_pnil_ready (σ : strat ready) (s : play ready) :
    Downset.has σ s →
    Downset.has σ pnil_ready.

  Lemma strat_has_any_pnil_suspended {q m} (σ : strat (suspended q m)) s :
    Downset.has σ s →
    Downset.has σ (pnil_suspended q m).

  Lemma pcons_eq_inv_l {i j} (m1 m2 : move i j) (s1 s2 : play j) :
    pcons m1 s1 = pcons m2 s2 → m1 = m2.

  Lemma pcons_eq_inv_r {i j} (m1 m2 : move i j) (s1 s2 : play j) :
    pcons m1 s1 = pcons m2 s2 → s1 = s2.

  Lemma oa_eq_inv q m n1 n2 :
    @oa q m n1 = @oa q m n2 → n1 = n2.

  Lemma pa_eq_inv q r1 r2 :
    @pa q r1 = @pa q r2 → r1 = r2.

  Lemma pcons_oa_inv q m (n1 n2 : ar m) (s1 s2: play (running q)) :
    pcons (oa n1) s1 = pcons (oa n2) s2 → n1 = n2 ∧ s1 = s2.

  Lemma pcons_pa_inv q (r1 r2 : ar q) s1 s2 :
    pcons (pa r1) s1 = pcons (pa r2) s2 → r1 = r2 ∧ s1 = s2.

Determinism

  Inductive pcoh : ∀ {i : position}, relation (play i) :=
    | pnil_ready_pcoh_l s : pcoh pnil_ready s
    | pnil_ready_pcoh_r s : pcoh s pnil_ready
    | pnil_suspended_pcoh_l q m s : pcoh (pnil_suspended q m) s
    | pnil_suspended_pcoh_r q m s : pcoh s (pnil_suspended q m)
    | pcons_pcoh {i j} (m : move i j) (s t : play j) :
        pcoh s t → pcoh (pcons m s) (pcons m t)
    | pcons_pcoh_oq (q1 q2 : F) s1 s2 :
        q1 ≠ q2 → pcoh (pcons (oq q1) s1) (pcons (oq q2) s2)
    | pcons_pcoh_oa {q m} (n1 n2 : ar m) (s1 s2 : play (running q)) :
        n1 ≠ n2 → pcoh (pcons (oa n1) s1) (pcons (oa n2) s2).

  Global Instance pcoh_refl i :
    Reflexive (@pcoh i).

  Global Instance pcoh_sym i :
    Symmetric (@pcoh i).

  Class Deterministic {p} (σ : strat p) :=
    {
      determinism : ∀ s t, Downset.has σ s → Downset.has σ t → pcoh s t;
    }.

  Lemma pcoh_inv_pq {q} (m1 m2 : E) (s1 s2 : play (suspended q _)) :
    pcoh (pcons (pq m1) s1) (pcons (pq m2) s2) →
    m1 = m2.

  Lemma pcoh_inv_pa {q} (r1 r2 : ar q) (s1 s2 : play ready) :
    pcoh (pcons (pa r1) s1) (pcons (pa r2) s2) →
    r1 = r2.

Residuals

  Section NEXT.
    Context {i j} (e : move i j).
    Obligation Tactic := cbn.

    Definition scons : strat j → strat i :=
      Downset.map (pcons e).

    Global Instance scons_deterministic (σ : strat j) :
      Deterministic σ →
      Deterministic (scons σ).

    Program Definition next (σ : strat i) : strat j :=
      {| Downset.has s := Downset.has σ (pcons e s) |}.

    Global Instance next_deterministic (σ : strat i) :
      Deterministic σ →
      Deterministic (next σ).

    Lemma scons_next_adj σ τ :
      scons σ [= τ ↔ σ [= next τ.
  End NEXT.
End STRAT.

Arguments strat : clear implicits.
Infix "::" := pcons.

Notation "E ->> F" := (strat E F ready) (at level 99, right associativity).
Declare Scope strat_scope.
Delimit Scope strat_scope with strat.
Bind Scope strat_scope with strat.
Open Scope strat_scope.

To make using determinism properties easier, we provide the determinism tactic below. Additional hints in the determinism database can used to establish that the strategy makes particular moves.

Global Hint Resolve determinism pcoh_inv_pq pcoh_inv_pa : determinism.

Global Hint Extern 1 (Downset.has ?σ (?e :: ?s)) ⇒
       change (Downset.has (next e σ) s) : determinism.

Ltac determinism m m' :=
  assert (m' = m) by eauto 10 with determinism;
  subst m'.

Signature homomorphisms

Signature homomorphisms define simple strategies.

Section EMOR_STRAT.
  Context {E F} (f : emor E F).
  Obligation Tactic := cbn.

  Variant epos : position → Type :=
    | eready : epos ready
    | esuspended q : epos (suspended q (operator (f q))).

  Inductive emor_has : ∀ {i}, epos i → play i → Prop :=
    | emor_ready :
        emor_has eready pnil_ready
    | emor_question q s :
        emor_has (esuspended q) s →
        emor_has eready (oq q :: pq (operator (f q)) :: s)
    | emor_suspended q :
        emor_has (esuspended q) (pnil_suspended _ _)
    | emor_answer q r s :
        emor_has eready s →
        emor_has (esuspended q) (oa r :: pa (operand (f q) r) :: s).

  Program Definition emor_when {i} p : strat E F i :=
    {| Downset.has := emor_has p |}.

  Definition emor_strat :=
    emor_when eready.

Residuals

  Lemma emor_next_question q :
    next (pq (operator (f q))) (next (oq q) emor_strat) =
    emor_when (esuspended q).

  Lemma emor_next_answer q r :
    next (pa (operand (f q) r)) (next (oa r) (emor_when (esuspended q))) =
    emor_strat.

  Lemma emor_next q r :
    (next (pa (operand (f q) r))
       (next (oa r)
          (next (pq (operator (f q)))
             (next (oq q) emor_strat)))) =
      emor_strat.
End EMOR_STRAT.

Arguments eready {_ _ _}.
Arguments esuspended {_ _ _}.

§3.2 Layered Composition

Def 3.4 (Layered Composition of Strategies)

The identity strategy can be defined using the corresponding signature homomorphism.

Notation id E := (emor_strat (@eid E)).

Lemma id_next {E} q r :
(next (pa r) (next (oa r) (next (pq q) (next (oq q) (id E))))) = id E.

Layered composition is more complex.

Section COMPOSE.
  Context {E F G : esig}.
  Obligation Tactic := cbn.

  Variant cpos : @position F G → @position E F → @position E G → Type :=
    | cpos_ready :
        cpos ready ready ready
    | cpos_left q :
        cpos (running q) ready (running q)
    | cpos_right q m :
        cpos (suspended q m) (running m) (running q)
    | cpos_suspended q m u :
        cpos (suspended q m) (suspended m u) (suspended q u).

  Inductive comp_has :
    ∀ {i j k} (p: cpos i j k), play i → play j → play k → Prop :=
    | comp_ready t :
        comp_has cpos_ready (pnil_ready) t (pnil_ready)
    | comp_oq q s t w :
        comp_has (cpos_left q) s t w →
        comp_has cpos_ready (oq q :: s) t (oq q :: w)
    | comp_lq q m s t w :
        comp_has (cpos_right q m) s t w →
        comp_has (cpos_left q) (pq m :: s) (oq m :: t) w
    | comp_rq q m u s t w :
        comp_has (cpos_suspended q m u) s t w →
        comp_has (cpos_right q m) s (pq u :: t) (pq u :: w)
    | comp_suspended q m u s :
        comp_has (cpos_suspended q m u) s (pnil_suspended m u) (pnil_suspended q u)
    | comp_oa q m u v s t w :
        comp_has (cpos_right q m) s t w →
        comp_has (cpos_suspended q m u) s (oa v :: t) (oa v :: w)
    | comp_ra q m n s t w :
        comp_has (cpos_left q) s t w →
        comp_has (cpos_right q m) (oa n :: s) (pa n :: t) w
    | comp_la q r s t w :
        comp_has cpos_ready s t w →
        comp_has (cpos_left q) (pa r :: s) t (pa r :: w).

  Hint Constructors comp_has : core.
  Hint Constructors pref : core.
  Hint Resolve (fun E F i ⇒ reflexivity (R := @pref E F i)) : core.

  Lemma comp_has_pref {i j k} (p : cpos i j k) s t w :
    comp_has p s t w →
    ∀ w', w' [= w → ∃ s' t', s' [= s ∧ t' [= t ∧ comp_has p s' t' w'.

  Program Definition compose_when {i j k} p (σ : strat F G i) (τ : strat E F j) : strat E G k :=
    {| Downset.has w :=
         ∃ s t , Downset.has σ s ∧ Downset.has τ t ∧ comp_has p s t w |}.

  Global Instance compose_deterministic {i j k} p σ τ :
    Deterministic σ →
    Deterministic τ →
    Deterministic (@compose_when i j k p σ τ).

Properties of compose vs. next

  Lemma compose_next_oq q σ τ :
    compose_when (cpos_left q) (next (oq q) σ) τ =
    next (oq q) (compose_when cpos_ready σ τ).

  Lemma compose_next_lq {q} m σ τ :
    compose_when (cpos_right q m) (next (pq m) σ) (next (oq m) τ) [=
    compose_when (cpos_left q) σ τ.

  Lemma compose_next_rq {q m} u σ τ :
    compose_when (cpos_suspended q m u) σ (next (pq u) τ) [=
    next (pq u) (compose_when (cpos_right q m) σ τ).

  Lemma compose_next_oa {q m u} v σ τ :
    compose_when (cpos_right q m) σ (next (oa v) τ) =
    next (oa v) (compose_when (cpos_suspended q m u) σ τ).

  Lemma compose_next_ra {q m} n σ τ :
    compose_when (cpos_left q) (next (oa n) σ) (next (pa n) τ) [=
    compose_when (cpos_right q m) σ τ.

  Lemma compose_next_la {q} r σ τ :
    compose_when cpos_ready (next (pa r) σ) τ [=
    next (pa r) (compose_when (cpos_left q) σ τ).
End COMPOSE.

Notation compose := (compose_when cpos_ready).
Infix "⊙" := compose (at level 45, right associativity) : strat_scope.

Theorem 3.5 (Properties of Layered Composition)

Section COMPOSE_ID.
Context {E F : esig}.

Hint Constructors emor_has comp_has : core.

When the identity is composed on the left, it passes through incoming interactions unchanged.

  Definition id_pos_l (i : @position E F) : @position F F :=
    match i with
      | ready ⇒ ready
      | running q ⇒ suspended q (operator (eid q))
      | suspended q m ⇒ suspended q (operator (eid q))
    end.

  Definition id_idpos_l i : epos eid (id_pos_l i) :=
    match i with
      | ready ⇒ eready
      | running q ⇒ esuspended q
      | suspended q m ⇒ esuspended q
    end.

  Definition id_cpos_l i : cpos (id_pos_l i) i i :=
    match i with
      | ready ⇒ cpos_ready
      | running q ⇒ cpos_right q q
      | suspended q m ⇒ cpos_suspended q q m
    end.

  Lemma compose_id_has_l_gt {i} (s : @play E F i) :
    ∃ t , emor_has eid (id_idpos_l i) t ∧ comp_has (id_cpos_l i) t s s.

  Lemma compose_id_has_l_lt {i} (s s': @play E F i) (t: @play F F (id_pos_l i)):
    emor_has eid (id_idpos_l i) t →
    comp_has (id_cpos_l i) t s s' →
    s' [= s.

  Lemma compose_id_l_when i (σ : strat E F i) :
    compose_when (id_cpos_l i) (emor_when eid (id_idpos_l i)) σ = σ.

  Lemma compose_id_l (σ : E ->> F) :
    id F ⊙ σ = σ.

Likewise, when the identity is composed on the right, it passes through outgoing interactions unchanged.

  Definition id_pos_r (i : @position E F) : @position E E :=
    match i with
      | ready ⇒ ready
      | running q ⇒ ready
      | suspended q m ⇒ suspended m (operator (eid m))
    end.

  Definition id_idpos_r i : epos eid (id_pos_r i) :=
    match i with
      | ready ⇒ eready
      | running q ⇒ eready
      | suspended q m ⇒ esuspended m
    end.

  Definition id_cpos_r i : cpos i (id_pos_r i) i :=
    match i with
      | ready ⇒ cpos_ready
      | running q ⇒ cpos_left q
      | suspended q m ⇒ cpos_suspended q m m
    end.

  Lemma compose_id_has_r_gt {i} (s : @play E F i) :
    ∃ t , emor_has eid (id_idpos_r i) t ∧ comp_has (id_cpos_r i) s t s.

  Lemma compose_id_has_r_lt {i} (s s': @play E F i) (t: @play E E (id_pos_r i)):
    emor_has eid (id_idpos_r i) t →
    comp_has (id_cpos_r i) s t s' →
    s' [= s.

  Lemma compose_id_r_when i (σ : strat E F i) :
    compose_when (id_cpos_r i) σ (emor_when eid (id_idpos_r i)) = σ.

  Lemma compose_id_r (σ : E ->> F) :
    σ ⊙ id E = σ.
End COMPOSE_ID.

Section COMPOSE_COMPOSE.
  Context {E F G H : esig}.

  Variant ccpos :
    ∀ {i σ i τ i υ i στ i τυ i στυ}, @cpos F G H i σ i τ i στ →
                                    @cpos E F G i τ i υ i τυ →
                                    @cpos E G H i σ i τυ i στυ →
                                    @cpos E F H i στ i υ i στυ → Type :=
    | ccpos_ready :
        ccpos cpos_ready
              cpos_ready
              cpos_ready
              cpos_ready
    | ccpos_left q1 :
        ccpos (cpos_left q1)
              cpos_ready
              (cpos_left q1)
              (cpos_left q1)
    | ccpos_mid q1 q2 :
        ccpos (cpos_right q1 q2)
              (cpos_left q2)
              (cpos_right q1 q2)
              (cpos_left q1)
    | ccpos_right q1 q2 q3 :
        ccpos (cpos_suspended q1 q2 q3)
              (cpos_right q2 q3)
              (cpos_right q1 q2)
              (cpos_right q1 q3)
    | ccpos_suspended q1 q2 q3 q4 :
        ccpos (cpos_suspended q1 q2 q3)
              (cpos_suspended q2 q3 q4)
              (cpos_suspended q1 q2 q4)
              (cpos_suspended q1 q3 q4).

  Hint Constructors pref comp_has : core.

  Ltac destruct_comp_has :=
    repeat
      match goal with
      | H : comp_has _ (_ _) _ _ |- _ ⇒ dependent destruction H
      | H : comp_has _ _ (_ _) _ |- _ ⇒ dependent destruction H
      | H : comp_has _ _ _ (_ _) |- _ ⇒ dependent destruction H
      | p : ccpos _ _ _ _ |- _ ⇒ dependent destruction p
      end.

  Lemma comp_has_assoc_1 {i σ i τ i υ i στ i τυ i στυ p στ p τυ p σ _τυ p στ _υ} :
    @ccpos i σ i τ i υ i στ i τυ i στυ p στ p τυ p σ _τυ p στ _υ →
    ∀ s t st u stu,
      comp_has p στ s t st →
      comp_has p στ _υ st u stu →
      ∃ s' t' u' tu ,
        s' [= s ∧ t' [= t ∧ u' [= u ∧
        comp_has p τυ t' u' tu ∧
        comp_has p σ _τυ s' tu stu.

  Lemma comp_has_assoc_2 {i σ i τ i υ i στ i τυ i στυ p στ p τυ p σ _τυ p στ _υ} :
    @ccpos i σ i τ i υ i στ i τυ i στυ p στ p τυ p σ _τυ p στ _υ →
    ∀ s t u tu stu,
      comp_has p τυ t u tu →
      comp_has p σ _τυ s tu stu →
      ∃ s' t' u' st ,
        s' [= s ∧ t' [= t ∧ u' [= u ∧
        comp_has p στ s' t' st ∧
        comp_has p στ _υ st u' stu.

  Lemma compose_assoc_when {i σ i τ i υ i στ i τυ i στυ p στ p τυ p σ _τυ p στ _υ} :
    @ccpos i σ i τ i υ i στ i τυ i στυ p στ p τυ p σ _τυ p στ _υ →
    ∀ σ τ υ,
      compose_when p στ _υ (compose_when p στ σ τ) υ =
      compose_when p σ _τυ σ (compose_when p τυ τ υ).

  Lemma compose_assoc (σ : G ->> H) (τ : F ->> G) (υ : E ->> F) :
    (σ ⊙ τ ) ⊙ υ = σ ⊙ τ ⊙ υ.
End COMPOSE_COMPOSE.

Isomorphisms

Class Retraction {E F} (f : E ->> F) (g : F ->> E) :=
  {
    retraction : f ⊙ g = id F;
  }.

Arguments retraction {E F} f {g _}.

Class Isomorphism {E F} (f : E ->> F) (g : F ->> E) :=
  {
    iso_fw :> Retraction f g;
    iso_bw :> Retraction g f;
  }.

Lemma retract {E F G} `{Hfg : Retraction F G} (σ : strat E G ready) :
  f ⊙ g ⊙ σ = σ.

Functoriality of emor_strat

Section ESTRAT_COMPOSE.
  Context {E F G} (g : emor F G) (f : emor E F).

  Variant cepos :
    ∀ {i j k}, @epos F G g i → @epos E F f j → @epos E G (ecomp g f) k →
                    @cpos E F G i j k → Type :=
    | cepos_ready :
        cepos eready
              eready
              eready
              cpos_ready
    | cepos_suspended q :
        cepos (esuspended q)
              (esuspended (operator (g q)))
              (esuspended q)
              (cpos_suspended _ _ _).

  Hint Constructors emor_has comp_has.

  Lemma estrat_ecomp_when {i j k pi pj pk pc} (p : @cepos i j k pi pj pk pc) :
    emor_when (ecomp g f) pk =
    compose_when pc (emor_when g pi) (emor_when f pj).

  Lemma emor_strat_ecomp :
    emor_strat (ecomp g f) = compose (emor_strat g) (emor_strat f).
End ESTRAT_COMPOSE.

§3.3 Flat Composition

Definition 3.6 (Flat composition of strategies)

Embedding signature homomorphisms preserves flat composition

Section ESTRAT_FCOMP.
  Context {E1 E2 F1 F2} (f1 : emor E1 F1) (f2 : emor E2 F2).

  Hint Constructors emor_has fcomp_has.

  Lemma emor_strat_fcomp_when {i1 i2 i} p1 p2 p p' :
    @emor_when _ _ (f1 + f2) i p =
    fcomp_when p' (@emor_when E1 F1 f1 i1 p1)
                  (@emor_when E2 F2 f2 i2 p2).

  Lemma emor_strat_fcomp :
    emor_strat (f1 + f2) = emor_strat f1 + emor_strat f2.
End ESTRAT_FCOMP.

More generally, we can reuse the structural isomorphisms defined above as signature homomorphisms for strategy-level monoidal structure. From now on, we will use emor_strat implcitly.

Coercion emor_strat : emor >-> strat.

Theorem 3.7 (Properties of flat composition)

Lemma fcomp_id {E1 E2} :
  id E1 + id E2 = id (E1 + E2).

Section COMPOSE_FCOMP.
  Context {E1 E2 F1 F2 G1 G2 : esig}.

  Variant fccpos :
    ∀ {i1 i2 j1 j2 i12 j12 ij1 ij2 ij12},
      (* the left-hand side does ⊙ first then ⊕ *)
      cpos i1 j1 ij1 → cpos i2 j2 ij2 → fcpos ij1 ij2 ij12 →
      (* the right-hand side does ⊕ first then ⊙ *)
      fcpos i1 i2 i12 → fcpos j1 j2 j12 → cpos i12 j12 ij12 → Type
    :=
    | fccpos_ready :
        fccpos cpos_ready cpos_ready fcpos_ready
               fcpos_ready fcpos_ready cpos_ready
    (* running σ1 *)
    | fccpos_left_l (q1 : G1) :
        fccpos (cpos_left q1) cpos_ready (fcpos_running_l q1)
               (fcpos_running_l q1) fcpos_ready (cpos_left (inl q1))
    (* running σ2 *)
    | fccpos_left_r (q2 : G2) :
        fccpos cpos_ready (cpos_left q2) (fcpos_running_r q2)
               (fcpos_running_r q2) fcpos_ready (cpos_left (inr q2))
    (* running τ *)
    | fccpos_right_l (q1 : G1) (m1 : F1) :
        fccpos (cpos_right q1 m1) cpos_ready (fcpos_running_l q1)
               (fcpos_suspended_l q1 m1) (fcpos_running_l m1) (cpos_right (inl q1) (inl m1))
    | fccpos_right_r (q2 : G2) (m2 : F2) :
        fccpos cpos_ready (cpos_right q2 m2) (fcpos_running_r q2)
               (fcpos_suspended_r q2 m2) (fcpos_running_r m2) (cpos_right (inr q2) (inr m2))
    (* τ suspended *)
    | fccpos_suspended_l (q1 : G1) (m1 : F1) (u1 : E1) :
        fccpos (cpos_suspended q1 m1 u1) cpos_ready (fcpos_suspended_l q1 u1)
               (fcpos_suspended_l q1 m1) (fcpos_suspended_l m1 u1) (cpos_suspended (inl q1) (inl m1) (inl u1))
    | fccpos_suspended_r (q2 : G2) (m2 : F2) (u2 : E2) :
        fccpos cpos_ready (cpos_suspended q2 m2 u2) (fcpos_suspended_r q2 u2)
               (fcpos_suspended_r q2 m2) (fcpos_suspended_r m2 u2) (cpos_suspended (inr q2) (inr m2) (inr u2)).

  Hint Constructors comp_has fcomp_has pref : core.

  Lemma compose_fcomp_has {i1 i2 j1 j2 i12 j12 ij1 ij2 ij12 p1 p2 p12 qi qj qij} :
    @fccpos i1 i2 j1 j2 i12 j12 ij1 ij2 ij12 p1 p2 p12 qi qj qij →
    ∀ s1 s2 t1 t2 st1 st2 st,
      comp_has p1 s1 t1 st1 →
      comp_has p2 s2 t2 st2 →
      fcomp_has p12 st1 st2 st →
      ∃ s1' s2' t1' t2' s12 t12 ,
        s1' [= s1 ∧ s2' [= s2 ∧ t1' [= t1 ∧ t2' [= t2 ∧
        fcomp_has qi s1' s2' s12 ∧
        fcomp_has qj t1' t2' t12 ∧
        comp_has qij s12 t12 st.

  Lemma fcomp_compose_has {i1 i2 j1 j2 i12 j12 ij1 ij2 ij12 p1 p2 p12 qi qj qij} :
    @fccpos i1 i2 j1 j2 i12 j12 ij1 ij2 ij12 p1 p2 p12 qi qj qij →
    ∀ s1 s2 t1 t2 s12 t12 st,
      fcomp_has qi s1 s2 s12 →
      fcomp_has qj t1 t2 t12 →
      comp_has qij s12 t12 st →
      ∃ s1' s2' t1' t2' st1 st2 ,
        s1' [= s1 ∧ s2' [= s2 ∧ t1' [= t1 ∧ t2' [= t2 ∧
        comp_has p1 s1' t1' st1 ∧
        comp_has p2 s2' t2' st2 ∧
        fcomp_has p12 st1 st2 st.

  Lemma fcomp_compose_when {i1 i2 j1 j2 i12 j12 ij1 ij2 ij12 p1 p2 p12 qi qj qij} :
    @fccpos i1 i2 j1 j2 i12 j12 ij1 ij2 ij12 p1 p2 p12 qi qj qij →
    ∀ σ1 σ2 τ1 τ2,
      fcomp_when p12 (compose_when p1 σ1 τ1) (compose_when p2 σ2 τ2) =
      compose_when qij (fcomp_when qi σ1 σ2) (fcomp_when qj τ1 τ2).

  Lemma fcomp_compose (σ1: F1 ->>G1) (σ2: F2 ->>G2) (τ1: E1 ->>F1) (τ2: E2 ->>F2) :
    (σ1 ⊙ τ1 ) + (σ2 ⊙ τ2 ) = (σ1 + σ2 ) ⊙ (τ1 + τ2 ).
End COMPOSE_FCOMP.

Symmetric monoidal structure

Left unitor properties

Global Instance flu_iso {E} :
Isomorphism (@flu E) (@flur E).

Right unitor properties

Global Instance fru_iso {E} :
Isomorphism (@fru E) (@frur E).

Associator properties

Global Instance fassoc_iso {E F G} :
Isomorphism (@fassoc E F G) (@fassocr E F G).

Braiding is its own inverse

Global Instance fswap_iso {E F} :
Isomorphism (@fswap E F) (@fswap F E).

Duplication and projections

Global Instance ffst_fdelta {E : esig} :
Retraction (F:=E) ffst fdup.

Global Instance fsnd_fdelta {E : esig} :
Retraction (F:=E) fsnd fdup.

§4 REFINEMENT CONVENTIONS

§4.2 Refinement Conventions

Section RC.
Context {E1 E2 : esig}.
Obligation Tactic := cbn.

Definition 4.1 (Refinement convention)

  Inductive rcp :=
    | rcp_allow (m1 : op E1) (m2 : op E2)
    | rcp_forbid (m1 : op E1) (m2 : op E2) (n1 : ar m1) (n2 : ar m2)
    | rcp_cont (m1 : op E1) (m2 : op E2) (n1 : ar m1) (n2 : ar m2) (k : rcp).

  Inductive rcp_ref : relation rcp :=
    | rcp_allow_ref m1 m2 :
        rcp_ref (rcp_allow m1 m2) (rcp_allow m1 m2)
    | rcp_allow_cont_ref m1 m2 n1 n2 k :
        rcp_ref (rcp_allow m1 m2) (rcp_cont m1 m2 n1 n2 k)
    | rcp_allow_forbid_ref m1 m2 n1 n2 :
        rcp_ref (rcp_allow m1 m2) (rcp_forbid m1 m2 n1 n2)
    | rcp_cont_ref m1 m2 n1 n2 k k' :
        rcp_ref k k' → rcp_ref (rcp_cont m1 m2 n1 n2 k) (rcp_cont m1 m2 n1 n2 k')
    | rcp_cont_forbid_ref m1 m2 n1 n2 k :
        rcp_ref (rcp_cont m1 m2 n1 n2 k) (rcp_forbid m1 m2 n1 n2)
    | rcp_forbid_ref m1 m2 n1 n2 :
        rcp_ref (rcp_forbid m1 m2 n1 n2) (rcp_forbid m1 m2 n1 n2).

  Program Canonical Structure rcp_poset : poset :=
    {|
      poset_carrier := rcp;
      ref := rcp_ref;
    |}.

  Definition conv :=
    poset_carrier (downset rcp_poset).

Residual

Program Definition rcnext q1 q2 r1 r2 (R : conv) : conv :=
{| Downset.has w := Downset.has R (rcp_cont q1 q2 r1 r2 w) |}.

Miscellaneous useful things

  Hint Constructors rcp_ref : core.

  Global Instance rcnext_ref :
    Monotonic rcnext (forallr -, forallr -, - ==> - ==> ref ++> ref).

The following auto hints facilitate the use of downward closure.

  Lemma conv_has_cont_allow q1 q2 r1 r2 k R :
    Downset.has R (rcp_cont q1 q2 r1 r2 k) →
    Downset.has R (rcp_allow q1 q2).

  Lemma conv_has_forbid_allow q1 q2 r1 r2 R :
    Downset.has R (rcp_forbid q1 q2 r1 r2) →
    Downset.has R (rcp_allow q1 q2).

  Lemma conv_has_forbid_cont q1 q2 r1 r2 k R :
    Downset.has R (rcp_forbid q1 q2 r1 r2) →
    Downset.has R (rcp_cont q1 q2 r1 r2 k).

rcnext not only trivially preserves sups and infs, but the fact that it is only sensitive to part of the refinement convention allows us to formulate these stronger properties.

  Lemma rcnext_inf {I} m1 m2 n1 n2 (R : I → conv) :
    rcnext m1 m2 n1 n2 (linf R) =
    inf {i | ¬ Downset.has (R i) (rcp_forbid m1 m2 n1 n2)}, rcnext m1 m2 n1 n2 (R i).

  Lemma rcnext_sup {I} m1 m2 n1 n2 (R : I → conv) :
    rcnext m1 m2 n1 n2 (lsup R) =
    sup {i | Downset.has (R i) (rcp_allow m1 m2)}, rcnext m1 m2 n1 n2 (R i).
End RC.

Arguments rcp : clear implicits.
Arguments rcp_poset : clear implicits.
Arguments conv : clear implicits.
Global Instance rcnext_params : Params (@rcnext) 5 := { }.

Global Hint Immediate
  conv_has_cont_allow
  conv_has_forbid_allow
  conv_has_forbid_cont : core.

Infix "<=>" := conv (at level 99, right associativity).

Declare Scope conv_scope.
Delimit Scope conv_scope with conv.
Bind Scope conv_scope with conv.
Open Scope conv_scope.

§4.3 Refinement Squares

Section RSQ.
Context {E1 E2 F1 F2 : esig}.

Definition 4.2 (Refinement square)

  Variant rspos : @position E1 F1 → @position E2 F2 → Type :=
    | rs_ready : rspos ready ready
    | rs_running q1 q2 : rspos (running q1) (running q2)
    | rs_suspended q1 q2 m1 m2 : rspos (suspended q1 m1) (suspended q2 m2).

  Inductive rsp (R S : conv _ _) :
    ∀ {i1 i2}, rspos i1 i2 → @play E1 F1 i1 → strat E2 F2 i2 → Prop :=
    | rsp_ready τ :
        Downset.has τ pnil_ready →
        rsp R S rs_ready pnil_ready τ
    | rsp_oq q1 s τ :
        Downset.has τ pnil_ready →
        (∀ q2, Downset.has S (rcp_allow q1 q2) →
                    rsp R S (rs_running q1 q2) s (next (oq q2) τ)) →
        rsp R S rs_ready (oq q1 :: s) τ
    | rsp_pq q1 q2 m1 m2 s τ :
        Downset.has R (rcp_allow m1 m2) →
        rsp R S (rs_suspended q1 q2 m1 m2) s (next (pq m2) τ) →
        rsp R S (rs_running q1 q2) (pq m1 :: s) τ
    | rsp_suspended q1 q2 m1 m2 τ :
        Downset.has τ (pnil_suspended q2 m2) →
        rsp R S (rs_suspended q1 q2 m1 m2) (pnil_suspended q1 m1) τ
    | rsp_oa q1 q2 m1 m2 n1 s τ :
        Downset.has τ (pnil_suspended q2 m2) →
        (∀ n2,
          ¬ Downset.has R (rcp_forbid m1 m2 n1 n2) →
          rsp (rcnext m1 m2 n1 n2 R) S (rs_running q1 q2) s (next (oa n2) τ)) →
        rsp R S (rs_suspended q1 q2 m1 m2) (oa n1 :: s) τ
    | rsp_pa q1 q2 r1 r2 s τ :
        ¬ Downset.has S (rcp_forbid q1 q2 r1 r2) →
        rsp R (rcnext q1 q2 r1 r2 S) rs_ready s (next (pa r2) τ) →
        rsp R S (rs_running q1 q2) (pa r1 :: s) τ.

  Definition rsq_when R S {i1 i2} p (σ : strat E1 F1 i1) (τ : strat E2 F2 i2) : Prop :=
    ∀ s, Downset.has σ s → rsp R S p s τ.

  Definition rsq R S σ τ :=
    rsq_when R S rs_ready σ τ.

Monotonicity properties

  Global Instance rsp_ref :
    Monotonic rsp (ref ++> ref --> forallr -, forallr -, - ==> ref --> ref ++> impl).

  Global Instance rsq_when_ref :
    Monotonic rsq_when
      (ref ++> ref --> forallr -, forallr -, - ==> ref --> ref ++> impl).

  Global Instance rsq_ref :
    Monotonic rsq (ref ++> ref --> ref --> ref ++> impl).

Determinism hints

  Lemma rsp_ready_inv_nil R S s τ :
    rsp R S rs_ready s τ →
    Downset.has τ pnil_ready.

  Lemma rsp_suspended_inv_nil R S q1 q2 m1 m2 s τ :
    rsp R S (rs_suspended q1 q2 m1 m2) s τ →
    Downset.has τ (pnil_suspended q2 m2).

  Hint Resolve rsp_ready_inv_nil rsp_suspended_inv_nil : determinism.

Operational behavior

  Lemma rsq_next_oq {R S σ τ} q1 q2 :
    rsq_when R S rs_ready σ τ →
    Downset.has S (rcp_allow q1 q2) →
    rsq_when R S (rs_running q1 q2) (next (oq q1) σ) (next (oq q2) τ).

  Lemma rsq_next_pq {R S q1 q2 σ τ} `{!Deterministic τ} m1 :
    rsq_when R S (rs_running q1 q2) σ τ →
    Downset.has σ (pq m1 :: pnil_suspended q1 m1) →
    ∃ m2 ,
      Downset.has R (rcp_allow m1 m2) ∧
      Downset.has τ (pq m2 :: pnil_suspended q2 m2) ∧
      rsq_when R S (rs_suspended q1 q2 m1 m2) (next (pq m1) σ) (next (pq m2) τ).

  Lemma rsq_next_oa {R S q1 q2 m1 m2 σ τ} n1 n2 :
    rsq_when R S (rs_suspended q1 q2 m1 m2) σ τ →
    ¬ Downset.has R (rcp_forbid m1 m2 n1 n2) →
    rsq_when (rcnext m1 m2 n1 n2 R) S (rs_running q1 q2) (next (oa n1) σ) (next (oa n2) τ).

  Lemma rsq_next_pa {R S q1 q2 σ τ} `{!Deterministic τ} r1 :
    rsq_when R S (rs_running q1 q2) σ τ →
    Downset.has σ (pa r1 :: pnil_ready) →
    ∃ r2 ,
      ¬ Downset.has S (rcp_forbid q1 q2 r1 r2) ∧
      Downset.has τ (pa r2 :: pnil_ready) ∧
      rsq_when R (rcnext q1 q2 r1 r2 S) rs_ready (next (pa r1) σ) (next (pa r2) τ).

Preservation of joins and meets

  Lemma rsp_sup_cases {I} {i1 i2} (p : rspos i1 i2) R (S : I → conv F1 F2) (s : play i1) (τ : strat E2 F2 i2) `{H τ : !Deterministic τ}:
    match p with
    | rs_ready ⇒ fun s τ ⇒
      inhabited I ∧
      ∀ i, rsp R (S i) p s τ
    | rs_running q1 q2
    | rs_suspended q1 q2 _ _ ⇒ fun s τ ⇒
      (∃ i , Downset.has (S i) (rcp_allow q1 q2)) ∧
      (∀ i, Downset.has (S i) (rcp_allow q1 q2) → rsp R (S i) p s τ )
    end s τ →
    rsp R (lsup S) p s τ.

  Lemma rsp_sup {I} R S s τ `{H τ : !Deterministic τ} :
    inhabited I →
    (∀ i:I, rsp R (S i) rs_ready s τ ) →
    rsp R (lsup S) rs_ready s τ.

  Lemma rsq_sup {I} R S σ τ `{H τ : !Deterministic τ} :
    inhabited I →
    (∀ i:I, rsq R (S i) σ τ ) →
    rsq R (lsup S) σ τ.

  Lemma rsp_inf {I} {i1 i2} (p : rspos i1 i2) R S s τ `{H τ : !Deterministic τ}:
    inhabited I →
    (∀ i:I, rsp (R i) S p s τ ) →
    rsp (linf R) S p s τ.
End RSQ.

Global Hint Resolve rsp_ready_inv_nil rsp_suspended_inv_nil : determinism.
Global Hint Unfold rsq.

Global Instance rsp_params : Params (@rsp) 7 := { }.
Global Instance rsq_when_params : Params (@rsq_when) 7 := { }.
Global Instance rsq_params : Params (@rsq) 4 := { }.

Declare Scope rsq_scope.
Delimit Scope rsq_scope with rsq.
Bind Scope rsq_scope with rsq.

Section RSQ_COMP.
  Context {E1 E2} (R : conv E1 E2).
  Context {F1 F2} (S : conv F1 F2).
  Context {G1 G2} (T : conv G1 G2).

Theorem 4.3 (Horizontal composition of refinement squares)

The possible combinations of positions for the source and target, left-hand side, right-hand side and composite stragies.

  Variant rscpos : ∀ {i1 j1 k1 i2 j2 k2},
    @cpos E1 F1 G1 i1 j1 k1 → @cpos E2 F2 G2 i2 j2 k2 →
    rspos i1 i2 → rspos j1 j2 → rspos k1 k2 → Type :=
    | rsc_ready :
        rscpos cpos_ready cpos_ready
               rs_ready rs_ready rs_ready
    | rsc_left q1 q2 :
        rscpos (cpos_left q1) (cpos_left q2)
               (rs_running q1 q2) rs_ready (rs_running q1 q2)
    | rsc_right q1 q2 m1 m2 :
        rscpos (cpos_right q1 m1) (cpos_right q2 m2)
               (rs_suspended q1 q2 m1 m2) (rs_running m1 m2) (rs_running q1 q2)
    | rsc_suspended q1 q2 m1 m2 u1 u2 :
        rscpos (cpos_suspended q1 m1 u1) (cpos_suspended q2 m2 u2)
               (rs_suspended q1 q2 m1 m2) (rs_suspended m1 m2 u1 u2) (rs_suspended q1 q2 u1 u2).

Having enumerated them, we can formulate the compatibility of composition with refinement squares as follows.

  Hint Constructors comp_has pref rscpos : core.

  Lemma rsp_comp {i1 j1 k1 i2 j2 k2 p1 p2 pi pj pk} :
    @rscpos i1 j1 k1 i2 j2 k2 p1 p2 pi pj pk →
    ∀ (s : @play F1 G1 i1) (t : @play E1 F1 j1)
      (σ : strat F2 G2 i2) (τ : strat E2 F2 j2) (w : @play E1 G1 k1),
      comp_has p1 s t w →
      rsp S T pi s σ →
      rsp R S pj t τ →
      rsp R T pk w (compose_when p2 σ τ).

  Lemma rsq_comp_when {i1 j1 k1 i2 j2 k2 p1 p2 pi pj pk} :
    @rscpos i1 j1 k1 i2 j2 k2 p1 p2 pi pj pk →
    ∀ (σ1 : strat F1 G1 i1) (τ1 : strat E1 F1 j1)
           (σ2 : strat F2 G2 i2) (τ2 : strat E2 F2 j2),
      rsq_when S T pi σ1 σ2 →
      rsq_when R S pj τ1 τ2 →
      rsq_when R T pk (compose_when p1 σ1 τ1) (compose_when p2 σ2 τ2).

  Lemma rsq_comp σ1 τ1 σ2 τ2:
    rsq S T σ1 σ2 →
    rsq R S τ1 τ2 →
    rsq R T (σ1 ⊙ τ1) (σ2 ⊙ τ2).
End RSQ_COMP.

Infix "⊙" := (rsq_comp _ _ _ _) : rsq_scope.

Definition 4.4 (Identity refinement convention)

Section VID.
  Context {E : esig}.

  Fixpoint vid_has (s : rcp E E) : Prop :=
    match s with
      | rcp_allow m1 m2 ⇒ m1 = m2
      | rcp_forbid m1 m2 n1 n2 ⇒ m1 = m2 ∧ ¬ JMeq n1 n2
      | rcp_cont m1 m2 n1 n2 k ⇒ m1 = m2 ∧ (JMeq n1 n2 → vid_has k)
    end.

  Program Definition vid : conv E E :=
    {| Downset.has := vid_has |}.

Properties

Lemma rcnext_vid m n :
rcnext m m n n vid = vid.
End VID.

Theorem 4.5 (Refinement ordering as refinement squares)

Section ID_RSQ.
  Context {E F : esig}.

  (*
    rsq vid vid p σ τ <-> σ = τ rsq R S p id id ↔ S [= R *)
End ID_RSQ.

§4.4 Vertical Composition

Definition 4.7 (Vertical composition of refinement conventions)

Section VCOMP.
  Context {E1 E2 E3 : esig}.
  Obligation Tactic := cbn.

  Fixpoint vcomp_has (R : conv E1 E2) (S : conv E2 E3) (s : rcp E1 E3) : Prop :=
    match s with
      | rcp_allow m1 m3 ⇒
        ∃ m2 , Downset.has R (rcp_allow m1 m2) ∧
                   Downset.has S (rcp_allow m2 m3)
      | rcp_forbid m1 m3 n1 n3 ⇒
        ∃ m2 , Downset.has R (rcp_allow m1 m2) ∧
                   Downset.has S (rcp_allow m2 m3) ∧
        ∀ n2, Downset.has R (rcp_forbid m1 m2 n1 n2) ∨
                   Downset.has S (rcp_forbid m2 m3 n2 n3)
      | rcp_cont m1 m3 n1 n3 s ⇒
        ∃ m2 , Downset.has R (rcp_allow m1 m2) ∧
                   Downset.has S (rcp_allow m2 m3) ∧
        ∀ n2, Downset.has R (rcp_forbid m1 m2 n1 n2) ∨
                   Downset.has S (rcp_forbid m2 m3 n2 n3) ∨
                   vcomp_has (rcnext m1 m2 n1 n2 R) (rcnext m2 m3 n2 n3 S) s
    end.

  Global Instance vcomp_has_ref :
    Monotonic vcomp_has (ref ++> ref ++> rcp_ref --> impl).

  Program Definition vcomp R S : conv E1 E3 :=
    {| Downset.has := vcomp_has R S |}.

The following formulation and properties of vcomp are useful for the vertical composition proof of refinement squares below.

  Definition vcomp_at_has (m2 : E2) (xn2 : option (ar m2)) R S s : Prop :=
    match s with
      | rcp_allow m1 m3 ⇒
        Downset.has R (rcp_allow m1 m2) ∧
        Downset.has S (rcp_allow m2 m3)
      | rcp_forbid m1 m3 n1 n3 ⇒
        Downset.has R (rcp_allow m1 m2) ∧
        Downset.has S (rcp_allow m2 m3) ∧
        ∀ n2, xn2 = Some n2 →
                   Downset.has R (rcp_forbid m1 m2 n1 n2) ∨
                   Downset.has S (rcp_forbid m2 m3 n2 n3)
      | rcp_cont m1 m3 n1 n3 k ⇒
        Downset.has R (rcp_allow m1 m2) ∧
        Downset.has S (rcp_allow m2 m3) ∧
        ∀ n2, xn2 = Some n2 →
                   Downset.has R (rcp_forbid m1 m2 n1 n2) ∨
                   Downset.has S (rcp_forbid m2 m3 n2 n3) ∨
                   Downset.has (vcomp (rcnext m1 m2 n1 n2 R) (rcnext m2 m3 n2 n3 S)) k
    end.

  Program Definition vcomp_at m2 n2 R S : conv E1 E3 :=
    {| Downset.has := vcomp_at_has m2 n2 R S |}.

  Lemma vcomp_expand R S :
    vcomp R S = sup m2 , inf xn2 , vcomp_at m2 xn2 R S.

  Lemma rcnext_vcomp_at m1 m2 m3 n1 n2 n3 R S :
    ¬ Downset.has R (rcp_forbid m1 m2 n1 n2) →
    ¬ Downset.has S (rcp_forbid m2 m3 n2 n3) →
    rcnext m1 m3 n1 n3 (vcomp_at m2 (Some n2) R S) =
    vcomp (rcnext m1 m2 n1 n2 R) (rcnext m2 m3 n2 n3 S).
End VCOMP.

Notation "R ;; S" := (vcomp R S) (at level 45, right associativity) : conv_scope.

Theorem 4.8 (Vertical composition of refinement squares)

Section RSVCOMP.
  Context {E1 F1 E2 F2 E3 F3 : esig}.

  Variant rsvpos : ∀ {p1 p2 p3}, @rspos E1 E2 F1 F2 p1 p2 →
                                      @rspos E2 E3 F2 F3 p2 p3 →
                                      @rspos E1 E3 F1 F3 p1 p3 → Type :=
    | rsv_ready :
        rsvpos rs_ready
               rs_ready
               rs_ready
    | rsv_running q1 q2 q3 :
        rsvpos (rs_running q1 q2)
               (rs_running q2 q3)
               (rs_running q1 q3)
    | rsv_suspended q1 q2 q3 m1 m2 m3 :
        rsvpos (rs_suspended q1 q2 m1 m2)
               (rs_suspended q2 q3 m2 m3)
               (rs_suspended q1 q3 m1 m3).

  Lemma rsp_vcomp {p1 p2 p3 p12 p23 p13} (p : @rsvpos p1 p2 p3 p12 p23 p13) :
    ∀ (R : conv E1 E2) (R' : conv E2 E3) (S : conv F1 F2) (S' : conv F2 F3)
           (s1 : @play E1 F1 p1) (σ2 : strat E2 F2 p2) (σ3 : strat E3 F3 p3)
           `{H σ2 : !Deterministic σ2} `{H σ3 : !Deterministic σ3},
      rsp R S p12 s1 σ2 →
      rsq_when R' S' p23 σ2 σ3 →
      match p with
        | rsv_ready ⇒
          rsp (vcomp R R') (vcomp S S') p13 s1 σ3
        | rsv_running q1 q2 q3 ⇒
          rsp (vcomp R R') (inf r2 , vcomp_at q2 r2 S S') p13 s1 σ3
        | rsv_suspended q1 q2 q3 m1 m2 m3 ⇒
          Downset.has R (rcp_allow m1 m2) →
          Downset.has R' (rcp_allow m2 m3) →
          rsp (inf n2 , vcomp_at m2 n2 R R') (inf r2 , vcomp_at q2 r2 S S') p13 s1 σ3
      end.

  Lemma rsq_vcomp_when {p1 p2 p3 p12 p23 p13} (p : @rsvpos p1 p2 p3 p12 p23 p13) :
    ∀ (R : conv E1 E2) (R' : conv E2 E3) (S : conv F1 F2) (S' : conv F2 F3)
           (σ1 : strat E1 F1 p1) (σ2 : strat E2 F2 p2) (σ3 : strat E3 F3 p3)
           `{H σ2 : !Deterministic σ2} `{H σ3 : !Deterministic σ3},
      rsq_when R S p12 σ1 σ2 →
      rsq_when R' S' p23 σ2 σ3 →
      match p with
        | rsv_ready ⇒
          rsq_when (vcomp R R') (vcomp S S') p13 σ1 σ3
        | rsv_running q1 q2 q3 ⇒
          rsq_when (vcomp R R') (inf r2 , vcomp_at q2 r2 S S') p13 σ1 σ3
        | rsv_suspended q1 q2 q3 m1 m2 m3 ⇒
          Downset.has R (rcp_allow m1 m2) →
          Downset.has R' (rcp_allow m2 m3) →
          rsq_when (inf n2 , vcomp_at m2 n2 R R') (inf r2 , vcomp_at q2 r2 S S') p13 σ1 σ3
      end.

  Lemma rsq_vcomp R R' S S' (σ1 : E1 ->> F1) (σ2 : E2 ->> F2) (σ3 : E3 ->> F3)
        `{H σ2 : !Deterministic σ2} `{H σ3 : !Deterministic σ3} :
    rsq R S σ1 σ2 →
    rsq R' S' σ2 σ3 →
    rsq (R ;; R') (S ;; S') σ1 σ3.
End RSVCOMP.

Infix ";;" := (rsq_vcomp _ _ _ _) : rsq_scope.

Other properties of vertical composition

Section VCOMP_VID.
  Context {E F : esig}.

  Lemma vcomp_vid_l (R : conv E F) :
    vcomp vid R = R.

  Lemma vcomp_vid_r (R : conv E F) :
    vcomp R vid = R.
End VCOMP_VID.

NB: One major flaw in the approach to refinement conventions given above is that vcomp is not associative. Specifically, the two ways to order the composition of three conventions yield answer relations that differ in their interleaving of the choices of the two intermediate questions and the two intermediate answers. Below we provide a counter-example to associativity to establish this fact.

An alternative to the formulation above would be to use Kripe worlds, as we have done in previous work. This allows us to force an earlier and permanent choice of intermediate question that persists once we get to comparing answers. Without the world we must re-quantify over intermediate questions when comparing answers, which is the source of the problem we get. It is quite remarkable that all other properties work despite this behavior of refinement conventions.

Module VCOMP_NOT_ASSOC.
  Definition one := {| op := unit; ar _ := unit |}.
  Definition twoa := {| op := unit; ar _ := bool |}.
  Definition twoq := {| op := bool; ar _ := unit |}.

  Definition toprc_has {E F} (s : rcp E F) : Prop :=
    match s with
      rcp_allow _ _ ⇒ True | _ ⇒ False
    end.

  Variant foo_has : rcp twoa twoq → Prop :=
    | foo_q (q : bool) :
      foo_has (@rcp_allow twoa twoq tt q)
    | foo_r (q r : bool) :
      q ≠ r → foo_has (@rcp_forbid twoa twoq tt q r tt)
    | foo_cont (q r : bool) k :
      q ≠ r → foo_has (@rcp_cont twoa twoq tt q r tt k).

  Hint Constructors foo_has : core.

  Program Definition R : one <=> twoa :=
    {| Downset.has := toprc_has |}.

  Program Definition foo : twoa <=> twoq :=
    {| Downset.has := foo_has |}.

  Program Definition S : twoq <=> one :=
    {| Downset.has := toprc_has |}.

  Lemma vcomp_not_assoc :
    (R ;; foo ) ;; S ≠ R ;; (foo ;; S ).
End VCOMP_NOT_ASSOC.

Signature homomorphisms

Signature homomorphisms embed into refinement conventions as well as strategies. This will again be useful to define the monoidal structure associated with flat composition for refinement conventions.

Section EMOR_RC.
Context {E1 E2} (f : emor E1 E2).
Obligation Tactic := cbn.

Definition

  Inductive emor_rc_has : rcp E1 E2 → Prop :=
    | emor_rc_allow m :
        emor_rc_has (rcp_allow (operator (f m)) m)
    | emor_rc_forbid m n1 n2 :
        operand (f m) n1 ≠ n2 →
        emor_rc_has (rcp_forbid (operator (f m)) m n1 n2)
    | emor_rc_cont m n1 n2 k :
        (operand (f m) n1 = n2 → emor_rc_has k ) →
        emor_rc_has (rcp_cont (operator (f m)) m n1 n2 k).

  Hint Constructors emor_rc_has.

  Program Definition emor_rc : conv E1 E2 :=
    {| Downset.has := emor_rc_has |}.

Useful lemmas

Behavior wrt rcnext

Lemma rcnext_emor q r :
rcnext (operator (f q)) q r (operand (f q) r) emor_rc = emor_rc.

The resulting refinement convention is in fact a companion of the embedded strategy (see §5.5).

  Hint Constructors rsp emor_has : core.
  Hint Unfold Downset.has : core.

  Variant esepos : ∀ {i j}, epos f i → epos eid j → rspos i j → Type :=
    | ese_ready :
        esepos eready eready rs_ready
    | ese_suspended (q : E2) :
        esepos (esuspended q) (esuspended q)
               (rs_suspended q q (operator (f q)) q).

  Lemma emor_strat_elim_when {i j pi pj pij} (p : @esepos i j pi pj pij) :
    rsq_when emor_rc vid pij (emor_when f pi) (emor_when eid pj).

  Lemma emor_strat_elim :
    rsq emor_rc vid f (id _).

  Variant esipos : ∀ {i j}, epos eid i → epos f j → rspos i j → Type :=
    | esi_ready :
        esipos eready eready rs_ready
    | esi_suspended (q : E2) :
        esipos (esuspended (operator (f q))) (esuspended q)
               (rs_suspended (operator (f q)) q (operator (f q)) (operator (f q))).

  Lemma emor_strat_intro_when {i j pi pj pij} (p : @esipos i j pi pj pij) :
    rsq_when vid emor_rc pij (emor_when (@eid E1) pi) (emor_when f pj).

  Lemma emor_strat_intro :
    rsq vid emor_rc (id _) f.
End EMOR_RC.

Functoriality

Lemma emor_rc_id {E} :
emor_rc (@eid E) = vid.

Lemma emor_rc_ecomp {E F G} (g : emor F G) (f : emor E F) :
emor_rc (g ∘ f) = vcomp (emor_rc f) (emor_rc g).

§4.5 Flat Composition

Definition 4.10 (Flat composition of refinement conventions)

Section FCOMP_RC.
  Context {E1 E2 F1 F2 : esig}.
  Obligation Tactic := cbn.

  Fixpoint fcomp_rc_has (R S : conv _ _) (s: rcp (E1 + F1) (E2 + F2)) : Prop :=
    match s with
      | rcp_allow (inl q1) (inl q2) ⇒ Downset.has R (rcp_allow q1 q2)
      | rcp_allow (inr q1) (inr q2) ⇒ Downset.has S (rcp_allow q1 q2)
      | rcp_allow _ _ ⇒ False
      | rcp_forbid (inl q1) (inl q2) r1 r2 ⇒ Downset.has R (rcp_forbid q1 q2 r1 r2)
      | rcp_forbid (inr q1) (inr q2) r1 r2 ⇒ Downset.has S (rcp_forbid q1 q2 r1 r2)
      | rcp_forbid _ _ _ _ ⇒ False
      | rcp_cont (inl q1) (inl q2) r1 r2 k ⇒
          Downset.has R (rcp_forbid q1 q2 r1 r2) ∨
          Downset.has R (rcp_allow q1 q2) ∧ fcomp_rc_has (rcnext q1 q2 r1 r2 R) S k
      | rcp_cont (inr q1) (inr q2) r1 r2 k ⇒
          Downset.has S (rcp_forbid q1 q2 r1 r2) ∨
          Downset.has S (rcp_allow q1 q2) ∧ fcomp_rc_has R (rcnext q1 q2 r1 r2 S) k
      | rcp_cont _ _ _ _ _ ⇒ False
    end.

  Program Definition fcomp_rc R S : conv (E1 + F1) (E2 + F2) :=
    {| Downset.has := fcomp_rc_has R S |}.

  Lemma rcnext_fcomp_l q1 q2 r1 r2 R S :
    Downset.has R (rcp_allow q1 q2) →
    ¬ Downset.has R (rcp_forbid q1 q2 r1 r2) →
    rcnext (inl q1) (inl q2) r1 r2 (fcomp_rc R S) = fcomp_rc (rcnext q1 q2 r1 r2 R) S.

  Lemma rcnext_fcomp_r q1 q2 r1 r2 R S :
    Downset.has S (rcp_allow q1 q2) →
    ¬ Downset.has S (rcp_forbid q1 q2 r1 r2) →
    rcnext (inr q1) (inr q2) r1 r2 (fcomp_rc R S) = fcomp_rc R (rcnext q1 q2 r1 r2 S).

  Lemma fcomp_sup_l {I} (R : I → _) S :
    inhabited I →
    fcomp_rc (lsup R) S = sup i , fcomp_rc (R i) S.

  Lemma fcomp_sup_r {I} R (S : I → _) :
    inhabited I →
    fcomp_rc R (lsup S) = sup i , fcomp_rc R (S i).

  Lemma fcomp_inf_l {I} (R : I → _) S :
    inhabited I →
    fcomp_rc (linf R) S = inf i , fcomp_rc (R i) S.

  Lemma fcomp_inf_r {I} R (S : I → _) :
    inhabited I →
    fcomp_rc R (linf S) = inf i , fcomp_rc R (S i).
End FCOMP_RC.

Infix "+" := fcomp_rc : conv_scope.

Theorem 4.11 (Flat composition properties)

Functoriality of ⊕

Section FCOMP_VID.
  Context {E F : esig}.

  Lemma fcomp_vid :
    (@vid E ) + (@vid F ) = @vid (E + F).
End FCOMP_VID.

Section FCOMP_VCOMP.
  Context {E1 E2 F1 F2 G1 G2 : esig}.

  Lemma fcomp_vcomp (R1: conv E1 F1) (R2: conv E2 F2) (S1: conv F1 G1) (S2: conv F2 G2):
    (R1 ;; S1 ) + (R2 ;; S2 ) = (R1 + R2 ) ;; (S1 + S2 ).
End FCOMP_VCOMP.

Flat composition of refinement squares

Section FCOMP_RSQ.
  Context {E1 E2 F1 F2 E1' E2' F1' F2' : esig}.

  Variant fcrspos : ∀ {i1 i2 i j1 j2 j}, rspos i1 j1 → rspos i2 j2 →
                                              fcpos i1 i2 i → fcpos j1 j2 j →
                                              rspos i j → Type :=
    | fcrs_ready :
        fcrspos rs_ready rs_ready fcpos_ready fcpos_ready rs_ready
    | fcrs_running_l (q1 : F1) (q2 : F1') :
        fcrspos (rs_running q1 q2) rs_ready
                (fcpos_running_l q1) (fcpos_running_l q2)
                (rs_running (inl q1) (inl q2))
    | fcrs_running_r (q1 : F2) (q2 : F2') :
        fcrspos rs_ready (rs_running q1 q2)
                (fcpos_running_r q1) (fcpos_running_r q2)
                (rs_running (inr q1) (inr q2))
    | fcrs_suspended_l (q1 : F1) (q2 : F1') (m1 : E1) (m2 : E1') :
        fcrspos (rs_suspended q1 q2 m1 m2) rs_ready
                (fcpos_suspended_l q1 m1) (fcpos_suspended_l q2 m2)
                (rs_suspended (inl q1) (inl q2) (inl m1) (inl m2))
    | fcrs_suspended_r (q1 : F2) (q2 : F2') (m1 : E2) (m2 : E2') :
        fcrspos rs_ready (rs_suspended q1 q2 m1 m2)
                (fcpos_suspended_r q1 m1) (fcpos_suspended_r q2 m2)
                (rs_suspended (inr q1) (inr q2) (inr m1) (inr m2)).

  Hint Constructors rsp fcomp_has fcrspos.

  Lemma fcomp_rsp {i1 i2 i j1 j2 j p1 p2 pi pj pij} :
    ∀ p : @fcrspos i1 i2 i j1 j2 j p1 p2 pi pj pij,
    ∀ R1 S1 s1 τ1, rsp R1 S1 p1 s1 τ1 →
    ∀ R2 S2 s2 τ2, rsp R2 S2 p2 s2 τ2 →
    ∀ s, fcomp_has pi s1 s2 s →
    match p with
      | fcrs_running_l q1 q2 ⇒
          Downset.has S1 (rcp_allow q1 q2)
      | fcrs_running_r q1 q2 ⇒
          Downset.has S2 (rcp_allow q1 q2)
      | fcrs_suspended_l q1 q2 m1 m2 ⇒
          Downset.has S1 (rcp_allow q1 q2) ∧
          Downset.has R1 (rcp_allow m1 m2)
      | fcrs_suspended_r q1 q2 m1 m2 ⇒
          Downset.has S2 (rcp_allow q1 q2) ∧
          Downset.has R2 (rcp_allow m1 m2)
      | _ ⇒ True
    end →
    rsp (R1 + R2) (S1 + S2) pij s (fcomp_when pj τ1 τ2).

  Lemma fcomp_rsq :
    ∀ (R1 : conv E1 E1') (S1 : conv F1 F1') (σ1 : E1 ->> F1) (τ1 : E1' ->> F1')
           (R2 : conv E2 E2') (S2 : conv F2 F2') (σ2 : E2 ->> F2) (τ2 : E2' ->> F2'),
      rsq R1 S1 σ1 τ1 →
      rsq R2 S2 σ2 τ2 →
      rsq (R1 + R2) (S1 + S2) (σ1 + σ2)%strat (τ1 + τ2)%strat.
End FCOMP_RSQ.

Infix "+" := (fcomp_rsq _ _ _ _ _ _ _ _) : rsq_scope.

Monoidal structure

Again we can lift the structural isomorphisms we used for signature homomorphisms.

Coercion emor_rc : emor >-> conv.

§5 SPATIAL COMPOSITION

§5.1 Explicit State

Tensor product of effect signatures

As with flat composition, we only formalize the nullary and binary cases. The unit is a special case of {u : U | u ∈ U}, defined below.

Definition glob U : esig :=
  {|
    op := U;
    ar _ := U;
  |}.

Notation "1" := (glob unit) : esig_scope.

The binary tensor product is defined as follows.

Canonical Structure tens E1 E2 :=
  {|
    op := op E1 × op E2;
    ar m := ar (fst m) × ar (snd m);
  |}%type.

Infix "×" := tens : esig_scope.

Tensor product of signature homomorphisms

As with flat composition, we first define the monoidal structure in the simpler setting of signature homomorphisms.

Section TENS_EMOR.
  Context {E1 E2 F1 F2} (f1 : emor E1 F1) (f2 : emor E2 F2).

  Definition tens_emor : emor (E1 × E2) (F1 × F2) :=
    fun q ⇒ econs (operator (f1 (fst q)),
                    operator (f2 (snd q)))
                   (fun r ⇒ (operand (f1 (fst q)) (fst r),
                              operand (f2 (snd q)) (snd r))).
End TENS_EMOR.

Infix "×" := tens_emor : emor_scope.

Functoriality

Lemma tens_eid {E F} :
  @eid E × @eid F = @eid (E × F).

Lemma tens_compose {E1 E2 F1 F2 G1 G2} :
  ∀ (g1 : emor F1 G1) (g2 : emor F2 G2) (f1 : emor E1 F1) (f2 : emor E2 F2),
    (g1 ∘ f1 ) × (g2 ∘ f2 ) = (g1 × g2 ) ∘ (f1 × f2 ).

Left unitor

Definition tlu {E} : emor (1 × E) E :=
  fun q ⇒ econs (E := 1 × E) (tt , q ) (fun r ⇒ snd r).

Definition tlur {E} : emor E (1 × E) :=
  fun q ⇒ econs (snd q) (fun r ⇒ (tt , r )).

Lemma tlur_tlu {E} :
  @tlur E ∘ @tlu E = eid.

Lemma tlu_tlur {E} :
  @tlu E ∘ @tlur E = eid.

Right unitor

Definition tru {E} : emor (E × 1) E :=
  fun q ⇒ econs (E := E × 1) (q , tt ) (fun r ⇒ fst r).

Definition trur {E} : emor E (E × 1) :=
  fun q ⇒ econs (fst q) (fun r ⇒ (r , tt )).

Lemma trur_tru {E} :
  @trur E ∘ @tru E = eid.

Lemma tru_trur {E} :
  @tru E ∘ @trur E = eid.

Associator

Definition tassoc {E F G} : emor ((E × F ) × G) (E × (F × G )) :=
  fun q ⇒ econs ((fst q , fst (snd q)), snd (snd q))
                 (fun r ⇒ (fst (fst r), (snd (fst r), snd r ))).

Definition tassocr {E F G} : emor (E × (F × G )) ((E × F ) × G) :=
  fun q ⇒ econs (fst (fst q), (snd (fst q), snd q ))
                 (fun r ⇒ ((fst r , fst (snd r)), snd (snd r))).

Lemma tassocr_tassoc {E F G} :
  @tassocr E F G ∘ @tassoc E F G = eid.

Lemma tassoc_tassocr {E F G} :
  @tassoc E F G ∘ @tassocr E F G = eid.

Braiding

Definition tswap {E F} : emor (tens E F) (tens F E) :=
fun q ⇒ econs (snd q , fst q ) (fun r ⇒ (snd r , fst r )).

Lemma tswap_tswap {E F} :
@tswap E F ∘ @tswap F E = eid.

Coherence diagrams

Triangle diagram

Lemma tlu_tassoc {E F} :
(@eid E × @tlu F ) ∘ @tassoc E 1 F = @tru E × @eid F.

Pentagon diagram

Lemma tassoc_tassoc {E F G H} :
@tassoc E F (G × H) ∘ @tassoc (E × F) G H =
(@eid E × @tassoc F G H ) ∘ @tassoc E (F × G) H ∘ (@tassoc E F G × @eid H ).

Unit coherence for braiding

Lemma tlu_tswap {E} :
@tlu E ∘ @tswap E 1 = @tru E.

Hexagon

Lemma tassoc_tswap {E F G} :
@tassoc F G E ∘ @tswap E (F × G) ∘ @tassoc E F G =
(@eid F × @tswap E G ) ∘ @tassoc F E G ∘ (@tswap E F × @eid G ).

Tensor product of strategies

We can define a form of tensor product for strategies, however note that it is not well-behaved in general. In partcular, if running strategies conflict on whether an outgoing question or top-level answer should come next, the result will be undefined. One consequence of that the composite (σ1 ⊙ τ1) ⊗ (σ2 ⊙ τ2) may synchronize even as the components (σ1 ⊗ σ2) ⊙ (τ1 ⊗ τ2) do not, weakening functoriality.

Section TSTRAT.
  Context {E1 E2 F1 F2 : esig}.

  Variant tpos : @position E1 F1 → @position E2 F2 → @position (tens E1 E2) (tens F1 F2) → Type :=
    | tp_ready :
        tpos ready ready ready
    | tp_running q1 q2 :
        tpos (running q1) (running q2) (running (q1 ,q2 ))
    | tp_suspended q1 q2 m1 m2 :
        tpos (suspended q1 m1) (suspended q2 m2) (suspended (q1 ,q2 ) (m1 ,m2 )).

  Inductive tstrat_has : ∀ {i1 i2 i}, tpos i1 i2 i → play i1 → play i2 → play i → Prop :=
    | tstrat_has_ready :
        tstrat_has (tp_ready)
                 pnil_ready
                 pnil_ready
                 pnil_ready
    | tstrat_has_oq q1 q2 s1 s2 s :
        tstrat_has (tp_running q1 q2) s1 s2 s →
        tstrat_has (tp_ready)
                 (oq q1 :: s1)
                 (oq q2 :: s2)
                 (oq (q1 ,q2 ) :: s)
    | tstrat_has_pq q1 q2 m1 m2 s1 s2 s :
        tstrat_has (tp_suspended q1 q2 m1 m2) s1 s2 s →
        tstrat_has (tp_running q1 q2)
                 (pq m1 :: s1)
                 (pq m2 :: s2)
                 (pq (m1 ,m2 ) :: s)
    | tstrat_has_suspended q1 q2 m1 m2 :
        tstrat_has (tp_suspended q1 q2 m1 m2)
                 (pnil_suspended q1 m1)
                 (pnil_suspended q2 m2)
                 (pnil_suspended (q1 ,q2 ) (m1 ,m2 ))
    | tstrat_has_oa q1 q2 m1 m2 n1 n2 s1 s2 s :
        tstrat_has (tp_running q1 q2) s1 s2 s →
        tstrat_has (tp_suspended q1 q2 m1 m2)
                 (oa n1 :: s1)
                 (oa n2 :: s2)
                 (oa (m:=(m1 ,m2 )) (n1 ,n2 ) :: s)
    | tstrat_has_pa q1 q2 r1 r2 s1 s2 s :
        tstrat_has (tp_ready) s1 s2 s →
        tstrat_has (tp_running q1 q2)
                 (pa r1 :: s1)
                 (pa r2 :: s2)
                 (pa (q:=(q1 ,q2 )) (r1 ,r2 ) :: s).

  Obligation Tactic := cbn.
  Hint Constructors pref tstrat_has : core.

  Program Definition tstrat_when {i1 i2 i} (p : tpos i1 i2 i)
    (σ1 : strat E1 F1 i1) (σ2 : strat E2 F2 i2) : strat (tens E1 E2) (tens F1 F2) i :=
      {| Downset.has s := ∃ s1 s2 , tstrat_has p s1 s2 s ∧
                                        Downset.has σ1 s1 ∧
                                        Downset.has σ2 s2 |}.

Residuals

  Lemma tstrat_next_oq q1 q2 σ1 σ2 :
    next (oq (q1 ,q2 )) (tstrat_when tp_ready σ1 σ2) =
    tstrat_when (tp_running q1 q2) (next (oq q1) σ1) (next (oq q2) σ2).

  Lemma tstrat_next_pq {q1 q2} m1 m2 σ1 σ2 :
    next (pq (m1 ,m2 )) (tstrat_when (tp_running q1 q2) σ1 σ2) =
    tstrat_when (tp_suspended q1 q2 m1 m2) (next (pq m1) σ1) (next (pq m2) σ2).

  Lemma tstrat_next_oa {q1 q2 m1 m2} n1 n2 σ1 σ2 :
    next (oa (m := (m1 ,m2 )) (n1 ,n2 )) (tstrat_when (tp_suspended q1 q2 m1 m2) σ1 σ2) =
    tstrat_when (tp_running q1 q2) (next (oa n1) σ1) (next (oa n2) σ2).

  Lemma tstrat_next_pa q1 q2 r1 r2 σ1 σ2 :
    next (pa (q := (q1 ,q2 )) (r1 ,r2 )) (tstrat_when (tp_running q1 q2) σ1 σ2) =
    tstrat_when tp_ready (next (pa r1) σ1) (next (pa r2) σ2).
End TSTRAT.

Notation tstrat := (tstrat_when tp_ready).
Infix "×" := tstrat : strat_scope.

Tensor product of refinement conventions

Section TCONV.
  Context {E1 E2 F1 F2 : esig}.

  Fixpoint tconv_has (R1 : conv E1 F1) (R2 : conv E2 F2) (s : rcp (tens E1 E2) (tens F1 F2)) :=
    match s with
      | rcp_allow (e1,e2) (f1,f2) ⇒
        Downset.has R1 (rcp_allow e1 f1) ∧
        Downset.has R2 (rcp_allow e2 f2)
      | rcp_forbid (e1,e2) (f1,f2) (n1,n2) (r1,r2) ⇒
        Downset.has R1 (rcp_allow e1 f1) ∧
        Downset.has R2 (rcp_allow e2 f2) ∧
        (Downset.has R1 (rcp_forbid e1 f1 n1 r1) ∨
         Downset.has R2 (rcp_forbid e2 f2 n2 r2))
      | rcp_cont (e1,e2) (f1,f2) (n1,n2) (r1,r2) k ⇒
        Downset.has R1 (rcp_allow e1 f1) ∧
        Downset.has R2 (rcp_allow e2 f2) ∧
        (Downset.has R1 (rcp_forbid e1 f1 n1 r1) ∨
         Downset.has R2 (rcp_forbid e2 f2 n2 r2) ∨
         tconv_has (rcnext e1 f1 n1 r1 R1) (rcnext e2 f2 n2 r2 R2) k)
    end.

  Obligation Tactic := cbn.

  Program Definition tconv R1 R2 : conv (tens E1 E2) (tens F1 F2) :=
    {| Downset.has := tconv_has R1 R2 |}.

Residuals

  Lemma rcnext_tconv m1 m2 m1' m2' n1 n2 n1' n2' R1 R2 :
    ¬ Downset.has R1 (rcp_forbid m1 m1' n1 n1') →
    ¬ Downset.has R2 (rcp_forbid m2 m2' n2 n2') →
    rcnext (m1 ,m2 ) (m1',m2') (n1 ,n2 ) (n1',n2') (tconv R1 R2) =
    tconv (rcnext m1 m1' n1 n1' R1) (rcnext m2 m2' n2 n2' R2).

Preservation of sup and inf.

  Lemma tconv_sup_l {I} R1 R2 :
    tconv (sup i:I , R1 i) R2 = sup i:I , tconv (R1 i) R2.

  Lemma tconv_sup_r {I} R1 R2 :
    tconv R1 (sup i:I , R2 i) = sup i:I , tconv R1 (R2 i).

  Lemma tconv_sup {I J} R1 R2 :
    tconv (sup i:I , R1 i) (sup j:J , R2 j) = sup i j , tconv (R1 i) (R2 j).

  Lemma tconv_inf_l {I} R1 R2 :
    inhabited I →
    tconv (inf i:I , R1 i) R2 = inf i:I , tconv (R1 i) R2.

  Lemma tconv_inf_r {I} R1 R2 :
    inhabited I →
    tconv R1 (inf i:I , R2 i) = inf i:I , tconv R1 (R2 i).
End TCONV.

Infix "×" := tconv : conv_scope.

Functoriality vs vertical composition

Section TCONV_VCOMP.
  Context {E1 F1 G1} (R1 : conv E1 F1) (S1 : conv F1 G1).
  Context {E2 F2 G2} (R2 : conv E2 F2) (S2 : conv F2 G2).

  Definition combine_ans (m1' : F1) (m2' : F2) (n1' : option (ar m1')) (n2' : option (ar m2')) :=
    match n1', n2' with
      | Some x, Some y ⇒ Some (x, y)
      | _, _ ⇒ None
    end.

  Ltac refold :=
    repeat
      match goal with
      | |- context C[vcomp_has ?R ?S ?s] ⇒
        let P := context C[Downset.has (vcomp R S) s] in change P
      | |- context C[vcomp_at_has ?m1 ?m2 ?n1 ?n2 ?R ?S ?s] ⇒
        let P := context C[Downset.has (vcomp_at m1 m2 n1 n2 R S) s] in change P
      | |- context C[tconv_has ?R ?S ?s] ⇒
        let P := context C[Downset.has (tconv R S) s] in change P
      end.

  Instance funext_rel A B :
    subrelation (- ==> eq) (@eq (A → B)).

  Instance sup_eq :
    Monotonic (@lsup) (forallr -, forallr -, (- ==> eq) ==> eq).

  Instance inf_eq :
    Monotonic (@linf) (forallr -, forallr -, (- ==> eq) ==> eq).

  Lemma tconv_vcomp_at m1' m2' n1' n2' :
    tconv (vcomp_at m1' n1' R1 S1) (vcomp_at m2' n2' R2 S2) =
    vcomp_at (m1', m2') (combine_ans m1' m2' n1' n2') (tconv R1 R2) (tconv S1 S2).

  Lemma tconv_vcomp :
    tconv (vcomp R1 S1) (vcomp R2 S2) = vcomp (tconv R1 R2) (tconv S1 S2).
End TCONV_VCOMP.

Lemma tconv_vid {E F} :
  tconv (@vid E) (@vid F) = @vid (E × F).

Tensor product of refinement squares

Section TRSQ.
  Context {E1 E2 F1 F2 E1' E2' F1' F2' : esig}.

  Variant trspos :
    ∀ {i1 i2 j1 j2 i j}, @rspos E1 E1' F1 F1' i1 j1 →
                              @rspos E2 E2' F2 F2' i2 j2 →
                              @rspos (tens E1 E2) (tens E1' E2') (tens F1 F2) (tens F1' F2') i j →
                              @tpos E1 E2 F1 F2 i1 i2 i →
                              @tpos E1' E2' F1' F2' j1 j2 j → Type :=
    | trs_ready :
        trspos rs_ready
               rs_ready
               rs_ready
               tp_ready
               tp_ready
    | trs_running q1 q2 q1' q2' :
        trspos (rs_running q1 q1')
               (rs_running q2 q2')
               (rs_running (q1 ,q2 ) (q1',q2'))
               (tp_running q1 q2)
               (tp_running q1' q2')
    | trs_suspended q1 q2 q1' q2' m1 m2 m1' m2' :
        trspos (rs_suspended q1 q1' m1 m1')
               (rs_suspended q2 q2' m2 m2')
               (rs_suspended (q1 ,q2 ) (q1',q2') (m1 ,m2 ) (m1',m2'))
               (tp_suspended q1 q2 m1 m2)
               (tp_suspended q1' q2' m1' m2').

  Hint Constructors tstrat_has : core.

  Lemma trsp :
    ∀ {i1 i2 j1 j2 i j u1 u2 u v v'} {p : @trspos i1 i2 j1 j2 i j u1 u2 u v v'}
      (R1 : conv E1 E1') (S1 : conv F1 F1') (s1 : @play E1 F1 i1) (τ1 : strat E1' F1' j1)
      (R2 : conv E2 E2') (S2 : conv F2 F2') (s2 : @play E2 F2 i2) (τ2 : strat E2' F2' j2)
      (s : @play (tens E1 E2) (tens F1 F2) i),
    rsp R1 S1 u1 s1 τ1 →
    rsp R2 S2 u2 s2 τ2 →
    tstrat_has v s1 s2 s →
    match p with
      | trs_suspended q1 q2 q1' q2' m1 m2 m1' m2' ⇒
        Downset.has R1 (rcp_allow m1 m1') →
        Downset.has R2 (rcp_allow m2 m2') →
        rsp (tconv R1 R2) (tconv S1 S2) u s (tstrat_when v' τ1 τ2)
      | _ ⇒
        rsp (tconv R1 R2) (tconv S1 S2) u s (tstrat_when v' τ1 τ2)
    end.

  Lemma trsq :
    ∀ {R1 : conv E1 E1'} {S1 : conv F1 F1'} {σ1 : E1 ->> F1} {τ1 : E1' ->> F1'}
           {R2 : conv E2 E2'} {S2 : conv F2 F2'} {σ2 : E2 ->> F2} {τ2 : E2' ->> F2'},
      rsq R1 S1 σ1 τ1 →
      rsq R2 S2 σ2 τ2 →
      rsq (R1 × R2) (S1 × S2) (σ1 × σ2) (τ1 × τ2).
End TRSQ.

Infix "×" := trsq : rsq_scope.

§5.2 Passing State Through

§5.3 Transforming State

Since the tensor product of full-blown strategies does not work in the general case, we define increasingly sophisticated notions of "passive components" to act on global state components of effect signatures. As with signature homomorphisms, this approach allows us to define and reason simple transformations more easily while retaining the expressivity required for the more sophisticated constructions.

Bijections

Record bijection {U V} :=
  {
    fw : U → V;
    bw : V → U;
    bw_fw u : bw (fw u) = u;
    fw_bw v : fw (bw v) = v;
  }.

Arguments bijection : clear implicits.

Declare Scope bijection_scope.
Delimit Scope bijection_scope with bijection.
Bind Scope bijection_scope with bijection.
Open Scope bijection_scope.

Lemma bij_eq_ext {U V} (f g : bijection U V) :
  (∀ u, fw f u = fw g u ) → f = g.

Composition

Program Definition bid {U} : bijection U U :=
  {| fw u := u;
     bw u := u |}.

Coercion bid : Sortclass >-> bijection.

Program Definition bcomp {U V W} (g : bijection V W) (f : bijection U V) :=
  {| fw u := fw g (fw f u);
     bw w := bw f (bw g w) |}.
Solve Obligations
  with cbn; intros; rewrite ?bw_fw, ?fw_bw; reflexivity.

Infix "∘" := bcomp : bijection_scope.

Lemma bcomp_bid_l {U V} (f : bijection U V) :
  bcomp bid f = f.

Lemma bcomp_bid_r {U V} (f : bijection U V) :
  bcomp f bid = f.

Lemma bcomp_bcomp {U V W X} f g h :
  @bcomp U V X (@bcomp V W X h g) f = @bcomp U W X h (@bcomp U V W g f).

Inverse

Definition inv {U V} (f : bijection U V) : bijection V U :=
  {| fw := bw f; bw := fw f; bw_fw := fw_bw f; fw_bw := bw_fw f |}.

Lemma inv_invol {U V} (f : bijection U V) :
  inv (inv f) = f.

Lemma inv_l {U V} (f : bijection U V) :
  inv f ∘ f = bid.

Lemma inv_r {U V} (f : bijection U V) :
  f ∘ inv f = bid.

Product

Program Definition prod_bij {U1 U2 V1 V2} (f1: bijection U1 V1) (f2: bijection U2 V2) :=
  {| fw u := (fw f1 (fst u), fw f2 (snd u));
     bw v := (bw f1 (fst v), bw f2 (snd v)) |}.
Solve Obligations with
  cbn; intros; rewrite ?bw_fw, ?fw_bw; auto using surjective_pairing.

Infix "×" := prod_bij : bijection_scope.

Lemma prod_bij_id {U V} :
  @bid U × @bid V = @bid (U × V).

Lemma prod_bij_bcomp {U1 U2 V1 V2 W1 W2} :
  ∀ (g1 : bijection V1 W1) (g2 : bijection V2 W2)
         (f1 : bijection U1 V1) (f2 : bijection U2 V2),
    (g1 ∘ f1 ) × (g2 ∘ f2 ) = (g1 × g2 ) ∘ (f1 × f2 ).

Left unitor

Program Definition plu {U} : bijection (unit × U) U :=
{| fw := snd; bw := pair tt |}.
Solve Obligations with
repeat (intros [[ ] ?] || intro); reflexivity.

Right unitor

Program Definition pru {U} : bijection (U × unit) U :=
{| fw := fst; bw u := (u , tt ) |}.
Solve Obligations with
repeat (intros [? [ ]] || intro); reflexivity.

Associator

Program Definition passoc {U V W} : bijection ((U × V ) × W) (U × (V × W )) :=
{| fw x := (fst (fst x), (snd (fst x), snd x ));
bw x := ((fst x , fst (snd x)), snd (snd x)) |}.

Braiding

Program Definition pswap {U V} : bijection (U × V) (V × U) :=
  {| fw uv := (snd uv , fst uv );
     bw vu := (snd vu , fst vu ) |}.

Lemma pswap_pswap {U V} :
  @pswap U V ∘ @pswap V U = bid.

Lemma inv_pswap {U V} :
  inv (@pswap U V) = @pswap V U.

Triangle diagram

Lemma plu_passoc {U V} :
(@bid U × @plu V ) ∘ @passoc U unit V = @pru U × @bid V.

Pentagon diagram

Lemma passoc_passoc {U V W X} :
@passoc U V (W × X) ∘ @passoc (U × V) W X =
(@bid U × @passoc V W X ) ∘ @passoc U (V × W) X ∘ (@passoc U V W × @bid X ).

Unit coherence for braiding

Lemma plu_pswap {U} :
@plu U ∘ @pswap U unit = @pru U.

Hexagon

Lemma passoc_pswap {U V W} :
@passoc V W U ∘ @pswap U (V × W) ∘ @passoc U V W =
(@bid V × @pswap U W ) ∘ @passoc V U W ∘ (@pswap U V × @bid W ).

Lenses

Note that in order to match the orientation of the strategies that we combine them with, our definition of lens is flipped compared with the traditional one.

Record lens {U V} :=
  {
    state : Type;
    init_state : state;
    get : state × V → U;
    set : state × V → U → state × V;
    get_set v u : get (set u v) = v;
    set_get v : set v (get v) = v;
    set_set v u u' : set (set v u) u' = set v u';
  }.

Global Arguments lens : clear implicits.
Infix "~>>" := lens (at level 99, right associativity).

Declare Scope lens_scope.
Delimit Scope lens_scope with lens.
Bind Scope lens_scope with lens.
Open Scope lens_scope.

Equivalence

Unfortunately the use of state means that equivalent lenses may not be equal, so we need to reason up to the following notion of equivalence. However, equivalent lenses will yield strategy interpretations that are equal.

Record lens_eqv {U V} (f g : U ~>> V) : Prop :=
  {
    state_eqv : rel (state f) (state g);
    init_state_eqv : state_eqv (init_state f) (init_state g);
    get_eqv : Related (get f) (get g) (state_eqv × eq ++> eq);
    set_eqv : Related (set f) (set g) (state_eqv × eq ++> - ==> state_eqv × eq);
}.

Global Instance slens_eqv_equiv {U V} :
  Equivalence (@lens_eqv U V).

Infix "==" := lens_eqv (at level 70, right associativity).

Embedding bijections

Program Definition bij_lens {U V} (f : bijection U V) : U ~>> V :=
  {|
    state := unit;
    init_state := tt;
    get x := bw f (snd x);
    set _ x := (tt , fw f x );
  |}.

Coercion bij_lens : bijection >-> lens.

Composition

Notation lid := (bij_lens bid).

Program Definition lcomp {U V W} (g : lens V W) (f : lens U V) : lens U W :=
  {|
    state := state g × state f;
    init_state := (init_state g , init_state f );
    get w := get f (snd (fst w), get g (fst (fst w), snd w ));
    set w u :=
      let v := get g (fst (fst w), snd w ) in
      let v' := set f (snd (fst w), v ) u in
      let w' := set g (fst (fst w), snd w ) (snd v') in
      ((fst w', fst v'), snd w')
  |}.

Infix "∘" := lcomp : lens_scope.

Lemma lcomp_lid_l {U V} (f : lens U V) :
  lid ∘ f == f.

Lemma lcomp_lid_r {U V} (f : lens U V) :
  f ∘ lid == f.

Lemma lcomp_lcomp {U V W X} :
  ∀ (h : lens W X) (g : lens V W) (f : lens U V),
    (h ∘ g ) ∘ f == h ∘ (g ∘ f ).

Lemma bij_lens_bcomp {U V W} (g : bijection V W) (f : bijection U V) :
  bij_lens (g ∘ f) == bij_lens g ∘ bij_lens f.

Tensor product

Program Definition prod_lens {U1 U2 V1 V2} (f1 : lens U1 V1) (f2 : lens U2 V2) :=
  {|
    init_state := (init_state f1 , init_state f2 );
    get v := (get f1 (fst (fst v), fst (snd v)),
              get f2 (snd (fst v), snd (snd v)));
    set v u :=
      let v1 := set f1 (fst (fst v), fst (snd v)) (fst u) in
      let v2 := set f2 (snd (fst v), snd (snd v)) (snd u) in
      ((fst v1 , fst v2 ), (snd v1 , snd v2 ));
  |}.

Infix "×" := prod_lens : lens_scope.

Initial lens

Program Definition ldrop {U} : lens unit U :=
{| init_state := tt; get _ := tt; set x _ := x |}.

Promoting a stateful lens to a strategy

Section LENS_STRAT.
Context {U V : Type} (f : lens U V).

Between any two visits back to the ready state, the strategy associated with a lens only needs to remember which u is currently the latest candidate for being written back into the (v, p) pair before we give it back to the environment. Given the lens laws, there are many equivalent ways to formulate it as far as when get and set are being used. But since we need to remember the latest incoming question for play structure purposes anyway, we choose to keep it constant and use this solution.

  Variant lpos : @position (glob U) (glob V) → Type :=
    | lready (p : state f) : lpos ready
    | lrunning (p : state f) (v : glob V) (u : glob U) : lpos (running v)
    | lsuspended (p : state f) (v : glob V) (u : glob U) : lpos (suspended v u).

  Inductive lens_has : ∀ {i}, lpos i → play i → Prop :=
    | lens_ready p :
        lens_has (lready p) pnil_ready
    | lens_oq p v u s :
        lens_has (lrunning p v u) s →
        get f (p , v ) = u →
        lens_has (lready p) (oq v :: s)
    | lens_pq p v u s :
        lens_has (lsuspended p v u) s →
        lens_has (lrunning p v u) (pq u :: s)
    | lens_suspended p v u :
        lens_has (lsuspended p v u) (pnil_suspended v u)
    | lens_oa p v u u' s :
        lens_has (lrunning p v u') s →
        lens_has (lsuspended p v u) (@oa _ _ v u u' :: s)
    | lens_pa p v u p' v' s :
        lens_has (lready p') s →
        set f (p , v ) u = (p', v') →
        lens_has (lrunning p v u) (@pa _ (glob V) v v' :: s).

  Obligation Tactic := cbn.

  Program Definition lens_strat_when {i} (p : lpos i) : strat (glob U) (glob V) i :=
    {| Downset.has := lens_has p |}.

  Definition lens_strat :=
    lens_strat_when (lready (init_state f)).

Some properties

  Lemma lens_strat_next_oq (p : state f) (v : glob V) (u : U) :
    get f (p , v ) = u →
    next (oq v) (lens_strat_when (lready p)) = lens_strat_when (lrunning p v u).

  Lemma lens_strat_next_pq (p : state f) (v : glob V) (u : glob U) :
    next (pq u) (lens_strat_when (lrunning p v u)) =
    lens_strat_when (lsuspended p v u).

  Lemma lens_strat_next_oa (p : state f) (v : glob V) (u : glob U) (u' : ar u) :
    next (oa u') (lens_strat_when (lsuspended p v u)) =
    lens_strat_when (lrunning p v u').

  Lemma lens_strat_next_pa (p : state f) (v : glob V) (u : U) p' (v' : ar v) :
    set f (p , v ) u = (p', v') →
    next (pa v') (lens_strat_when (lrunning p v u)) =
    lens_strat_when (lready p').
End LENS_STRAT.

Section LENS_STRAT_REF.
  Context {U V : Type} (f g : U ~>> V).

  Inductive lpos_eqv (R : rel _ _) : ∀ {i j}, rel (lpos f i) (lpos g j) :=
    | lready_eqv pf pg :
        R pf pg →
        lpos_eqv R (lready f pf) (lready g pg)
    | lrunning_eqv pf pg v u :
        R pf pg →
        lpos_eqv R (lrunning f pf v u) (lrunning g pg v u)
    | lsuspended_eqv pf pg v u :
        R pf pg →
        lpos_eqv R (lsuspended f pf v u) (lsuspended g pg v u).

  Hint Constructors lens_has lpos_eqv.

  Lemma lens_strat_ref :
    lens_eqv f g → lens_strat f [= lens_strat g.
End LENS_STRAT_REF.

Global Instance lens_strat_eq :
  Monotonic (@lens_strat) (forallr -, forallr -, lens_eqv ==> eq).

Refinement conventions and refinement squares

Giving lenses a strategy representation means that we can reuse the notions of refinement conventions and refinement square that we defined in that broader setting. Below we provide specialized definitions.

Definition lconv U V := conv (glob U) (glob V).
Infix "<~>" := lconv (at level 99, right associativity).

Definition lsq {U1 U2 V1 V2} (R : U1 <~> U2) (S : V1 <~> V2) (f1 : U1 ~>> V1) (f2 : U2 ~>> V2) :=
rsq R S (lens_strat f1) (lens_strat f2).

§5.4 State Encapsulation

Encapsulation primitive

This allows to hide part of the global state. All stateful lenses can be obtained as normal lense plus state encapsulation.

Program Definition encap {U} (u : U) : lens U unit :=
  {|
    state := U;
    init_state := u;
    get := fst;
    set _ u' := (u', tt );
  |}.

Lemma encap_prod {U V} (u : U) (v : V) :
  encap u × encap v == inv plu ∘ encap (u , v ).

Companion and conjoint of a stateful lens

Section LENS_RC.
  Context {U V : Type} (f : lens U V).
  Obligation Tactic := cbn.
  Hint Constructors rsp lens_has : core.

  Fixpoint lcp_has (p : state f) (s : rcp (glob U) (glob V)) : Prop :=
    match s with
      | rcp_allow u v ⇒
          get f (p , v) = u
      | rcp_forbid u v u' v' ⇒
          get f (p , v) = u ∧
          ∀ p', set f (p , v) u' ≠ (p', v')
      | rcp_cont u v u' v' k ⇒
          get f (p , v) = u ∧
          ∀ p', set f (p , v) u' = (p', v') → lcp_has p' k
    end.

  Program Definition lcp_when p : U <~> V :=
    {| Downset.has := lcp_has p |}.

  Definition lcp :=
    lcp_when (init_state f).

Useful lemmas

  Lemma rcnext_lcp pf (u : glob U) (v : glob V) pf' u' v' :
    get f (pf , v ) = u →
    set f (pf , v ) u' = (pf', v') →
    rcnext u v u' v' (lcp_when pf) = lcp_when pf'.

Companion properties

  Variant lcpipos pf : ∀ {i j}, lpos lid i → lpos f j → rspos i j → Type :=
    | lcpi_ready :
      lcpipos pf (lready lid tt)
                 (lready f pf) rs_ready
    | lcpi_running (u : glob U) (v : glob V) u' :
      lcpipos pf (lrunning lid tt u u')
                 (lrunning f pf v u') (rs_running u v)
    | lcpi_suspended (u : glob U) (v : glob V) u' :
      lcpipos pf (lsuspended lid tt u u')
                 (lsuspended f pf v u') (rs_suspended u v u' u').

  Lemma lcp_intro_when {pf i j pi pj pij} (q : @lcpipos pf i j pi pj pij) :
    match q with
      | lcpi_running _ u v _ | lcpi_suspended _ u v _ ⇒ get f (pf , v) = u
      | _ ⇒ True
    end →
    rsq_when vid (lcp_when pf) pij (lens_strat_when lid pi) (lens_strat_when f pj).

  Lemma lcp_intro :
    lsq vid lcp lid f.

  Variant lcpepos : ∀ pf {i j}, lpos f i → lpos lid j → rspos i j → Type :=
    | lcpe_ready pf :
      lcpepos pf (lready f pf)
                 (lready lid tt) rs_ready
    | lcpe_running pf (u : glob U) (v : glob V) (pf' : state f) u' v' :
      lcpepos pf' (lrunning f pf v u')
                 (lrunning lid tt v v') (rs_running v v)
    | lcpe_suspended pf (u : glob U) (v : glob V) (pf' : state f) u' v' :
      lcpepos pf' (lsuspended f pf v u')
                 (lsuspended lid tt v v') (rs_suspended v v u' v').

  Lemma lcp_elim_when {pf i j pi pj pij} (q : @lcpepos pf i j pi pj pij) :
    match q with
      | lcpe_running pf u v pf' u' v'
      | lcpe_suspended pf u v pf' u' v' ⇒
          get f (pf , v) = u ∧
          set f (pf , v) u' = (pf', v')
      | _ ⇒ True
    end →
    rsq_when (lcp_when pf) vid pij (lens_strat_when f pi) (lens_strat_when lid pj).

  Lemma lcp_elim :
    lsq lcp vid f lid.

This is just the transpose, maybe we could introduce that operation.

  Fixpoint lcj_has (p : state f) (s : rcp (glob V) (glob U)) : Prop :=
    match s with
      | rcp_allow v u ⇒
          get f (p , v) = u
      | rcp_forbid v u v' u' ⇒
          get f (p , v) = u ∧
          ∀ p', set f (p , v) u' ≠ (p', v')
      | rcp_cont v u v' u' k ⇒
          get f (p , v) = u ∧
          ∀ p', set f (p , v) u' = (p', v') → lcj_has p' k
    end.

  Program Definition lcj_when pf : V <~> U :=
    {| Downset.has := lcj_has pf |}.

  Definition lcj :=
    lcj_when (init_state f).

Useful lemmas

  Lemma rcnext_lcj pf (u : glob U) (v : glob V) pf' u' v' :
    get f (pf , v ) = u →
    set f (pf , v ) u' = (pf', v') →
    rcnext v u v' u' (lcj_when pf) = lcj_when pf'.

Companion properties

  Variant lcjipos : ∀ pf {i j}, lpos lid i → lpos f j → rspos i j → Type :=
    | lcji_ready pf :
      lcjipos pf (lready lid tt)
                 (lready f pf) rs_ready
    | lcji_running pf (u : glob U) (v : glob V) (pf' : state f) u' v' :
      lcjipos pf' (lrunning lid tt v v')
                  (lrunning f pf v u') (rs_running v v)
    | lcji_suspended pf (u : glob U) (v : glob V) (pf' : state f) u' v' :
      lcjipos pf' (lsuspended lid tt v v')
                  (lsuspended f pf v u') (rs_suspended v v v' u').

  Lemma lcj_intro_when {pf i j pi pj pij} (q : @lcjipos pf i j pi pj pij) :
    match q with
      | lcji_running pf u v pf' u' v'
      | lcji_suspended pf u v pf' u' v' ⇒
          get f (pf , v) = u ∧
          set f (pf , v) u' = (pf', v')
      | _ ⇒ True
    end →
    rsq_when (lcj_when pf) vid pij (lens_strat_when lid pi) (lens_strat_when f pj).

  Lemma lcj_intro :
    lsq lcj vid lid f.

  Variant lcjepos pf : ∀ {i j}, lpos f i → lpos lid j → rspos i j → Type :=
    | lcje_ready :
      lcjepos pf (lready f pf)
                 (lready lid tt) rs_ready
    | lcje_running (u : glob U) (v : glob V) u' :
      lcjepos pf (lrunning f pf v u')
                 (lrunning lid tt u u') (rs_running v u)
    | lcje_suspended (u : glob U) (v : glob V) u' :
      lcjepos pf (lsuspended f pf v u')
                 (lsuspended lid tt u u') (rs_suspended v u u' u').

  Lemma lcj_elim_when {pf i j pi pj pij} (q : @lcjepos pf i j pi pj pij) :
    match q with
      | lcje_running _ u v _ | lcje_suspended _ u v _ ⇒ get f (pf , v) = u
      | _ ⇒ True
    end →
    rsq_when vid (lcj_when pf) pij (lens_strat_when f pi) (lens_strat_when lid pj).

  Lemma lcj_elim :
    lsq vid lcj f lid.
End LENS_RC.

Spatial Composition

Based on the ingredients above, we can develop our theory of spatial composition, which is analogous to the tensor product but accepts only lenses on the right-hand side.

Definitions

Effect signatures

Definition scomp (E : esig) (U : Type) : esig :=
E × glob U.

Infix "@" := scomp (at level 40, left associativity) : esig_scope.

Strategies and lenses

Definition scomp_strat {E F U V} (σ: E ->> F) (f: lens U V) : E @ U ->> F @ V :=
  tstrat σ (lens_strat f).

Infix "@" := scomp_strat : strat_scope.

Global Instance scomp_strat_eq :
  Monotonic
    (@scomp_strat)
    (forallr -, forallr -, forallr -, forallr -, - ==> lens_eqv ==> eq).

Refinement conventions

Definition scomp_conv {E1 E2 U1 U2} (R : conv E1 E2) (S : conv (glob U1) (glob U2)) : conv (E1 @ U1) (E2 @ U2) :=
tconv R S.

Infix "@" := scomp_conv : conv_scope.

Refinement squares

Lemma scomp_rsq {E1 E2 F1 F2 U1 U2 V1 V2} :
  ∀ (R : E1 <=> E2) (S : F1 <=> F2) (R' : U1 <~> U2) (S' : V1 <~> V2)
         (σ1 : E1 ->> F1) (σ2 : E2 ->> F2) (f1 : U1 ~>> V1) (f2 : U2 ~>> V2),
    rsq R S σ1 σ2 →
    lsq R' S' f1 f2 →
    rsq (R @ R') (S @ S') (σ1 @ f1) (σ2 @ f2).

Infix "@" := (scomp_rsq _ _ _ _ _ _ _ _) : rsq_scope.

Functoriality

Horizontal component

Section SCOMP_ID.
  Context {E : esig} {U : Type}.

  Variant scipos : ∀ {i j ij}, epos eid i → lpos lid j → tpos i j ij → epos eid ij → Type :=
    | sci_ready :
      scipos eready (lready lid tt) tp_ready eready
    | sci_suspended (q : E) (u : U) :
      scipos (esuspended q) (lsuspended lid tt u u)
        (tp_suspended (E2:=glob U) (F2:=glob U) q u q u)
        (esuspended (f := @eid (E @ U)) (q , u )).

  Hint Constructors tstrat_has emor_has lens_has.

  Lemma scomp_id_when {i j ij pi pj pij p} (x : @scipos i j ij pi pj pij p) :
    tstrat_when pij (emor_when eid pi) (lens_strat_when lid pj) = emor_when eid p.

  Lemma scomp_id :
    (id E @ lid = id (E @ U))%strat.
End SCOMP_ID.

Section SCOMP_COMPOSE.
  Context {E F G : esig} {U V W : Type} {g : V ~>> W} {f : U ~>> V}.

  Variant sccpos :
    ∀ {i1 j1 i2 j2 ij1 ij2 i12 j12 ij12}, @cpos E F G i1 j1 ij1 →
                                               lpos (g ∘ f) ij2 →
                                               tpos ij1 ij2 ij12 →
                                               lpos g i2 → tpos i1 i2 i12 →
                                               lpos f j2 → tpos j1 j2 j12 →
                                               cpos i12 j12 ij12 → Type :=
      | scc_ready pg pf :
        sccpos cpos_ready
               (lready (g ∘f) (pg ,pf ))
               tp_ready
               (lready g pg) tp_ready
               (lready f pf) tp_ready
               cpos_ready
      | scc_left pg pf (**) q (w : glob W) pf' (v : glob V) :
        sccpos (cpos_left q)
               (lrunning (g ∘f) (pg ,pf ) w (get f (pf',v )))
               (tp_running q w)
               (lrunning g pg w v) (tp_running q w)
               (lready f pf') tp_ready
               (cpos_left (q ,w ))
      | scc_right pg pf (**) q (w : glob W) pf' (v : glob V) (**) m (u : glob U) :
        sccpos (cpos_right q m)
               (lrunning (g ∘f) (pg ,pf ) w u)
               (tp_running q w)
               (lsuspended g pg w v) (tp_suspended q w m v)
               (lrunning f pf' v u) (tp_running m v)
               (cpos_right (q ,w ) (m ,v ))
      | scc_suspended pg pf (**) q (w : glob W) pf' (v : glob V) (**) m u (**) x :
        sccpos (cpos_suspended q m x)
               (lsuspended (g ∘f) (pg ,pf ) w u)
               (tp_suspended q w x u)
               (lsuspended g pg w v) (tp_suspended q w m v)
               (lsuspended f pf' v u) (tp_suspended m v x u)
               (cpos_suspended (q ,w ) (m ,v ) (x ,u )).

  Hint Constructors lens_has tstrat_has comp_has pref sccpos.

  Lemma scomp_compose_when_1 {i1 j1 i2 j2 ij1 ij2 i12 j12 ij12 pij1 pij2 pij12 pi2 pi12 pj2 pj12 pij12'} :
    ∀ p: @sccpos i1 j1 i2 j2 ij1 ij2 i12 j12 ij12 pij1 pij2 pij12 pi2 pi12 pj2 pj12 pij12',
    ∀ s1 t1 st1, comp_has pij1 s1 t1 st1 →
    ∀ st2, lens_has (g ∘f) pij2 st2 →
    ∀ st12, tstrat_has pij12 st1 st2 st12 →
    match p with
      | scc_ready pg pf ⇒
        True
      | scc_left pg pf q w pf' v
      | scc_right pg pf q w pf' v _ _
      | scc_suspended pg pf q w pf' v _ _ _ ⇒
        set f (pf, get g (pg, w)) (get f (pf', v)) = (pf', v)
    end →
    ∃ s1' t1' s2 t2 s12 t12 ,
      s1' [= s1 ∧ t1' [= t1 ∧
      lens_has g pi2 s2 ∧
      lens_has f pj2 t2 ∧
      tstrat_has pi12 s1' s2 s12 ∧
      tstrat_has pj12 t1' t2 t12 ∧
      comp_has pij12' s12 t12 st12.

  Lemma scomp_compose_when_2 {i1 j1 i2 j2 ij1 ij2 i12 j12 ij12 pij1 pij2 pij12 pi2 pi12 pj2 pj12 pij12'} :
    ∀ p: @sccpos i1 j1 i2 j2 ij1 ij2 i12 j12 ij12 pij1 pij2 pij12 pi2 pi12 pj2 pj12 pij12',
    ∀ s12 t12 st12, comp_has pij12' s12 t12 st12 →
    ∀ s1 s2 t1 t2,
    lens_has g pi2 s2 →
    lens_has f pj2 t2 →
    tstrat_has pi12 s1 s2 s12 →
    tstrat_has pj12 t1 t2 t12 →
    match p with
      | scc_ready pg pf ⇒
        True
      | scc_left pg pf q w pf' v
      | scc_right pg pf q w pf' v _ _
      | scc_suspended pg pf q w pf' v _ _ _ ⇒
        set f (pf, get g (pg, w)) (get f (pf', v)) = (pf', v)
    end →
    ∃ st1 st2 ,
      comp_has pij1 s1 t1 st1 ∧
      lens_has (g ∘f) pij2 st2 ∧
      tstrat_has pij12 st1 st2 st12.
End SCOMP_COMPOSE.

Lemma scomp_compose {E F G U V W} :
  ∀ (σ : F ->> G) (τ : E ->> F) (g : V ~>> W) (f : U ~>> V),
    ((σ ⊙ τ ) @ (g ∘ f ) = (σ @ g ) ⊙ (τ @ f ))%strat.

Vertical component

Lemma scomp_vid {E U} :
  ((@vid E ) @ (@vid (glob U)) = @vid (E @ U))%conv.

Lemma scomp_vcomp {E F G U V W} :
  ∀ (R1 : conv E F) (S1 : conv F G)
         (R2 : conv (glob U) (glob V)) (S2 : conv (glob V) (glob W)),
    ((R1 ;; S1 ) @ (R2 ;; S2 ) = (R1 @ R2 ) ;; (S1 @ S2 ))%conv.

Horizontal structural isomorphisms

XXX not sure if the left unitor makes that much sense here

Definition slu {U} : 1 @ U ->> glob U := tlu.
Definition slur {U} : glob U ->> 1 @ U := tlur.

Global Instance slu_iso {U} : @Isomorphism (1 @ U) (glob U) slu slur.

Definition sru {E} : E @ unit ->> E := tru.
Definition srur {E} : E ->> E @ unit := trur.

Global Instance sru_iso {E} : @Isomorphism (E @ unit) E sru srur.

Definition sassoc {E U V} : E @ U @ V ->> E @ (U × V ) := @tassoc E (glob U) (glob V).
Definition sassocr {E U V} : E @ (U × V ) ->> E @ U @ V := @tassocr E (glob U) (glob V).

Global Instance sassoc_iso {E U V}: Isomorphism (@sassoc E U V) (@sassocr E U V).

Additional properties of embedded structural isomorphisms

Naturality of sru

Section SRU_NATURAL.
  Context {E F : esig}.
  Hint Constructors emor_has comp_has tstrat_has pref lens_has.

  Variant srunpos :
    ∀ i {j1 j2 k ik ijk},
           epos tru j1 → cpos i j1 ijk →
           epos tru j2 → lpos bid k → tpos i k ik → cpos j2 ik ijk → Type :=
    | srun_ready :
        srunpos ready eready cpos_ready
                eready (lready bid tt) tp_ready cpos_ready
    | srun_running (q : F) :
        srunpos (running q) eready (cpos_left q)
                (esuspended q) (lrunning bid tt tt tt)
                (tp_running q (tt : glob unit))
                (cpos_right (F:=F@unit) q (q ,tt ))
    | srun_suspended (q : F) (m : E) :
        srunpos (suspended q m) (esuspended m)
                (cpos_suspended (E:=E@unit) q m (m ,tt ))
                (esuspended q) (lsuspended bid tt tt tt)
                (tp_suspended (E2 := glob unit) (F2 := glob unit) q tt m tt)
                (cpos_suspended (F:=F@unit) (E:=E@unit) q (q ,tt ) (m ,tt )).

  Lemma sru_natural_has_1 {i j1 j2 k ik ijk pj1 pijk pj2 pk pik pijk'} :
    @srunpos i j1 j2 k ik ijk pj1 pijk pj2 pk pik pijk' →
    ∀ s w t,
      emor_has tru pj1 t →
      comp_has pijk s t w →
      ∃ s' t' u su ,
          s' [= s ∧
          emor_has tru pj2 t' ∧
          lens_has bid pk u ∧
          tstrat_has pik s' u su ∧
          comp_has pijk' t' su w.

  Lemma sru_natural_has_2 {i j1 j2 k ik ijk pj1 pijk pj2 pk pik pijk'} :
    @srunpos i j1 j2 k ik ijk pj1 pijk pj2 pk pik pijk' →
    ∀ s t u su w,
      emor_has tru pj2 t →
      lens_has bid pk u →
      tstrat_has pik s u su →
      comp_has pijk' t su w →
      ∃ s' t',
        s' [= s ∧
        emor_has tru pj1 t' ∧
        comp_has pijk s' t' w.

  Lemma sru_natural (σ : E ->> F) :
    σ ⊙ sru = sru ⊙ (σ @ unit ).

  Lemma srur_natural (σ : E ->> F) :
    srur ⊙ σ = (σ @ unit ) ⊙ srur.
End SRU_NATURAL.

Open Scope strat_scope.