Combining borrows.

iris @ 42cf780a

-Subproject commit 26ae0c67ca3e0dacedb957709c9526e66741e55d
+Subproject commit 42cf780adc3d61438701a106e50e07977c9b6abb

theories/lifetime/borrow.v

@@ -23,7 +23,7 @@ Qed.
 Lemma idx_bor_shorten κ κ' i P : κ ⊑ κ' -∗ &{κ',i} P -∗ &{κ,i} P.
 Proof. unfold idx_bor. iIntros "#Hκκ' [#? $]". by iApply (lft_incl_trans with "Hκκ'"). Qed.
 
-Lemma bor_fake_internal E κ P :
+Lemma raw_bor_fake E κ P :
   ↑borN ⊆ E →
   ▷ lft_bor_dead κ ={E}=∗ ∃ i, ▷ lft_bor_dead κ ∗ raw_bor (κ, i) P.
 Proof.
@@ -51,7 +51,7 @@ Proof.
           ?elem_of_dom // /lfts_inv /lft_inv /lft_inv_dead /lft_alive_in.
   iDestruct "Hinv" as "[[[_ >%]|[Hinv >%]]Hclose']". naive_solver.
   iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
-  iMod (bor_fake_internal with "Hdead") as (i) "[Hdead Hbor]". solve_ndisj.
+  iMod (raw_bor_fake with "Hdead") as (i) "[Hdead Hbor]". solve_ndisj.
   unfold bor. iExists (κ, i). iFrame. rewrite -lft_incl_refl -big_sepS_later.
   iApply "Hclose". iExists _, _. iFrame. iApply "Hclose'". iRight. iFrame "∗%". eauto.
 Qed.
@@ -120,7 +120,7 @@ Proof.
       rewrite to_gmap_union_singleton delete_insert // lookup_to_gmap_None. set_solver.
   - iFrame "HP". iApply fupd_frame_r. iSplitR ""; last by auto.
     iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)" .
-    iMod (bor_fake_internal with "Hdead") as (i) "[Hdead Hbor]". solve_ndisj.
+    iMod (raw_bor_fake with "Hdead") as (i) "[Hdead Hbor]". solve_ndisj.
     unfold bor. iExists (κ, i). iFrame. rewrite -lft_incl_refl -big_sepS_later.
     iApply "Hclose". iExists _, _. iFrame. iApply "Hclose'". iRight. iFrame "∗%". eauto.
 Qed.
@@ -156,7 +156,7 @@ Proof.
           (alloc_singleton_local_update _ γ2 (1%Qp, DecAgree Bor_in)); last done.
         rewrite lookup_insert_ne // /to_borUR -fmap_delete lookup_fmap fmap_None
                 -fmap_None -lookup_fmap fmap_delete //. }
