From 6e6cf9b3453fc9d64bee76572f7f25d0022772bb Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date: Fri, 12 Apr 2019 12:43:10 +0200
Subject: [PATCH] Redefined send_vs in terms of chan_frag_snoc

---
 theories/logrel.v | 18 ++++++++----------
 1 file changed, 8 insertions(+), 10 deletions(-)

diff --git a/theories/logrel.v b/theories/logrel.v
index fec60b4..1340800 100644
--- a/theories/logrel.v
+++ b/theories/logrel.v
@@ -120,15 +120,19 @@ Section logrel.
     iFrame.
   Qed.
 
+  Definition to_side s :=
+    match s with
+    | Left  => #true
+    | Right => #false
+    end.
+
   Lemma send_vs c γ s (P : val → Prop) st E :
     ↑N ⊆ E →
     ⟦ c @ s : TSend P st ⟧{γ} ={E,E∖↑N}=∗
       ∃ l r, chan_frag (st_c_name γ) c l r ∗
       ▷ (∀ v, ⌜P v⌝ -∗
-              match s with
-              | Left  => chan_frag (st_c_name γ) c (l ++ [v]) r
-              | Right => chan_frag (st_c_name γ) c l (r ++ [v])
-              end ={E∖ ↑N,E}=∗ ⟦ c @ s : st v ⟧{γ}).
+               chan_frag_snoc (st_c_name γ) c l r (to_side s) v
+              ={E∖ ↑N,E}=∗ ⟦ c @ s : st v ⟧{γ}).
   Proof.
     iIntros (Hin) "[Hstf #[Hcctx Hinv]]".
     iMod (inv_open with "Hinv") as "Hinv'"=> //.
@@ -182,12 +186,6 @@ Section logrel.
       iModIntro. iFrame "Hcctx ∗ Hinv".
   Qed.
 
-  Definition to_side s :=
-    match s with
-    | Left  => #true
-    | Right => #false
-    end.
-
   Lemma send_st_spec st γ c s (P : val → Prop) v :
     P v →
     {{{ ⟦ c @ s : TSend P st ⟧{γ} }}}
-- 
GitLab