The inheritance of raw reborrowing is not (no longer) necessary. Let's remove...

The inheritance of raw reborrowing is not (no longer) necessary. Let's remove it and call it shorten.

theories/lifetime/model/borrow_sep.v

@@ -78,9 +78,9 @@ Lemma bor_combine E κ P Q :
 Proof.
   iIntros (?) "#LFT HP HQ". rewrite {1 2}/bor.
   iDestruct "HP" as (κ1) "[#Hκ1 Hbor1]". iDestruct "HQ" as (κ2) "[#Hκ2 Hbor2]".
-  iMod (raw_rebor _ _ (κ1 ⊓ κ2) with "LFT Hbor1") as "[Hbor1 _]".
+  iMod (raw_bor_shorten _ _ (κ1 ⊓ κ2) with "LFT Hbor1") as "Hbor1".
     done. by apply gmultiset_union_subseteq_l.
-  iMod (raw_rebor _ _ (κ1 ⊓ κ2) with "LFT Hbor2") as "[Hbor2 _]".
+  iMod (raw_bor_shorten _ _ (κ1 ⊓ κ2) with "LFT Hbor2") as "Hbor2".
     done. by apply gmultiset_union_subseteq_r.
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose". unfold raw_bor, idx_bor_own.
   iDestruct "Hbor1" as (j1) "[Hbor1 Hslice1]". iDestruct "Hbor2" as (j2) "[Hbor2 Hslice2]".

theories/lifetime/model/creation.v

@@ -138,7 +138,7 @@ Proof.
   pose (K := kill_set I Λ).
   pose (K' := filter (lft_alive_in A) (dom (gset lft) I) ∖ K).
   destruct (proj1 (subseteq_disjoint_union_L (K ∪ K') (dom (gset lft) I))) as (K''&HI&HK'').
-  { set_solver. }
+  { set_solver+. }
   assert (K ⊥ K') by set_solver+.
   rewrite HI !big_sepS_union //. iDestruct "Hinv" as "[[HinvK HinvD] Hinv]".
   iAssert ([∗ set] κ ∈ K', lft_inv_alive κ)%I with "[HinvD]" as "HinvD".

theories/lifetime/model/reborrow.v

@@ -60,10 +60,8 @@ Proof.
   { apply auth_update_alloc,
      (alloc_singleton_local_update _ j (1%Qp, to_agree Bor_in)); last done.
     rewrite /to_borUR lookup_fmap. by rewrite HBj. }
-  iModIntro. iExists (P ∗ Pb)%  I. rewrite /Iinv. iFrame "HI". iFrame.
-  iSplitL "Hj".
-  { rewrite /raw_bor /idx_bor_own. iExists j. iFrame. iExists P.
-    rewrite -uPred.iff_refl. auto. }
+  iModIntro. iExists (P ∗ Pb)%  I. rewrite /Iinv. iFrame "HI Hκ". iSplitL "Hj".
+  { iExists j. iFrame. iExists P. rewrite -uPred.iff_refl. auto. }
   iSplitL "Hbox HB● HB".
   { rewrite /lft_bor_alive. iNext. iExists (<[j:=Bor_in]> B).
     rewrite /to_borUR !fmap_insert big_sepM_insert //. iFrame.
@@ -75,7 +73,7 @@ Proof.
   iDestruct (own_bor_auth with "HI Hi") as %?%elem_of_dom.
   iDestruct (@big_sepS_delete with "Hinv") as "[Hκalive Hinv]"; first done.
   rewrite lft_inv_alive_unfold.
-  iDestruct ("Hκalive" with "[%]") as (Pb' Pi') "(Hκalive&Hvs'&Hinh)"; first done.
+  iDestruct ("Hκalive" with "[//]") as (Pb' Pi') "(Hκalive&Hvs'&Hinh)".
   rewrite /lft_bor_alive; iDestruct "Hκalive" as (B') "(Hbox & HB● & HB)".
   iDestruct (own_bor_valid_2 with "HB● Hi")
     as %[HB%to_borUR_included _]%auth_valid_discrete_2.
@@ -89,14 +87,13 @@ Proof.
   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]
-                         [$HPb Hi] Hκ†") as "($ & $ & Hcnt')".
+                         [$HPb $Hi] Hκ†") as "($ & $ & Hcnt')".
   { rewrite lft_vs_inv_unfold. iFrame "Hκdead' 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.
     iExists (<[i:=Bor_in]>B'). rewrite /to_borUR !fmap_insert. iFrame.
     rewrite -insert_delete big_sepM_insert ?lookup_delete //=. by iFrame. }
-  { rewrite /raw_bor /idx_bor_own /=. auto. }
   iModIntro. rewrite -[S n]Nat.add_1_l -nat_op_plus auth_frag_op own_cnt_op.
   by iFrame.
 Qed.
@@ -149,19 +146,16 @@ Proof.
   rewrite /lft_inv lft_inv_alive_unfold. auto 10 with iFrame.
 Qed.
 
-Lemma raw_rebor E κ κ' P :
+Lemma raw_bor_shorten E κ κ' P :
   ↑lftN ⊆ E → κ ⊆ κ' →
-  lft_ctx -∗ raw_bor κ P ={E}=∗ raw_bor κ' P ∗ ([†κ'] ={E}=∗ raw_bor κ P).
+  lft_ctx -∗ raw_bor κ P ={E}=∗ raw_bor κ' P.
 Proof.
   iIntros (? Hκκ') "#LFT Hbor".
-  destruct (decide (κ = κ')) as [<-|Hκneq].
-  { iFrame. iIntros "!> H†". by iApply raw_bor_fake'. }
+  destruct (decide (κ = κ')) as [<-|Hκneq]; [by iFrame|].
   assert (κ ⊂ κ') by (by apply strict_spec_alt).
   rewrite [_ κ P]/raw_bor. iDestruct "Hbor" as (s) "[Hbor Hs]".
   iDestruct "Hs" as (P') "[#HP'P #Hs]".
-  iMod (raw_bor_create _ κ' with "LFT Hbor") as "[Hbor Hinh]"; first done.
-  iSplitR "Hinh"; first last.
-  { iIntros "!> #H†". iExists _. iMod ("Hinh" with "H†") as ">$". auto with iFrame. }
+  iMod (raw_bor_create _ κ' with "LFT Hbor") as "[Hbor _]"; [done|].
   iApply (raw_bor_iff with "HP'P"). by iApply raw_idx_bor_unnest.
 Qed.
 
@@ -180,7 +174,7 @@ Proof.
       iApply lft_intersect_incl_l. }
   rewrite /idx_bor /bor. destruct i as [κ0 i].
   iDestruct "HP" as "[Hκκ0 HP]". iDestruct "HP" as (P') "[HPP' HP']".
-  iMod (raw_rebor _ _ (κ0 ⊓ κ'0) with "LFT Hbor") as "[Hbor _]";
+  iMod (raw_bor_shorten _ _ (κ0 ⊓ κ'0) with "LFT Hbor") as "Hbor";
     [done|by apply gmultiset_union_subseteq_r|].
   iMod (raw_idx_bor_unnest with "LFT HP' Hbor") as "Hbor";
     [done|by apply gmultiset_union_subset_l|].