Commit 6e6cf9b3 authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

Redefined send_vs in terms of chan_frag_snoc

parent 5c2fa2d5
...@@ -120,15 +120,19 @@ Section logrel. ...@@ -120,15 +120,19 @@ Section logrel.
iFrame. iFrame.
Qed. Qed.
Definition to_side s :=
match s with
| Left => #true
| Right => #false
end.
Lemma send_vs c γ s (P : val Prop) st E : Lemma send_vs c γ s (P : val Prop) st E :
N E N E
c @ s : TSend P st {γ} ={E,E∖↑N}= c @ s : TSend P st {γ} ={E,E∖↑N}=
l r, chan_frag (st_c_name γ) c l r l r, chan_frag (st_c_name γ) c l r
( v, P v - ( v, P v -
match s with chan_frag_snoc (st_c_name γ) c l r (to_side s) v
| Left => chan_frag (st_c_name γ) c (l ++ [v]) r ={E N,E}= c @ s : st v {γ}).
| Right => chan_frag (st_c_name γ) c l (r ++ [v])
end ={E N,E}= c @ s : st v {γ}).
Proof. Proof.
iIntros (Hin) "[Hstf #[Hcctx Hinv]]". iIntros (Hin) "[Hstf #[Hcctx Hinv]]".
iMod (inv_open with "Hinv") as "Hinv'"=> //. iMod (inv_open with "Hinv") as "Hinv'"=> //.
...@@ -182,12 +186,6 @@ Section logrel. ...@@ -182,12 +186,6 @@ Section logrel.
iModIntro. iFrame "Hcctx ∗ Hinv". iModIntro. iFrame "Hcctx ∗ Hinv".
Qed. Qed.
Definition to_side s :=
match s with
| Left => #true
| Right => #false
end.
Lemma send_st_spec st γ c s (P : val Prop) v : Lemma send_st_spec st γ c s (P : val Prop) v :
P v P v
{{{ c @ s : TSend P st {γ} }}} {{{ c @ s : TSend P st {γ} }}}
......
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