From ffb0a675015feca525d40fc7abfa77de3e48223b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 17 Feb 2016 17:20:39 +0100
Subject: [PATCH] prove recv_strengthen

---
 barrier/barrier.v | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/barrier/barrier.v b/barrier/barrier.v
index 224c0e889..43ad8a574 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -220,6 +220,12 @@ Section proof.
   Lemma recv_strengthen l P1 P2 :
     (P1 -★ P2) ⊑ (recv l P1 -★ recv l P2).
   Proof.
-  Abort.
+    apply wand_intro_l. rewrite /recv. rewrite sep_exist_r. apply exist_mono=>γ.
+    rewrite sep_exist_r. apply exist_mono=>P. rewrite sep_exist_r.
+    apply exist_mono=>Q. rewrite sep_exist_r. apply exist_mono=>i.
+    rewrite -!assoc. apply sep_mono_r, sep_mono_r, sep_mono_r, sep_mono_r.
+    rewrite (later_intro (P1 -★ _)%I) -later_sep. apply later_mono.
+    apply wand_intro_l. rewrite !assoc wand_elim_r wand_elim_r. done.
+  Qed.
 
 End proof.
-- 
GitLab