From ae3a4b2d2b5fcf7136cf168013d1a77bc8ed29e7 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 2 Aug 2017 22:34:07 +0200
Subject: [PATCH] Cleaning up the lifetime logic.

---
 theories/lifetime/lifetime.v        | 15 +++++++++++++++
 theories/lifetime/lifetime_sig.v    | 13 ++++---------
 theories/lifetime/model/accessors.v | 16 ----------------
 3 files changed, 19 insertions(+), 25 deletions(-)

diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index e5cbde2a..b2b78797 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -26,6 +26,21 @@ Section derived.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
+Lemma bor_acc_atomic_cons E κ P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
+    (▷ P ∗ ∀ Q, ▷ (▷ Q ={∅}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ} Q) ∨
+    ([†κ] ∗ |={E∖↑lftN,E}=> True).
+Proof.
+  iIntros (?) "#LFT HP".
+  iMod (bor_acc_atomic_strong with "LFT HP") as "[H|[??]]"; first done.
+  - iLeft. iDestruct "H" as (κ') "(#Hκκ' & $ & Hclose)". iIntros "!>* HPQ HQ".
+    iMod ("Hclose" with "[HPQ] HQ") as "Hb".
+    + iNext. iIntros "? _". by iApply "HPQ".
+    + iApply (bor_shorten with "Hκκ' Hb").
+  - iRight. by iFrame.
+Qed.
+
 Lemma bor_acc_atomic E κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ}P ={E,E∖↑lftN}=∗
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index f2dd298f..0492383b 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -62,12 +62,12 @@ Module Type lifetime_sig.
   Global Declare Instance lft_intersect_right_id : RightId eq static lft_intersect.
 
   Global Declare Instance lft_ctx_persistent : PersistentP lft_ctx.
-  Global Declare Instance lft_dead_persistent κ : PersistentP (lft_dead κ).
+  Global Declare Instance lft_dead_persistent κ : PersistentP ([†κ]).
   Global Declare Instance lft_incl_persistent κ κ' : PersistentP (κ ⊑ κ').
-  Global Declare Instance idx_bor_persistent κ i P : PersistentP (idx_bor κ i P).
+  Global Declare Instance idx_bor_persistent κ i P : PersistentP (&{κ,i} P).
 
-  Global Declare Instance lft_tok_timeless q κ : TimelessP (lft_tok q κ).
-  Global Declare Instance lft_dead_timeless κ : TimelessP (lft_dead κ).
+  Global Declare Instance lft_tok_timeless q κ : TimelessP (q.[κ]).
+  Global Declare Instance lft_dead_timeless κ : TimelessP ([†κ]).
   Global Declare Instance idx_bor_own_timeless q i : TimelessP (idx_bor_own q i).
 
   Global Instance idx_bor_params : Params (@idx_bor) 5.
@@ -151,11 +151,6 @@ Module Type lifetime_sig.
     □ ((∀ q, lft_tok q κ ={↑lftN}=∗ ∃ q',
                  lft_tok q' κ' ∗ (lft_tok q' κ' ={↑lftN}=∗ lft_tok q κ)) ∗
         (lft_dead κ' ={↑lftN}=∗ lft_dead κ)) -∗ κ ⊑ κ'.
-  (* Same for some of the derived lemmas. *)
-  Parameter bor_acc_atomic_cons : ∀ E κ P,
-    ↑lftN ⊆ E → lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
-      (▷ P ∗ ∀ Q, ▷ (▷ Q ={∅}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ} Q) ∨
-      ([†κ] ∗ |={E∖↑lftN,E}=> True).
 
   End properties.
 
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 053a65ce..1dbe1206 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -262,20 +262,4 @@ Proof.
     + iMod (lft_incl_dead with "Hle H†") as "$". done.
       iApply fupd_intro_mask'. solve_ndisj.
 Qed.
-
-(* These derived lemmas are needed inside the model. *)
-Lemma bor_acc_atomic_cons E κ P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
-    (▷ P ∗ ∀ Q, ▷ (▷ Q ={∅}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ} Q) ∨
-    ([†κ] ∗ |={E∖↑lftN,E}=> True).
-Proof.
-  iIntros (?) "#LFT HP".
-  iMod (bor_acc_atomic_strong with "LFT HP") as "[H|[??]]"; first done.
-  - iLeft. iDestruct "H" as (κ') "(#Hκκ' & $ & Hclose)". iIntros "!>* HPQ HQ".
-    iMod ("Hclose" with "[HPQ] HQ") as "Hb".
-    + iNext. iIntros "? _". by iApply "HPQ".
-    + iApply (bor_shorten with "Hκκ' Hb").
-  - iRight. by iFrame.
-Qed.
 End accessors.
-- 
GitLab