From 3401f1b3277cf50b8eca08465cf64b8ceb1a540a Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sun, 27 Nov 2016 15:48:49 +0100
Subject: [PATCH] Clarify dependencies. Rename todo.v -> accessors.v

---
 _CoqProject                               |  2 +-
 theories/lifetime/{todo.v => accessors.v} |  4 ++--
 theories/lifetime/borrow.v                | 24 +-------------------
 theories/lifetime/derived.v               |  2 +-
 theories/lifetime/rebor.v                 | 27 ++++++++++++++++++++++-
 theories/typing/perm.v                    |  2 +-
 theories/typing/perm_incl.v               |  2 +-
 theories/typing/type.v                    |  2 +-
 theories/typing/type_incl.v               |  2 +-
 theories/typing/typing.v                  |  2 +-
 10 files changed, 36 insertions(+), 33 deletions(-)
 rename theories/lifetime/{todo.v => accessors.v} (97%)

diff --git a/_CoqProject b/_CoqProject
index 67a059fc..99d284ab 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -4,7 +4,7 @@ theories/lifetime/definitions.v
 theories/lifetime/derived.v
 theories/lifetime/creation.v
 theories/lifetime/primitive.v
-theories/lifetime/todo.v
+theories/lifetime/accessors.v
 theories/lifetime/borrow.v
 theories/lifetime/rebor.v
 theories/lifetime/shr_borrow.v
diff --git a/theories/lifetime/todo.v b/theories/lifetime/accessors.v
similarity index 97%
rename from theories/lifetime/todo.v
rename to theories/lifetime/accessors.v
index b04360b6..3c74848b 100644
--- a/theories/lifetime/todo.v
+++ b/theories/lifetime/accessors.v
@@ -1,6 +1,6 @@
 From lrust.lifetime Require Export definitions.
 
-Section todo.
+Section accessors.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
@@ -31,4 +31,4 @@ Lemma idx_bor_atomic_acc E q κ i P :
               [†κ] ∗ (|={E∖↑lftN,E}=> idx_bor_own q i).
 Proof. Admitted.
 
-End todo.
\ No newline at end of file
+End accessors.
\ No newline at end of file
diff --git a/theories/lifetime/borrow.v b/theories/lifetime/borrow.v
index 2cfa33a7..239a0e22 100644
--- a/theories/lifetime/borrow.v
+++ b/theories/lifetime/borrow.v
@@ -1,4 +1,4 @@
-From lrust.lifetime Require Export primitive creation.
+From lrust.lifetime Require Export primitive creation rebor.
 From iris.algebra Require Import csum auth frac gmap dec_agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
@@ -23,22 +23,6 @@ Qed.
 Lemma idx_bor_shorten κ κ' i P : κ ⊑ κ' -∗ &{κ',i} P -∗ &{κ,i} P.
 Proof. unfold idx_bor. iIntros "#Hκκ' [#? $]". by iApply (lft_incl_trans with "Hκκ'"). Qed.
 
-Lemma raw_bor_fake E κ P :
-  ↑borN ⊆ E →
-  ▷ lft_bor_dead κ ={E}=∗ ∃ i, ▷ lft_bor_dead κ ∗ raw_bor (κ, i) 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 (own_bor_update with "Hown") as "Hown".
-  { apply auth_update_alloc.
-    apply: (alloc_local_update _ _ _ (1%Qp, DecAgree Bor_in)); last done.
-    do 2 eapply lookup_to_gmap_None. by eauto. }
-  rewrite own_bor_op insert_empty /bor /raw_bor /idx_bor_own. iExists _.
-  iDestruct "Hown" as "[H● H◯]". iSplitL "H● Hbox"; last by eauto.
-  iExists _, _. rewrite -!to_gmap_union_singleton. by iFrame.
-Qed.
-
 Lemma bor_fake E κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
@@ -177,12 +161,6 @@ Proof.
     unfold bor. iSplitL "Hbor1"; iExists (_, _); eauto.
 Qed.
 
-Lemma raw_rebor E κ κ' i P :
-  ↑lftN ⊆ E → κ ⊆ κ' →
-  lft_ctx -∗ raw_bor (κ, i) P ={E}=∗
-    ∃ j, raw_bor (κ', j) P ∗ ([†κ'] ={E}=∗ raw_bor (κ, i) P).
-Admitted.
-
 Lemma bor_combine E κ P Q :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P -∗ &{κ} Q ={E}=∗ &{κ} (P ∗ Q).
diff --git a/theories/lifetime/derived.v b/theories/lifetime/derived.v
index e3262300..263a0af2 100644
--- a/theories/lifetime/derived.v
+++ b/theories/lifetime/derived.v
@@ -1,4 +1,4 @@
-From lrust.lifetime Require Export primitive borrow todo.
+From lrust.lifetime Require Export primitive borrow accessors rebor.
 From iris.proofmode Require Import tactics.
 
 Section derived.
