Soundness (Theorem 6.12)

Finally, all the pieces are in place to prove that bisimilarity of induced LTS is sound w.r.t. substitution equivalence. Having worked hard to establish adequacy and congruence of weak bisimilarity for composition, very little remains to do here.

We consider a language abstractly captured as a machine satisfying an appropriate axiomatization.

  Context {T C} {CC : context T C} {CL : context_laws T C}.
  Context {val} {VM : subst_monoid val} {VML : subst_monoid_laws val}.
  Context {conf} {CM : subst_module val conf} {CML : subst_module_laws val conf}.
  Context {obs : obs_struct T C} {M : machine val conf obs} {ML : machine_laws val conf obs}.
  Context {VV : var_assumptions val}.

We define substitution equivalence of two language machine configurations (Def 4.24).

  Definition substeq {Γ} Δ (a b : conf Γ) : Prop
    := forall γ : Γ =[val]> Δ, evalₒ (a ₜ⊛ γ) ≈ evalₒ (b ₜ⊛ γ).
  Notation "x ≈⟦sub Δ ⟧≈ y" := (substeq Δ x y) (at level 50).

We define an intermediate notion of equivalence, stating that for any assignment γ, the induced LTS are bisimilar when composed with the passive interpretation of γ.

  Definition barb {Γ} Δ (x y : conf Γ) : Prop
    := forall γ : Γ =[val]> Δ,
         (inj_init_act Δ x ∥ inj_init_pas γ)
       ≈ (inj_init_act Δ y ∥ inj_init_pas γ).
  Notation "x ≈⟦barb Δ ⟧≈ y" := (barb Δ x y) (at level 50).

Barbed equivalence is sound w.r.t. substitution equivalence, by swapping the naive composition with the guarded one and then applying adequacy.

  Theorem barb_correction {Γ} Δ (x y : conf Γ) : x ≈⟦barb Δ ⟧≈ y -> x ≈⟦sub Δ ⟧≈ y.T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Γ, Δ: C
x, y: conf Γ
x ≈⟦barb Δ ⟧≈ y -> x ≈⟦sub Δ ⟧≈ y
  Proof.T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Γ, Δ: C
x, y: conf Γ
x ≈⟦barb Δ ⟧≈ y -> x ≈⟦sub Δ ⟧≈ y
    intros H e.T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Γ, Δ: C
x, y: conf Γ
H: x ≈⟦barb Δ ⟧≈ y
e: Γ =[ val ]> Δ
evalₒ (x ₜ⊛ e) ≈ evalₒ (y ₜ⊛ e)
    rewrite (it_eq_wbisim _ _ _ (adequacy x e)), (it_eq_wbisim _ _ _ (adequacy y e)).T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Γ, Δ: C
x, y: conf Γ
H: x ≈⟦barb Δ ⟧≈ y
e: Γ =[ val ]> Δ
(inj_init_act Δ x ∥g inj_init_pas e)
≈ (inj_init_act Δ y ∥g inj_init_pas e)
    unfold compo_ev_guarded; rewrite 2 iter_evg_iter; apply H.
  Qed.

Our main theorem: bisimilarity of induced OGS machine strategies is sound w.r.t. substitution equivalence, by applying barbed equivalence soundness, swapping the naive composition with the opaque one and then applying congruence.

  Theorem ogs_correction {Γ} Δ (x y : conf Γ) : x ≈⟦ogs Δ ⟧≈ y -> x ≈⟦sub Δ ⟧≈ y.T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Γ, Δ: C
x, y: conf Γ
x ≈⟦ogs Δ ⟧≈ y -> x ≈⟦sub Δ ⟧≈ y
  Proof.T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Γ, Δ: C
x, y: conf Γ
x ≈⟦ogs Δ ⟧≈ y -> x ≈⟦sub Δ ⟧≈ y
    intro H; apply barb_correction.T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Γ, Δ: C
x, y: conf Γ
H: x ≈⟦ogs Δ ⟧≈ y
x ≈⟦barb Δ ⟧≈ y
    intro e; unfold compo.T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Γ, Δ: C
x, y: conf Γ
H: x ≈⟦ogs Δ ⟧≈ y
e: Γ =[ val ]> Δ
Delay.iter_delay compo_body
  {|
    red_ctx := Ctx.ccon Ctx.cnil Γ;
    red_act := inj_init_act Δ x;
    red_pas := inj_init_pas e
  |}
≈ Delay.iter_delay compo_body
    {|
      red_ctx := Ctx.ccon Ctx.cnil Γ;
      red_act := inj_init_act Δ y;
      red_pas := inj_init_pas e
    |}
    rewrite <- 2 (compo_compo_alt (x := RedT _ _)).T, C: Type
CC: context T C
CL: context_laws T C
val: Fam₁ T C
VM: subst_monoid val
VML: subst_monoid_laws val
conf: Fam₀ T C
CM: subst_module val conf
CML: subst_module_laws val conf
obs: obs_struct T C
M: machine val conf obs
ML: machine_laws val conf obs
VV: var_assumptions val
Γ, Δ: C
x, y: conf Γ
H: x ≈⟦ogs Δ ⟧≈ y
e: Γ =[ val ]> Δ
Delay.iter_delay compo_alt_body
  (reduce_t_inj
     {|
       red_ctx := Ctx.ccon Ctx.cnil Γ;
       red_act := inj_init_act Δ x;
       red_pas := inj_init_pas e
     |})
≈ Delay.iter_delay compo_alt_body
    (reduce_t_inj
       {|
         red_ctx := Ctx.ccon Ctx.cnil Γ;
         red_act := inj_init_act Δ y;
         red_pas := inj_init_pas e
       |})
    apply compo_alt_proper; [ exact H | intro; reflexivity ].
  Qed.
End with_param.

If you wish to double check these results you can run the following commands at this point in the file:

About ogs_correction.ogs_correction :
forall {T C : Type} {CC : context T C}
  {CL : context_laws T C} {val : Fam₁ T C}
  {VM : subst_monoid val},
subst_monoid_laws val ->
forall (conf : Fam₀ T C) (CM : subst_module val conf),
subst_module_laws val conf ->
forall (obs : obs_struct T C)
  (M : machine val conf obs),
machine_laws val conf obs ->
var_assumptions val ->
forall (Γ Δ : C) (x y : conf Γ),
x ≈⟦ogs Δ ⟧≈ y -> substeq Δ x y

ogs_correction is not universe polymorphic
Arguments ogs_correction {T C}%type_scope
  {CC CL val VM VML conf CM CML obs M ML VV Γ} Δ x 
  y _ γ
ogs_correction is opaque
Expands to: Constant Soundness.ogs_correction
Print Assumptions ogs_correction.Axioms:
Eqdep.Eq_rect_eq.eq_rect_eq
  : forall (U : Type) (p : U) (Q : U -> Type)
      (x : Q p) (h : p = p), x = rew [Q] h in x

The first command will explicit the assumptions of the theorem, which we show how to provide with several examples:

The second command will explicit if any axiom has been used to establish the result. As stated in the prelude, we exclusively use Eq_rect_eq.eq_rect_eq, ie Streicher's axiom K.