lifetime logic invariant simplification: no need to have LftBorDead around LftVs

theories/lifetime/model/accessors.v

@@ -59,7 +59,7 @@ Lemma add_vs Pb Pb' P Q Pi κ :
   lft_vs κ (Q ∗ Pb') Pi.
 Proof.
   iIntros "#HEQ Hvs HvsQ". iApply (lft_vs_cons with "[-Hvs] Hvs").
-  iIntros "$ [HQ HPb'] #H†".
+  iIntros "[HQ HPb'] #H†".
   iApply fupd_mask_mono; last iMod ("HvsQ" with "HQ H†") as "HP". set_solver.
   iModIntro. iNext. iRewrite "HEQ". iFrame.
 Qed.

theories/lifetime/model/borrow_sep.v

@@ -30,7 +30,7 @@ Proof.
       as (s' Pb') "(% & #HPbPb' & Hslice & Hbox)"; first solve_ndisj.
     { by rewrite lookup_fmap EQB. }
     iAssert (▷ lft_vs κ' Pb' Pi)%I with "[Hvs]" as "Hvs".
-    { iNext. iApply (lft_vs_cons with "[] Hvs"). iIntros "$ ? _ !>".
+    { iNext. iApply (lft_vs_cons with "[] Hvs"). iIntros "? _ !>".
       by iApply "HPbPb'". }
     iMod (slice_split _ _ true with "Hslice Hbox")
       as (γ1 γ2) "(Hγ1 & Hγ2 & % & Hs1 & Hs2 & Hbox)"; first solve_ndisj.

theories/lifetime/model/creation.v

@@ -40,18 +40,19 @@ Proof.
     as "[Halive Halive']".
   { intros κ'. rewrite elem_of_dom. eauto. }
   iApply fupd_trans. iApply fupd_mask_mono; first by apply union_subseteq_l.
-  iMod ("Hvs" $! I with "[HI Halive Hbox Hbor] HP Hκ") as "(Hinv & HQ & Hcnt')".
-  { rewrite lft_vs_inv_unfold. iFrame. rewrite /lft_bor_dead.
-    iExists (dom _ B), P. rewrite !gset_to_gmap_dom -map_fmap_compose.
-    rewrite (map_fmap_ext _ ((1%Qp,.) ∘ to_agree) B); last naive_solver.
-    iFrame. }
-  rewrite lft_vs_inv_unfold; iDestruct "Hinv" as "(?&HI&Halive)".
+  iMod ("Hvs" $! I with "[HI Halive] HP Hκ") as "(Hinv & HQ & Hcnt')".
+  { rewrite lft_vs_inv_unfold. iFrame. }
+  rewrite lft_vs_inv_unfold; iDestruct "Hinv" as "(HI&Halive)".
   iSpecialize ("Halive'" with "Halive").
   iMod (own_cnt_update_2 with "Hcnt Hcnt'") as "?".
   { apply auth_update_dealloc, (nat_local_update _ _ 0 0); lia. }
   rewrite /Iinv. iFrame "Hdead Halive' HI".
   iModIntro. iMod (lft_inh_kill with "[$Hinh $HQ]"); first set_solver+.
-  iModIntro. rewrite /lft_inv_dead. iExists Q. by iFrame.
+  iModIntro. rewrite /lft_inv_dead. iExists Q. iFrame.
+  rewrite /lft_bor_dead. iExists (dom _ B), P.
+  rewrite !gset_to_gmap_dom -map_fmap_compose.
+  rewrite (map_fmap_ext _ ((1%Qp,.) ∘ to_agree) B); last naive_solver.
+  iFrame.
 Qed.
 
 Lemma lfts_kill (A : gmap atomic_lft _) (I : gmap lft lft_names) (K K' : gset lft) :

theories/lifetime/model/definitions.v

@@ -131,8 +131,7 @@ Section defs.
 
    Definition lft_vs_inv_go (κ : lft) (lft_inv_alive : ∀ κ', κ' ⊂ κ → iProp Σ)
        (I : gmap lft lft_names) : iProp Σ :=
-     (lft_bor_dead κ ∗
-       own_ilft_auth I ∗
+     (own_ilft_auth I ∗
        [∗ set] κ' ∈ dom _ I, ∀ Hκ : κ' ⊂ κ, lft_inv_alive κ' Hκ)%I.
 
    Definition lft_vs_go (κ : lft) (lft_inv_alive : ∀ κ', κ' ⊂ κ → iProp Σ)
@@ -230,7 +229,7 @@ Lemma lft_vs_inv_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → iProp Σ) I n :
   (∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
   lft_vs_inv_go κ f I ≡{n}≡ lft_vs_inv_go κ f' I.
 Proof.
-  intros Hf. apply sep_ne, sep_ne, big_opS_ne=> // κ' _.
+  intros Hf. apply sep_ne, big_opS_ne=> // κ' _.
   by apply forall_ne=> Hκ.
 Qed.
 
@@ -259,7 +258,7 @@ Proof.
   apply (Fix_F_proper _ (λ _, dist n)); auto using lft_inv_alive_go_ne.
 Qed.
 Lemma lft_vs_inv_unfold κ (I : gmap lft lft_names) :
-  lft_vs_inv κ I ⊣⊢ lft_bor_dead κ ∗
+  lft_vs_inv κ I ⊣⊢
     own_ilft_auth I ∗
     [∗ set] κ' ∈ dom _ I, ⌜κ' ⊂ κ⌝ → lft_inv_alive κ'.
 Proof.

theories/lifetime/model/primitive.v

@@ -490,15 +490,15 @@ Proof.
 Qed.
 
 Lemma lft_vs_cons κ Pb Pb' Pi :
-  (lft_bor_dead κ -∗ ▷ Pb'-∗ [†κ] ={↑borN}=∗ lft_bor_dead κ ∗ ▷ Pb) -∗
+  (▷ Pb'-∗ [†κ] ={↑borN}=∗ ▷ Pb) -∗
   lft_vs κ Pb Pi -∗ lft_vs κ Pb' Pi.
 Proof.
   iIntros "Hcons Hvs". rewrite !lft_vs_unfold.
   iDestruct "Hvs" as (n) "[Hn● Hvs]". iExists n. iFrame "Hn●".
   iIntros (I). rewrite {1}lft_vs_inv_unfold.
-  iIntros "(Hdead & Hinv & Hκs) HPb #Hκ†".
-  iMod ("Hcons" with "Hdead HPb Hκ†") as "[Hdead HPb]".
-  iApply ("Hvs" $! I with "[Hdead Hinv Hκs] HPb Hκ†").
+  iIntros "(Hinv & Hκs) HPb #Hκ†".
+  iMod ("Hcons" with "HPb Hκ†") as "HPb".
+  iApply ("Hvs" $! I with "[Hinv Hκs] HPb Hκ†").
   rewrite lft_vs_inv_unfold. by iFrame.
 Qed.
 End primitive.

theories/lifetime/model/reborrow.v

@@ -68,7 +68,7 @@ Proof.
   clear dependent Iinv I.
   iNext. rewrite lft_vs_unfold. iExists (S n). iFrame "Hn●".
   iIntros (I) "Hinv [HP HPb] #Hκ†".
-  rewrite {1}lft_vs_inv_unfold; iDestruct "Hinv" as "(Hκdead' & HI & Hinv)".
+  rewrite {1}lft_vs_inv_unfold; iDestruct "Hinv" as "(HI & Hinv)".
   iDestruct (own_bor_auth with "HI Hi") as %?%(elem_of_dom (D:=gset lft)).
   iDestruct (@big_sepS_delete with "Hinv") as "[Hκalive Hinv]"; first done.
   rewrite lft_inv_alive_unfold.
@@ -85,9 +85,9 @@ Proof.
   { by rewrite lookup_fmap HB. }
   iDestruct (@big_sepM_delete with "HB") as "[Hcnt HB]"; first done.
   rewrite /=. iDestruct "Hcnt" as "[% H1◯]".
-  iMod ("Hvs" $! I with "[Hκdead' HI Hinv Hvs' Hinh HB● Hbox HB]
+  iMod ("Hvs" $! I with "[HI Hinv Hvs' Hinh HB● Hbox HB]
                          [$HPb $Hi] Hκ†") as "($ & $ & Hcnt')".
-  { rewrite lft_vs_inv_unfold. iFrame "Hκdead' HI".
+  { rewrite lft_vs_inv_unfold. iFrame "HI".
     iApply (big_sepS_delete _ (dom (gset lft) I) with "[- $Hinv]"); first done.
     iIntros (_). rewrite lft_inv_alive_unfold.
     iExists Pb', Pi'. iFrame "Hvs' Hinh". rewrite /lft_bor_alive.
@@ -135,7 +135,7 @@ Proof.
   { rewrite /lft_bor_alive (big_sepM_delete _ B i') //. iDestruct "HB" as "[_ HB]".
     iExists (delete i' B). rewrite -fmap_delete. iFrame.
     rewrite fmap_delete -insert_delete delete_insert ?lookup_delete //=. }
-  { iNext. iApply (lft_vs_cons with "[] Hvs"). iIntros "$ [??] _ !>". iNext.
+  { iNext. iApply (lft_vs_cons with "[] Hvs"). iIntros "[??] _ !>". iNext.
     iRewrite "HeqPb'". iFrame. by iApply "HP'". }
   iDestruct "HH" as "([HI Hinvκ] & $ & Halive & Hvs)".
   iApply "Hclose". iExists _, _. iFrame.