diff --git a/theories/lifetime/rebor.v b/theories/lifetime/rebor.v
index 7fe8f7e7..410d07a6 100644
--- a/theories/lifetime/rebor.v
+++ b/theories/lifetime/rebor.v
@@ -1,4 +1,4 @@
-From lrust.lifetime Require Export primitive (* borrow *).
+From lrust.lifetime Require Export primitive.
 From iris.algebra Require Import csum auth frac gmap dec_agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
@@ -12,6 +12,22 @@ Section rebor.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
+Lemma raw_bor_fake E κ P :
+  ↑borN ⊆ E →
+  ▷ lft_bor_dead κ ={E}=∗ ∃ i, ▷ lft_bor_dead κ ∗ raw_bor (κ, i) 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 (own_bor_update with "Hown") as "Hown".
+  { apply auth_update_alloc.
+    apply: (alloc_local_update _ _ _ (1%Qp, DecAgree Bor_in)); last done.
+    do 2 eapply lookup_to_gmap_None. by eauto. }
+  rewrite own_bor_op insert_empty /bor /raw_bor /idx_bor_own. iExists _.
+  iDestruct "Hown" as "[H● H◯]". iSplitL "H● Hbox"; last by eauto.
+  iExists _, _. rewrite -!to_gmap_union_singleton. by iFrame.
+Qed.
+
 Lemma raw_bor_unnest A I Pb Pi P κ κ' i :
   let Iinv := (
     own_ilft_auth I ∗
@@ -115,6 +131,13 @@ admit.
 
 Admitted.
 
+
+Lemma raw_rebor E κ κ' i P :
+  ↑lftN ⊆ E → κ ⊆ κ' →
+  lft_ctx -∗ raw_bor (κ, i) P ={E}=∗
+    ∃ j, raw_bor (κ', j) P ∗ ([†κ'] ={E}=∗ raw_bor (κ, i) P).
+Admitted.
+
 Lemma bor_rebor' E κ κ' P :
   ↑lftN ⊆ E → κ ⊆ κ' →
   lft_ctx -∗ &{κ} P ={E}=∗ &{κ'} P ∗ ([†κ'] ={E}=∗ &{κ} P).
@@ -131,8 +154,10 @@ Proof.
 Qed.
 *)
 Admitted.
+
 Lemma bor_unnest E κ κ' P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ∪ κ'} P.
 Proof. Admitted.
+
 End rebor.
diff --git a/theories/typing/perm.v b/theories/typing/perm.v
index 4f0b536a..7e88e51a 100644
--- a/theories/typing/perm.v
+++ b/theories/typing/perm.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
 From lrust.lang Require Export proofmode.
-From lrust.lifetime Require Import derived.
+From lrust.lifetime Require Import frac_borrow.
 
 Delimit Scope perm_scope with P.
 Bind Scope perm_scope with perm.
diff --git a/theories/typing/perm_incl.v b/theories/typing/perm_incl.v
index 15ed02de..8791ec05 100644
--- a/theories/typing/perm_incl.v
+++ b/theories/typing/perm_incl.v
@@ -1,7 +1,7 @@
 From Coq Require Import Qcanon.
 From iris.base_logic Require Import big_op.
 From lrust.typing Require Export type perm.
-From lrust.lifetime Require Import frac_borrow rebor.
+From lrust.lifetime Require Import frac_borrow.
 
 Import Perm Types.
 
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 07430ccb..2f7e5ea8 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -3,7 +3,7 @@ From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Export thread_local.
 From iris.program_logic Require Import hoare.
 From lrust.lang Require Export heap notation.
-From lrust.lifetime Require Import frac_borrow rebor.
+From lrust.lifetime Require Import frac_borrow.
 
 Class iris_typeG Σ := Iris_typeG {
   type_heapG :> heapG Σ;
diff --git a/theories/typing/type_incl.v b/theories/typing/type_incl.v
index efe320a0..060c52bc 100644
--- a/theories/typing/type_incl.v
+++ b/theories/typing/type_incl.v
@@ -1,7 +1,7 @@
 From iris.base_logic Require Import big_op.
 From iris.program_logic Require Import hoare.
 From lrust.typing Require Export type perm_incl.
-From lrust.lifetime Require Import derived frac_borrow.
+From lrust.lifetime Require Import frac_borrow.
 
 Import Types.
 
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index 28e6e81c..f9d40637 100644
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -3,7 +3,7 @@ From iris.base_logic Require Import big_op.
 From lrust.lang Require Export notation memcpy.
 From lrust.typing Require Export type perm.
 From lrust Require Import typing.perm_incl lang.proofmode.
-From lrust.lifetime Require Import frac_borrow rebor.
+From lrust.lifetime Require Import frac_borrow.
 
 Import Types Perm.
 
-- 
GitLab