From 6dd63e3a653b37123f178e4912a44d635e4cc8c0 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 25 Nov 2016 12:29:14 +0100
Subject: [PATCH] Update wrt iris new boxes. Starting spliting/combining
 borrows.

---
 iris                         |  2 +-
 theories/lifetime/borrow.v   | 23 ++++++++++++++++-------
 theories/lifetime/creation.v |  2 +-
 theories/lifetime/todo.v     |  9 ---------
 4 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/iris b/iris
index ff96075a..513b8d85 160000
--- a/iris
+++ b/iris
@@ -1 +1 @@
-Subproject commit ff96075aa1472b1c3b0cfee87cc4ffb06e0f1e2b
+Subproject commit 513b8d852bf398ca0acfa2e02ed327507c9d2ff0
diff --git a/theories/lifetime/borrow.v b/theories/lifetime/borrow.v
index cacfa5ee..a690f466 100644
--- a/theories/lifetime/borrow.v
+++ b/theories/lifetime/borrow.v
@@ -14,7 +14,7 @@ Lemma bor_fake_internal E κ P :
 Proof.
   iIntros (?) "Hdead". rewrite /lft_bor_dead.
   iDestruct "Hdead" as (B Pinh) "[>Hown Hbox]".
-  iMod (box_insert_empty _ _ _ _ P with "Hbox") as (γ) "(% & Hslice & Hbox)".
+  iMod (box_insert_empty _ P with "Hbox") as (γ) "(% & Hslice & Hbox)".
   iMod (own_bor_update with "Hown") as "Hown".
   { apply auth_update_alloc.
     apply: (alloc_local_update _ _ _ (1%Qp, DecAgree Bor_in)); last done.
@@ -57,10 +57,10 @@ Proof.
     iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
     iDestruct "Halive" as (B) "(HboxB & >HownB & HB)".
     iDestruct "Hinh" as (PE) "[>HownE HboxE]".
-    iMod (box_insert_full _ _ _ _ P with "[$HboxB $HP]")
-      as (γB) "(HBlookup & HsliceB & HboxB)". by solve_ndisj.
+    iMod (box_insert_full with "HP HboxB") as (γB) "(HBlookup & HsliceB & HboxB)".
+      by solve_ndisj.
     rewrite lookup_fmap. iDestruct "HBlookup" as %HBlookup.
-    iMod (box_insert_empty _ _ _ _ P with "HboxE") as (γE) "(% & HsliceE & HboxE)".
+    iMod (box_insert_empty _ P with "HboxE") as (γE) "(% & HsliceE & HboxE)".
     rewrite -(fmap_insert bor_filled _ _ Bor_in) -to_gmap_union_singleton.
     iMod (own_bor_update with "HownB") as "HownB".
     { apply auth_update_alloc.
@@ -99,10 +99,9 @@ Proof.
       rewrite <-elem_of_subseteq_singleton in Hle.
       iMod (own_inh_update with "[HE◯ Hinh]") as "HE●"; [|iApply own_inh_op; by iFrame|].
       { apply auth_update_dealloc, gset_disj_dealloc_local_update. }
-      iMod (box_delete_full with "[$HsliceE $Hbox]") as "[$ Hbox]".
+      iMod (box_delete_full with "HsliceE Hbox") as (Pinh') "($ & _ & Hbox)".
         solve_ndisj. by rewrite lookup_to_gmap_Some.
-      iDestruct "Hbox" as (Pinh') "[_ Hbox]". iApply "Hclose".
-      iExists _, _. iFrame. iNext. iApply "Hclose'". iRight. iFrame "%".
+      iApply "Hclose". iExists _, _. iFrame. iNext. iApply "Hclose'". iRight. iFrame "%".
       iExists _. iFrame. iExists _. iFrame.
       rewrite {1}(union_difference_L {[γE]} ESlices); last set_solver.
       rewrite to_gmap_union_singleton delete_insert // lookup_to_gmap_None. set_solver.
@@ -113,4 +112,14 @@ Proof.
     iFrame. iMod ("Hclose" with "[-]") as "_"; last by auto. iExists _, _. by iFrame.
 Qed.
 
+Lemma bor_sep E κ P Q :
+  ↑lftN ⊆ E →
+  lft_ctx ⊢ &{κ} (P ∗ Q) ={E}=∗ &{κ} P ∗ &{κ} Q.
+Proof.
+Admitted.
+Lemma bor_combine E κ P Q :
+  ↑lftN ⊆ E →
+  lft_ctx ⊢ &{κ} P -∗ &{κ} Q ={E}=∗ &{κ} (P ∗ Q).
+Proof. Admitted.
+
 End borrow.
\ No newline at end of file
diff --git a/theories/lifetime/creation.v b/theories/lifetime/creation.v
index 1f8c1ee8..8ea552ff 100644
--- a/theories/lifetime/creation.v
+++ b/theories/lifetime/creation.v
@@ -15,7 +15,7 @@ Lemma lft_inh_kill E κ Q :
 Proof.
   rewrite /lft_inh. iIntros (?) "[Hinh HQ]".
   iDestruct "Hinh" as (E') "[Hinh Hbox]".
-  iMod (box_fill_all with "[$Hbox $HQ]") as "?"=>//.
+  iMod (box_fill_all with "Hbox HQ") as "?"=>//.
   rewrite fmap_to_gmap. iModIntro. iExists E'. by iFrame.
 Qed.
 
diff --git a/theories/lifetime/todo.v b/theories/lifetime/todo.v
index 5d60fea4..ac0911a6 100644
--- a/theories/lifetime/todo.v
+++ b/theories/lifetime/todo.v
@@ -5,15 +5,6 @@ Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
 (** Basic borrows  *)
-Lemma bor_sep E κ P Q :
-  ↑lftN ⊆ E →
-  lft_ctx ⊢ &{κ} (P ∗ Q) ={E}=∗ &{κ} P ∗ &{κ} Q.
-Proof.
-Admitted.
-Lemma bor_combine E κ P Q :
-  ↑lftN ⊆ E →
-  lft_ctx ⊢ &{κ} P -∗ &{κ} Q ={E}=∗ &{κ} (P ∗ Q).
-Proof. Admitted.
 Lemma bor_acc_strong E q κ P :
   ↑lftN ⊆ E →
   lft_ctx ⊢ &{κ} P -∗ q.[κ] ={E}=∗ ▷ P ∗
-- 
GitLab