Commit 0a068c24 authored by Dan Frumin's avatar Dan Frumin

Show the compatibility lemma for the derived parallel composition

parent 3c36b147
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth.
From iris.base_logic Require Import lib.auth.
From iris_logrel.F_mu_ref_conc Require Export examples.lock.
From iris_logrel.F_mu_ref_conc Require Import tactics rel_tactics soundness_binary relational_properties.
From iris.program_logic Require Import adequacy.
From iris_logrel.F_mu_ref_conc Require Import hax.
Definition par : val := λ: "e1" "e2",
let: "x1" := ref InjL #() in
Fork ("x1" <- InjR ("e1" #()));;
let: "x2" := "e2" #() in
let: "f" := rec: "f" <> := case: !"x1" of
InjL => λ: <>, "f" #()
| InjR => λ: "v", "v"
end
in ("f" #(), "x2").
Lemma par_type Γ τ1 τ2 :
typed Γ par
(TArrow (TArrow TUnit τ1) (TArrow (TArrow TUnit τ2)
(TProd τ1 τ2))).
Proof.
unfold par. unlock.
eauto 40 with typeable.
Qed.
Hint Resolve par_type : typeable.
Section compatibility.
Context `{heapIG Σ, cfgSG Σ}.
Lemma bin_log_related_par Γ E e1 e2 e1' e2' τ1 τ2 :
specN E
logN E
{E,E;Γ} e1 log e1' : TArrow TUnit τ1 -
{E,E;Γ} e2 log e2' : TArrow TUnit τ2 -
{E,E;Γ} par e1 e2 log par e1' e2' : TProd τ1 τ2.
Proof.
iIntros (??) "He1 He2".
iApply (bin_log_related_app with "[He1] He2").
iApply (bin_log_related_app with "[] He1").
iApply binary_fundamental_masked; eauto with typeable.
Qed.
End compatibility.
......@@ -24,6 +24,7 @@ F_mu_ref_conc/notation.v
F_mu_ref_conc/examples/lock.v
F_mu_ref_conc/examples/counter.v
F_mu_ref_conc/examples/lateearlychoice.v
F_mu_ref_conc/examples/par.v
#F_mu_ref_conc/examples/stack/stack_rules.v
#F_mu_ref_conc/examples/stack/CG_stack.v
#F_mu_ref_conc/examples/stack/FG_stack.v
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment