Commit fd7dc61d authored by Jonas Kastberg's avatar Jonas Kastberg

Proved spar using typing rule instead of breaking abstraction

parent 821a4c23
......@@ -438,12 +438,12 @@ Section properties.
(** Parallel composition properties *)
Lemma ltyped_par Γ Γ' Γ1 Γ1' Γ2 Γ2' e1 e2 A B :
env_split Γ Γ1 Γ2 -
env_split Γ' Γ1' Γ2' -
(Γ1 e1 : A Γ1') -
(Γ2 e2 : B Γ2') -
env_split Γ' Γ1' Γ2' -
Γ e1 ||| e2 : A * B Γ'.
Proof.
iIntros "#Hsplit #Hsplit' #H1 #H2" (vs) "!> HΓ /=".
iIntros "#Hsplit #H1 #H2 #Hsplit'" (vs) "!> HΓ /=".
iDestruct ("Hsplit" with "HΓ") as "[HΓ1 HΓ2]".
wp_apply (wp_par with "[HΓ1] [HΓ2]").
- iApply ("H1" with "HΓ1").
......@@ -460,10 +460,10 @@ Section properties.
Context `{chanG Σ}.
Lemma ltyped_new_chan Γ S :
Γ new_chan : () (chan S * chan (lty_dual S)) Γ.
Γ new_chan : () (chan S * chan (lty_dual S)) Γ.
Proof.
iIntros (vs) "!> HΓ /=". iApply wp_value. iFrame "HΓ".
iIntros "!>" (u) ">->".
iIntros (u) ">->".
iApply (new_chan_spec with "[//]"); iIntros (c1 c2) "!> [Hp1 Hp2]".
iExists c1, c2. iSplit=>//. iFrame "Hp1 Hp2".
Qed.
......@@ -471,37 +471,44 @@ Section properties.
Section with_spawn.
Context `{spawnG Σ}.
Definition spar : val :=
(λ: "e2" "e1",
Definition spar : expr :=
(λ: "e1" "e2",
let: "c" := new_chan #() in
("e1" (Fst "c")) ||| ("e2" (Snd "c")))%V.
Lemma ltyped_spar Γ Γ1 Γ2 Γ' Γ1' Γ2' e1 e2 S A B :
env_split Γ Γ1 Γ2 -
env_split Γ' Γ1' Γ2' -
(Γ1 e1 : (chan S) A Γ1') -
(Γ2 e2 : (chan (lty_dual S)) B Γ2') -
Γ spar e2 e1 : A * B Γ'.
let: "c1" := Fst "c" in
let: "c2" := Snd "c" in
("e1" "c1") ||| ("e2" "c2"))%E.
Lemma ltyped_spar Γ S A B :
Γ spar : ((chan S) A) (chan (lty_dual S) B) A * B.
Proof.
iIntros "#Hsplit1 #Hsplit2 #He1 #He2" (vs) "!> HΓ /=".
iDestruct ("Hsplit1" with "HΓ") as "[HΓ1 HΓ2]".
iDestruct ("He1" with "HΓ1") as "Hv1".
iDestruct ("He2" with "HΓ2") as "Hv2".
wp_apply (wp_wand with "Hv1").
iIntros (v1) "[Hv1 HΓ1']".
wp_apply (wp_wand with "Hv2").
iIntros (v2) "[Hv2 HΓ2']".
wp_lam. wp_pures.
wp_apply (new_chan_spec (lsty_car S))=> //.
iIntros (c1 c2) "[Hc1 Hc2]".
wp_pures.
wp_apply (wp_par with "[Hc1 Hv1] [Hc2 Hv2] [HΓ1' HΓ2']").
- wp_apply "Hv1". iApply "Hc1".
- wp_apply "Hv2". iApply "Hc2".
- iIntros (w1 w2) "[Hw1 Hw2]".
iSplitL "Hw1 Hw2".
+ iExists _, _. iFrame. done.
+ iApply "Hsplit2". iFrame "HΓ1' HΓ2'".
rewrite /spar.
iApply ltyped_lam; [ iApply env_split_id_l | ].
iApply ltyped_lam; [ iApply env_split_id_r | ].
iApply ltyped_let.
{ iApply ltyped_app; [ iApply ltyped_unit | iApply ltyped_new_chan ]. }
iApply ltyped_let; [ by iApply ltyped_fst | ].
rewrite insert_insert.
iApply ltyped_let; [ by iApply ltyped_snd | ].
rewrite /binder_insert (insert_commute _ "c1" "c") // insert_insert.
iApply (ltyped_par).
- iApply env_split_right; last first.
{ rewrite (insert_commute _ "c1" "e2"); [ | eauto ].
rewrite (insert_commute _ "c" "e2"); [ | eauto ].
iApply env_split_right; last by iApply env_split_id_r.
eauto. eauto. }
eauto. eauto.
- iApply ltyped_app; by iApply ltyped_var.
- iApply ltyped_app; by iApply ltyped_var.
- rewrite insert_insert.
rewrite (insert_commute _ "c2" "e2") // insert_insert.
rewrite (insert_commute _ "c1" "c") // insert_insert.
rewrite (insert_commute _ "c1" "e1") //
(insert_commute _ "c" "e1") // insert_insert.
iApply env_split_left=> //; last first.
iApply env_split_left=> //; last first.
iApply env_split_left=> //; last first.
iApply env_split_id_l.
eauto. eauto. eauto.
Qed.
End with_spawn.
......
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