From 2f15e108f070f2bb31394d9224c158e3db3d04e3 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 24 Nov 2016 22:02:22 +0100
Subject: [PATCH] Boxes : insert full slices.

---
 base_logic/lib/boxes.v | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/base_logic/lib/boxes.v b/base_logic/lib/boxes.v
index 5ecb2d037..3ae9b0c7b 100644
--- a/base_logic/lib/boxes.v
+++ b/base_logic/lib/boxes.v
@@ -85,7 +85,7 @@ Proof.
   - by rewrite big_sepM_empty.
 Qed.
 
-Lemma box_insert E f P Q :
+Lemma box_insert_empty E f P Q :
   ▷ box N f P ={E}=∗ ∃ γ, ⌜f !! γ = None⌝ ∗
     slice N γ Q ∗ ▷ box N (<[γ:=false]> f) (Q ∗ P).
 Proof.
@@ -143,6 +143,18 @@ Proof.
     iFrame; eauto.
 Qed.
 
+Lemma box_insert_full E f P Q :
+  ↑N ⊆ E →
+  ▷ Q ∗ ▷ box N f P ={E}=∗ ∃ γ, ⌜f !! γ = None⌝ ∗
+    slice N γ Q ∗ ▷ box N (<[γ:=true]> f) (Q ∗ P).
+Proof.
+  iIntros (?) "[HQ Hbox]".
+  iMod (box_insert_empty with "Hbox") as (γ) "(% & #Hslice & Hbox)".
+  iExists γ. iFrame "%#".
+  iMod (box_fill with "[$Hslice $HQ $Hbox]"). done.
+  by apply lookup_insert. by rewrite insert_insert.
+Qed.
+
 Lemma box_empty E f P Q γ :
   ↑N ⊆ E →
   f !! γ = Some true →
-- 
GitLab