Change the masks of shared borrows, so that the previous commit has a purpose.

This requires using a different invariant in the case N ⊥ lftN. Hence, we add the side condition that (N = lftN ∨ N ⊥ lftN). This is not particularly pretty : the alternative would be to have two different kinds of shared borrows.

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φ"). done. }
+      { iExists γ, κ'. iFrame "#". iApply (bor_share 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. by iApply bor_share.
+      iMod (bor_fake with "LFT H†"). done. iApply bor_share; auto.
   Qed.
 
   Lemma frac_bor_atomic_acc E κ :
@@ -62,7 +62,7 @@ Section frac_bor.
     iIntros (?) "#LFT #Hφ". iDestruct "Hφ" as (γ κ') "[Hκκ' Hshr]".
     iMod (shr_bor_acc with "LFT Hshr") as "[[Hφ Hclose]|[H† Hclose]]"; try done.
     - iLeft. iDestruct "Hφ" as (q) "(Hφ & Hγ & H)". iExists q. iFrame.
-      iIntros "!>Hφ". iApply "Hclose". iExists q. iFrame.
+      rewrite difference_twice_L. 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

@@ -4,9 +4,11 @@ From lrust.lifetime Require Export lifetime.
 Set Default Proof Using "Type".
 
 (** Shared bors  *)
-(* TODO : update the TEX with the fact that we can chose the namespace. *)
+(* TODO : update the TEX with the fact that we can choose the namespace. *)
 Definition shr_bor `{invG Σ, lftG Σ} κ N (P : iProp Σ) :=
-  (∃ i, &{κ,i}P ∗ inv N (∃ q, idx_bor_own q i))%I.
+  (∃ i, &{κ,i}P ∗
+    (⌜N ⊥ lftN⌝ ∗ inv N (idx_bor_own 1 i) ∨
+     ⌜N = lftN⌝ ∗ inv N (∃ q, idx_bor_own q i)))%I.
 Notation "&shr{ κ , N } P" := (shr_bor κ N P)
   (format "&shr{ κ , N }  P", at level 20, right associativity) : uPred_scope.
 
@@ -28,33 +30,44 @@ Section shared_bors.
 
   Global Instance shr_bor_persistent : PersistentP (&shr{κ, N} P) := _.
 
-  Lemma bor_share E κ : ↑lftN ⊆ E → &{κ}P ={E}=∗ &shr{κ, N}P.
+  Lemma bor_share E κ :
+    ↑lftN ⊆ E → N = lftN ∨ N ⊥ lftN → &{κ}P ={E}=∗ &shr{κ, N}P.
   Proof.
-    iIntros (?) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "(#?&Hown)".
-    iExists i. iFrame "#". iApply inv_alloc. auto.
+    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.
   Qed.
 
   Lemma shr_bor_acc E κ :
     ↑lftN ⊆ E → ↑N ⊆ E →
-    lft_ctx -∗ &shr{κ,N}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
-               [†κ] ∗ |={E∖↑lftN,E}=> True.
+    lft_ctx -∗ &shr{κ,N}P ={E,E∖↑N∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑N∖↑lftN,E}=∗ True) ∨
+               [†κ] ∗ |={E∖↑N∖↑lftN,E}=> True.
   Proof.
-    iIntros (??) "#LFT #HP". iDestruct "HP" as (i) "(#Hidx&#Hinv)".
-    iInv N as (q') ">[Hq'0 Hq'1]" "Hclose".
-    iMod ("Hclose" with "[Hq'1]") as "_". by eauto.
-    iMod (idx_bor_atomic_acc with "LFT Hidx Hq'0") as "[[HP Hclose]|[H† Hclose]]". done.
-    - iLeft. iFrame. iIntros "!>HP". by iMod ("Hclose" with "HP").
-    - iRight. iFrame. iIntros "!>". by iMod "Hclose".
+    iIntros (??) "#LFT #HP". iDestruct "HP" as (i) "#[Hidx [[% Hinv]|[% Hinv]]]".
+    - iInv N as ">Hi" "Hclose". iMod (idx_bor_atomic_acc with "LFT Hidx Hi")
+        as "[[HP Hclose']|[H† Hclose']]". solve_ndisj.
+      + iLeft. iFrame. iIntros "!>HP". iMod ("Hclose'" with "HP"). by iApply "Hclose".
+      + iRight. iFrame. iIntros "!>". iMod "Hclose'". by iApply "Hclose".
+    - subst. rewrite difference_twice_L. iInv lftN as (q') ">[Hq'0 Hq'1]" "Hclose".
+      iMod ("Hclose" with "[Hq'1]") as "_". by eauto.
+      iMod (idx_bor_atomic_acc with "LFT Hidx Hq'0") as "[[HP Hclose]|[H† Hclose]]". done.
+      + iLeft. iFrame. iIntros "!>HP". by iMod ("Hclose" with "HP").
+      + iRight. iFrame. iIntros "!>". by iMod "Hclose".
   Qed.
 
   Lemma shr_bor_acc_tok E q κ :
     ↑lftN ⊆ E → ↑N ⊆ E →
-    lft_ctx -∗ &shr{κ,N}P -∗ q.[κ] ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ q.[κ]).
+    lft_ctx -∗ &shr{κ,N}P -∗ q.[κ] ={E,E∖↑N}=∗ ▷P ∗ (▷P ={E∖↑N,E}=∗ q.[κ]).
   Proof.
-    iIntros (??) "#LFT #Hshr Hκ".
-    iMod (shr_bor_acc with "LFT Hshr") as "[[$ Hclose]|[H† _]]"; try done.
-    - iIntros "!>HP". by iMod ("Hclose" with "HP").
-    - iDestruct (lft_tok_dead with "Hκ H†") as "[]".
+    iIntros (??) "#LFT #HP Hκ". iDestruct "HP" as (i) "#[Hidx [[% Hinv]|[% Hinv]]]".
+    - iInv N as ">Hi" "Hclose".
+      iMod (idx_bor_acc with "LFT Hidx Hi Hκ") as "[$ Hclose']". solve_ndisj.
+      iIntros "!> H". iMod ("Hclose'" with "H") as "[? $]". by iApply "Hclose".
+    - iMod (shr_bor_acc with "LFT []") as "[[$ Hclose]|[H† _]]"; try done.
+      + iExists i. auto.
+      + subst. rewrite difference_twice_L. iIntros "!>HP". by iMod ("Hclose" with "HP").
+      + iDestruct (lft_tok_dead with "Hκ H†") as "[]".
   Qed.
 
   Lemma shr_bor_shorten κ κ': κ ⊑ κ' -∗ &shr{κ',N}P -∗ &shr{κ,N}P.
@@ -63,9 +76,10 @@ Section shared_bors.
       by iApply (idx_bor_shorten with "H⊑").
   Qed.
 
-  Lemma shr_bor_fake E κ: ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &shr{κ,N}P.
+  Lemma shr_bor_fake E κ:
+    ↑lftN ⊆ E → N = lftN ∨ N ⊥ lftN → lft_ctx -∗ [†κ] ={E}=∗ &shr{κ,N}P.
   Proof.
-    iIntros (?) "#LFT#H†". iApply (bor_share with ">"). done.
+    iIntros (??) "#LFT#H†". iApply (bor_share with ">"); try done.
     by iApply (bor_fake with "LFT H†").
   Qed.
 End shared_bors.