From 42cf780adc3d61438701a106e50e07977c9b6abb Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 25 Nov 2016 17:13:20 +0100
Subject: [PATCH] Stronger splitting rule for boxes.

---
 base_logic/lib/boxes.v | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/base_logic/lib/boxes.v b/base_logic/lib/boxes.v
index 22c010f75..fb8f4e1bb 100644
--- a/base_logic/lib/boxes.v
+++ b/base_logic/lib/boxes.v
@@ -233,22 +233,24 @@ Qed.
 Lemma box_split E f P Q1 Q2 γ b :
   ↑N ⊆ E → f !! γ = Some b →
   slice N γ (Q1 ∗ Q2) -∗ ▷ box N f P ={E}=∗ ∃ γ1 γ2,
-    ⌜delete γ f !! γ1 = None⌝ ∗ ⌜delete γ f !! γ2 = None⌝ ∗
+    ⌜delete γ f !! γ1 = None⌝ ∗ ⌜delete γ f !! γ2 = None⌝ ∗ ⌜γ1 ≠ γ2⌝ ∗
     slice N γ1 Q1 ∗ slice N γ2 Q2 ∗ ▷ box N (<[γ2 := b]>(<[γ1 := b]>(delete γ f))) P.
 Proof.
   iIntros (??) "#Hslice Hbox". destruct b.
   - iMod (box_delete_full with "Hslice Hbox") as (P') "([HQ1 HQ2] & Heq & Hbox)"; try done.
     iMod (box_insert_full Q1 with "HQ1 Hbox") as (γ1) "(% & #Hslice1 & Hbox)". done.
     iMod (box_insert_full Q2 with "HQ2 Hbox") as (γ2) "(% & #Hslice2 & Hbox)". done.
-    iExists γ1, γ2. iFrame "%#". iModIntro. iSplit.
-    { iPureIntro. by eapply lookup_insert_None. }
+    iExists γ1, γ2. iFrame "%#". iModIntro. iSplit; last iSplit; try iPureIntro.
+    { by eapply lookup_insert_None. }
+    { by apply (lookup_insert_None (delete γ f) γ1 γ2 true). }
     iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
     iNext. iRewrite "Heq". iPureIntro. rewrite assoc. f_equiv. by rewrite comm. done.
   - iMod (box_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done.
     iMod (box_insert_empty Q1 with "Hbox") as (γ1) "(% & #Hslice1 & Hbox)".
     iMod (box_insert_empty Q2 with "Hbox") as (γ2) "(% & #Hslice2 & Hbox)".
-    iExists γ1, γ2. iFrame "%#". iModIntro. iSplit.
-    { iPureIntro. by eapply lookup_insert_None. }
+    iExists γ1, γ2. iFrame "%#". iModIntro. iSplit; last iSplit; try iPureIntro.
+    { by eapply lookup_insert_None. }
+    { by apply (lookup_insert_None (delete γ f) γ1 γ2 false). }
     iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
     iNext. iRewrite "Heq". iPureIntro. rewrite assoc. f_equiv. by rewrite comm. done.
 Qed.
-- 
GitLab