From 75a90bac56f4ea3ddf2108b47c6131fa6a7695c5 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Fri, 7 Aug 2020 11:23:47 +0200
Subject: [PATCH] Added framing example

---
 theories/examples/subprotocols.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/theories/examples/subprotocols.v b/theories/examples/subprotocols.v
index d828053..2a4d355 100644
--- a/theories/examples/subprotocols.v
+++ b/theories/examples/subprotocols.v
@@ -11,6 +11,14 @@ Section basics.
     (<! (l1 : loc)> MSG (#l1, #l2') {{ l1 ↦ #20 }}; END).
   Proof. iIntros "Hl2'" (l1) "Hl1". iExists l1, l2'. by iFrame "Hl1 Hl2'". Qed.
 
+  Lemma framing_example (P Q R : iProp Σ) (v w : val) :
+    ⊢ ((<!> MSG v {{ P }} ; <?> MSG w {{ Q }}; END)%proto ⊑
+       (<!> MSG v {{ P ∗ R }} ; <?> MSG w {{ Q ∗ R }};END)%proto)%proto.
+  Proof.
+    iIntros "[HP HR]". iFrame "HP". iModIntro.
+    iIntros "HQ". iFrame "HQ HR". eauto.
+  Qed.
+
   Section program_reuse.
     Context {T U R : Type}.
     Context (IT : T -> val -> iProp Σ).
-- 
GitLab