-    rewrite !own_bor_op. iDestruct "Hbor" as "[[H●  H◯2] H◯1]".
+    rewrite !own_bor_op. iDestruct "Hbor" as "[[H● H◯2] H◯1]".
     iAssert (&{κ}P)%I with "[H◯1 Hs1]" as "$".
     { rewrite /bor /raw_bor /idx_bor_own. iExists (κ', γ1). iFrame "∗#". }
     iAssert (&{κ}Q)%I with "[H◯2 Hs2]" as "$".
@@ -169,19 +169,79 @@ Proof.
     + by rewrite -fmap_None -lookup_fmap fmap_delete.
     + by rewrite lookup_insert_ne // -fmap_None -lookup_fmap fmap_delete.
   - iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
-    iMod (bor_fake_internal with "Hdead") as (i1) "[Hdead Hbor1]". solve_ndisj.
-    iMod (bor_fake_internal with "Hdead") as (i2) "[Hdead Hbor2]". solve_ndisj.
+    iMod (raw_bor_fake with "Hdead") as (i1) "[Hdead Hbor1]". solve_ndisj.
+    iMod (raw_bor_fake with "Hdead") as (i2) "[Hdead Hbor2]". solve_ndisj.
     iMod ("Hclose" with "[-Hbor1 Hbor2]") as "_".
     { iExists A, I. iFrame. rewrite big_sepS_later. iApply "Hclose'".
       iRight. iSplit; last by auto. iExists _. iFrame. }
     unfold bor. iSplitL "Hbor1"; iExists (_, _); eauto.
 Qed.
 
-
+Lemma raw_rebor E κ κ' i P :
+  ↑lftN ⊆ E → κ ⊆ κ' →
+  lft_ctx -∗ raw_bor (κ, i) P ={E}=∗
+    ∃ j, raw_bor (κ', j) P ∗ ([†κ'] ={E}=∗ raw_bor (κ, i) P).
+Admitted.
 
 Lemma bor_combine E κ P Q :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P -∗ &{κ} Q ={E}=∗ &{κ} (P ∗ Q).
-Proof. Admitted.
+Proof.
+  iIntros (?) "#Hmgmt HP HQ". rewrite {1 2}/bor.
+  iDestruct "HP" as ([κ1 i1]) "[#Hκ1 Hbor1]".
+  iDestruct "HQ" as ([κ2 i2]) "[#Hκ2 Hbor2]".
+  iMod (raw_rebor _ _ (κ1 ∪ κ2) with "Hmgmt Hbor1") as (j1) "[Hbor1 _]".
+    done. by apply gmultiset_union_subseteq_l.
+  iMod (raw_rebor _ _ (κ1 ∪ κ2) with "Hmgmt Hbor2") as (j2) "[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 "[Hbor1 Hslice1]". iDestruct "Hbor2" as "[Hbor2 Hslice2]".
+  iDestruct (own_bor_auth with "HI Hbor1") as %Hκ'.
+  rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
+          /lfts_inv /lft_inv /lft_inv_dead /lft_alive_in. simpl.
+  iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]] Hclose']".
+  - rewrite lft_inv_alive_unfold /lft_bor_alive.
+    iDestruct "Hinv" as (Pb Pi) "(H & Hvs & Hinh)".
+    iDestruct "H" as (B) "(Hbox & >Hown & HB)".
+    iDestruct (own_bor_valid_2 with "Hown Hbor1")
+        as %[EQB1%to_borUR_included _]%auth_valid_discrete_2.
+    iDestruct (own_bor_valid_2 with "Hown Hbor2")
+        as %[EQB2%to_borUR_included _]%auth_valid_discrete_2.
+    iAssert (⌜j1 ≠ j2⌝)%I with "[#]" as %Hj1j2.
+    { iIntros (->).
+      iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2%auth_valid_discrete.
+      exfalso. revert Hj1j2. rewrite /= op_singleton singleton_valid.
+      compute. tauto. }
+    iMod (box_combine with "Hslice1 Hslice2 Hbox") as (γ) "(% & Hslice & Hbox)".
+      solve_ndisj. done. by rewrite lookup_fmap EQB1. by rewrite lookup_fmap EQB2.
+    iCombine "Hown" "Hbor1" as "Hbor1". iCombine "Hbor1" "Hbor2" as "Hbor".
+    rewrite -!own_bor_op. iMod (own_bor_update with "Hbor") as "Hbor".
+    { etrans; last etrans.
+      - apply cmra_update_op; last done.
+        apply auth_update_dealloc. by apply delete_singleton_local_update, _.
+      - apply auth_update_dealloc. by apply delete_singleton_local_update, _.
+      - apply auth_update_alloc,
+           (alloc_singleton_local_update _ γ (1%Qp, DecAgree Bor_in)); last done.
+        rewrite /to_borUR -!fmap_delete lookup_fmap fmap_None
+                -fmap_None -lookup_fmap !fmap_delete //. }
+    rewrite own_bor_op. iDestruct "Hbor" as "[H● H◯]".
+    iAssert (&{κ}(P ∗ Q))%I with "[H◯ Hslice]" as "$".
+    { rewrite /bor /raw_bor /idx_bor_own. iExists (κ1 ∪ κ2, γ). iFrame.
+      iApply (lft_incl_glb with "Hκ1 Hκ2"). }
+    iApply "Hclose". iExists A, I. iFrame. rewrite big_sepS_later.
+    iApply "Hclose'". iLeft. iFrame "%". iExists Pb, Pi. iFrame. iExists _.
+    rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "Hbox H●".
+    rewrite !big_sepM_insert /=.
+    + rewrite (big_sepM_delete _ _ _ _ EQB1) /=.
+      rewrite (big_sepM_delete _ _ j2 Bor_in) /=. by iDestruct "HB" as "[_ $]".
+      rewrite lookup_delete_ne //.
+    + rewrite -fmap_None -lookup_fmap !fmap_delete //.
+  - iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
+    iMod (raw_bor_fake with "Hdead") as (i) "[Hdead Hbor]". solve_ndisj.
+    iMod ("Hclose" with "[-Hbor]") as "_".
+    { iExists A, I. iFrame. rewrite big_sepS_later. iApply "Hclose'".
+      iRight. iSplit; last by auto. iExists _. iFrame. }
+    unfold bor. iExists (_, _). iFrame. iApply (lft_incl_glb with "Hκ1 Hκ2").
+Qed.
 
 End borrow.
\ No newline at end of file

theories/lifetime/derived.v

@@ -59,21 +59,6 @@ Proof.
   iIntros (?) "#[_ H] Hq". iApply fupd_mask_mono; first done. by iApply "H".
 Qed.
 
-Lemma lft_incl_lb κ κ' κ'' : κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ∪ κ''.
-Proof. (*
-  iIntros "[#[H1 H1†] #[H2 H2†]]!#". iSplitR.
-  - iIntros (q) "[Hκ'1 Hκ'2]".
-    iMod ("H1" with "*Hκ'1") as (q') "[Hκ' Hclose']".
-    iMod ("H2" with "*Hκ'2") as (q'') "[Hκ'' Hclose'']".
-    destruct (Qp_lower_bound q' q'') as (qq & q'0 & q''0 & -> & ->).
-    iExists qq. rewrite -lft_tok_op !lft_tok_frac_op.
-    iDestruct "Hκ'" as "[$ Hκ']". iDestruct "Hκ''" as "[$ Hκ'']".
-    iIntros "!>[Hκ'0 Hκ''0]".
-    iMod ("Hclose'" with "[$Hκ' $Hκ'0]") as "$".
-    by iMod ("Hclose''" with "[$Hκ'' $Hκ''0]") as "$".
-  - rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
-Qed. *) Admitted.
-
 Lemma lft_incl_static κ : (κ ⊑ static)%I.
 Proof.
   iIntros "!#". iSplitR.

theories/lifetime/primitive.v

@@ -263,4 +263,19 @@ Proof.
   - iIntros "H†". iMod ("H2†" with "H†"). by iApply "H1†".
 Qed.
 
+Lemma lft_incl_glb κ κ' κ'' : κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ∪ κ''.
+Proof. (*
+  iIntros "[#[H1 H1†] #[H2 H2†]]!#". iSplitR.
+  - iIntros (q) "[Hκ'1 Hκ'2]".
+    iMod ("H1" with "*Hκ'1") as (q') "[Hκ' Hclose']".
+    iMod ("H2" with "*Hκ'2") as (q'') "[Hκ'' Hclose'']".
+    destruct (Qp_lower_bound q' q'') as (qq & q'0 & q''0 & -> & ->).
+    iExists qq. rewrite -lft_tok_op !lft_tok_frac_op.
+    iDestruct "Hκ'" as "[$ Hκ']". iDestruct "Hκ''" as "[$ Hκ'']".
+    iIntros "!>[Hκ'0 Hκ''0]".
+    iMod ("Hclose'" with "[$Hκ' $Hκ'0]") as "$".
+    by iMod ("Hclose''" with "[$Hκ'' $Hκ''0]") as "$".
+  - rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
+Qed. *) Admitted.
+
 End primitive.