Clarify the API of shared borrows: create specific lemmas for lftN.

theories/lifetime/frac_borrow.v

@@ -44,14 +44,14 @@ Section frac_bor.
     iMod (bor_acc_atomic_strong with "LFT Hφ") as "[H|[H† Hclose]]". done.
     - iDestruct "H" as (κ') "(#Hκκ' & Hφ & Hclose)".
       iMod ("Hclose" with "[-] []") as "Hφ"; last first.
-      { iExists γ, κ'. iFrame "#". iApply (bor_share with "Hφ"); auto. }
+      { iExists γ, κ'. iFrame "#". iApply (bor_share_lftN with "Hφ"); auto. }
       { iIntros "!>Hφ H†!>". iNext. iDestruct "Hφ" as (q') "(Hφ & _ & [%|Hκ])". by subst.
         iDestruct "Hκ" as (q'') "[_ Hκ]".
         iDestruct (lft_tok_dead with "Hκ H†") as "[]". }
       iExists 1%Qp. iFrame. eauto.
     - iMod "Hclose" as "_"; last first.
       iExists γ, κ. iSplitR. by iApply lft_incl_refl.
-      iMod (bor_fake with "LFT H†"). done. iApply bor_share; auto.
+      by iApply shr_bor_fake_lftN.
   Qed.
 
   Lemma frac_bor_atomic_acc E κ :
@@ -60,9 +60,9 @@ Section frac_bor.
                                       ∨ [†κ] ∗ |={E∖↑lftN,E}=> True.
   Proof.
     iIntros (?) "#LFT #Hφ". iDestruct "Hφ" as (γ κ') "[Hκκ' Hshr]".
-    iMod (shr_bor_acc with "LFT Hshr") as "[[Hφ Hclose]|[H† Hclose]]"; try done.
+    iMod (shr_bor_acc_lftN with "LFT Hshr") as "[[Hφ Hclose]|[H† Hclose]]"; try done.
     - iLeft. iDestruct "Hφ" as (q) "(Hφ & Hγ & H)". iExists q. iFrame.
-      rewrite difference_twice_L. iIntros "!>Hφ". iApply "Hclose". iExists q. iFrame.
+      iIntros "!>Hφ". iApply "Hclose". iExists q. iFrame.
     - iRight. iMod "Hclose" as "_". iMod (lft_incl_dead with "Hκκ' H†") as "$". done.
       iApply fupd_intro_mask. set_solver. done.
   Qed.

theories/lifetime/shr_borrow.v

@@ -31,12 +31,19 @@ Section shared_bors.
   Global Instance shr_bor_persistent : PersistentP (&shr{κ, N} P) := _.
 
   Lemma bor_share E κ :
-    ↑lftN ⊆ E → N = lftN ∨ N ⊥ lftN → &{κ}P ={E}=∗ &shr{κ, N}P.
+    ↑lftN ⊆ E → N ⊥ lftN → &{κ}P ={E}=∗ &shr{κ, N}P.
   Proof.
     iIntros (? HN) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "(#?&Hown)".
-    iExists i. iFrame "#". destruct HN as [->|HN].
-    - iRight. iSplitR. done. by iMod (inv_alloc with "[Hown]") as "$"; auto.
-    - iLeft. iSplitR. done. by iMod (inv_alloc with "[Hown]") as "$"; auto.
+    iExists i. iFrame "#".
+    iLeft. iSplitR. done. by iMod (inv_alloc with "[Hown]") as "$"; auto.
+  Qed.
+
+  Lemma bor_share_lftN E κ :
+    ↑lftN ⊆ E → &{κ}P ={E}=∗ &shr{κ, lftN}P.
+  Proof.
+    iIntros (?) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "(#?&Hown)".
+    iExists i. iFrame "#". subst.
+    iRight. iSplitR. done. by iMod (inv_alloc with "[Hown]") as "$"; auto.
   Qed.
 
   Lemma shr_bor_acc E κ :
@@ -77,11 +84,24 @@ Section shared_bors.
   Qed.
 
   Lemma shr_bor_fake E κ:
-    ↑lftN ⊆ E → N = lftN ∨ N ⊥ lftN → lft_ctx -∗ [†κ] ={E}=∗ &shr{κ,N}P.
+    ↑lftN ⊆ E → N ⊥ lftN → lft_ctx -∗ [†κ] ={E}=∗ &shr{κ,N}P.
   Proof.
     iIntros (??) "#LFT#H†". iApply (bor_share with ">"); try done.
     by iApply (bor_fake with "LFT H†").
   Qed.
+
+  Lemma shr_bor_fake_lftN E κ:
+    ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &shr{κ,lftN}P.
+  Proof.
+    iIntros (?) "#LFT#H†". iApply (bor_share_lftN with ">"); try done.
+    by iApply (bor_fake with "LFT H†").
+  Qed.
 End shared_bors.
 
+Lemma shr_bor_acc_lftN `{invG Σ, lftG Σ} (P : iProp Σ) E κ :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &shr{κ,lftN}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
+             [†κ] ∗ |={E∖↑lftN,E}=> True.
+Proof. intros. by rewrite (shr_bor_acc _ lftN) // difference_twice_L. Qed.
+
 Typeclasses Opaque shr_bor.