From d1fb7ffd50922bd0943a77bd24ec8e0b99889c36 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Mon, 12 Oct 2020 15:22:49 +0200
Subject: [PATCH] Added spec for telescoped version of send and bumped
 proofmode

---
 theories/channel/channel.v   | 16 ++++++++++++++++
 theories/channel/proofmode.v | 11 +++++------
 2 files changed, 21 insertions(+), 6 deletions(-)

diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 0832aa2..6a69f5e 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -239,6 +239,22 @@ Section channel.
       iIntros "_". iApply "HΦ". iExists γ, Right, l, r, lk. eauto 10 with iFrame.
   Qed.
 
+  Lemma send_spec_tele {TT} c (tt : TT)
+        (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
+    {{{ c ↣ (<!.. x > MSG v x {{ P x }}; p x) ∗ P tt }}}
+      send c (v tt)
+    {{{ RET #(); c ↣ (p tt) }}}.
+  Proof.
+    iIntros (Φ) "[Hc HP] HΦ".
+    iDestruct (iProto_mapsto_le _ _ (<!> MSG v tt; p tt)%proto with "Hc [HP]")
+      as "Hc".
+    { iIntros "!>".
+      iApply iProto_le_trans.
+      iApply iProto_le_texist_intro_l.
+      by iFrame "HP". }
+    by iApply (send_spec with "Hc").
+  Qed.
+
   Lemma try_recv_spec {TT} c (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
     {{{ c ↣ <?.. x> MSG v x {{ P x }}; p x }}}
       try_recv c
diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 58701fb..24b5683 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -312,12 +312,11 @@ Proof.
   destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //.
   rewrite envs_split_sound //; rewrite (envs_app_sound Δ2) //; simpl.
   destruct HΦ as (-> & -> & ->). rewrite right_id assoc.
-  assert (c ↣ p ∗ tele_app tP x ⊢
-    c ↣ <!> MSG tele_app tv x; tele_app tp x) as ->.
-  { iIntros "[Hc Hm]". iApply (iProto_mapsto_le with "Hc"); iIntros "!>".
-    iApply iProto_le_trans; [iApply Hp|]. rewrite Hm.
-    iApply iProto_le_trans; [iApply iProto_le_texist_intro_l|]. by iFrame. }
-  eapply bi.wand_apply; [rewrite -wp_bind; by eapply send_spec|].
+  assert (c ↣ p ⊢
+    c ↣ <!.. (x : TT)> MSG tele_app tv x {{ tele_app tP x }}; tele_app tp x) as ->.
+  { iIntros "Hc". iApply (iProto_mapsto_le with "Hc"); iIntros "!>".
+    iApply iProto_le_trans; [iApply Hp|]. by rewrite Hm. }
+  eapply bi.wand_apply; [rewrite -wp_bind; by eapply send_spec_tele|].
   by rewrite -bi.later_intro.
 Qed.
 
-- 
GitLab