Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coq

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 →