From a62f5782f7a4f3700818823274778bb268e039bb Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Mon, 28 Nov 2016 17:57:09 +0100
Subject: [PATCH] change raw-bor: no longer expose the slice index
---
theories/lifetime/accessors.v | 26 +++++++++--------
theories/lifetime/borrow.v | 49 +++++++++++++++++----------------
theories/lifetime/definitions.v | 6 ++--
theories/lifetime/rebor.v | 44 +++++++++++++++--------------
4 files changed, 66 insertions(+), 59 deletions(-)
diff --git a/theories/lifetime/accessors.v b/theories/lifetime/accessors.v
index cae3177e..db2fa8ec 100644
--- a/theories/lifetime/accessors.v
+++ b/theories/lifetime/accessors.v
@@ -169,7 +169,7 @@ Lemma bor_acc_strong E q κ P :
∀ Q, ▷ Q -∗ ▷(▷ Q -∗ [†κ'] ={⊤∖↑lftN}=∗ ▷ P) ={E}=∗ &{κ'} Q ∗ q.[κ].
Proof.
unfold bor, raw_bor. iIntros (HE) "#LFT Hbor Htok".
- iDestruct "Hbor" as (i) "(#Hle & Hbor & #Hs)".
+ iDestruct "Hbor" as (κ'') "(#Hle & Htmp)". iDestruct "Htmp" as (s'') "(Hbor & #Hs)".
iMod (lft_incl_acc with "Hle Htok") as (q') "[Htok Hclose]". solve_ndisj.
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
iDestruct (own_bor_auth with "HI [Hbor]") as %Hκ'. by unfold idx_bor_own.
@@ -177,12 +177,12 @@ Proof.
/lfts_inv /lft_inv /lft_inv_dead /lft_alive_in lft_inv_alive_unfold.
iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]] Hclose'']".
- iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
- iMod (bor_open_internal with "Hs Halive Hbor Htok") as "(Halive & Hbor & $)".
+ iMod (bor_open_internal _ _ (κ'', s'') with "Hs Halive Hbor Htok") as "(Halive & Hbor & $)".
solve_ndisj.
iMod ("Hclose'" with "[-Hbor Hclose]") as "_".
{ iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
iLeft. iFrame "%". iExists _, _. iFrame. }
- iExists (i.1). iFrame "#". iIntros "!>*HQ HvsQ". clear -HE.
+ iExists κ''. iFrame "#". iIntros "!>*HQ HvsQ". clear -HE.
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
iDestruct (own_bor_auth with "HI Hbor") as %Hκ'.
rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
@@ -214,8 +214,8 @@ Proof.
iMod ("Hclose'" with "[-Hbor Htok Hclose]") as "_".
{ iExists _, _. iFrame. rewrite big_sepS_later /lft_bor_alive. iApply "Hclose''".
iLeft. iFrame "%". iExists _, _. iFrame. }
- iMod ("Hclose" with "Htok") as "$". iExists (i.1, j). iFrame "∗#".
- iApply lft_incl_refl.
+ iMod ("Hclose" with "Htok") as "$". iExists κ''. iModIntro.
+ iSplit; first by iApply lft_incl_refl. iExists j. iFrame "∗#".
+ iDestruct "Hinv" as (?) "[Hinv _]". iDestruct "Hinv" as (B ?) "[>Hinv _]".
iDestruct (own_bor_valid_2 with "Hinv Hbor")
as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_valid_discrete_2.
@@ -232,8 +232,8 @@ Lemma bor_acc_atomic_strong E κ P :
∀ Q, ▷ Q -∗ ▷ (▷ Q -∗ [†κ'] ={⊤∖↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ'} Q) ∨
[†κ] ∗ |={E∖↑lftN,E}=> True.
Proof.
- unfold bor, raw_bor. iIntros (HE) "#LFT Hbor".
- iDestruct "Hbor" as (i) "(#Hle & Hbor & #Hs)".
+ iIntros (HE) "#LFT Hbor". rewrite bor_unfold_idx /idx_bor /bor /raw_bor.
+ iDestruct "Hbor" as (i) "((#Hle & #Hs) & Hbor)".
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
iDestruct (own_bor_auth with "HI [Hbor]") as %Hκ'. by unfold idx_bor_own.
rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
@@ -251,18 +251,20 @@ Proof.
iMod "Hclose" as "_". iDestruct (add_vs with "EQ Hvs HvsQ") as "Hvs".
iMod (slice_insert_full _ _ true with "HQ Hbox") as (j) "(% & #Hs' & Hbox)".
solve_ndisj.
- iExists (i.1, j). iFrame "∗#".
iMod (own_bor_update_2 with "Hown Hbor") as "Hown".
{ apply auth_update. etrans.
- apply delete_singleton_local_update, _.
- apply (alloc_singleton_local_update _ j (1%Qp, DecAgree (Bor_in))); last done.
rewrite -fmap_delete lookup_fmap fmap_None
-fmap_None -lookup_fmap fmap_delete //. }
- rewrite own_bor_op -lft_incl_refl. iDestruct "Hown" as "[Hown $]".
- iApply "Hclose'". iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
- iLeft. iFrame "%". iExists _, _. iFrame.
+ rewrite own_bor_op. iDestruct "Hown" as "[Hâ— Hâ—¯]".
+ iMod ("Hclose'" with "[- Hâ—¯]"); last first.
+ { iModIntro. iExists (i.1). iSplit; first by iApply lft_incl_refl.
+ iExists j. iFrame. done. }
+ iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
+ iLeft. iFrame "%". iExists _, _. iFrame. iNext.
rewrite -!fmap_delete -fmap_insert -(fmap_insert _ _ _ Bor_in).
- iExists _. iFrame "Hbox Hown".
+ iExists _. iFrame "Hbox Hâ—".
rewrite big_sepM_insert. by rewrite big_sepM_delete.
by rewrite -fmap_None -lookup_fmap fmap_delete.
- iRight. iMod (create_dead with "HA") as "[HA #H†]". done.
diff --git a/theories/lifetime/borrow.v b/theories/lifetime/borrow.v
index 5a97f4f7..c4e5f040 100644
--- a/theories/lifetime/borrow.v
+++ b/theories/lifetime/borrow.v
@@ -10,8 +10,11 @@ Implicit Types κ : lft.
Lemma bor_unfold_idx κ P : &{κ}P ⊣⊢ ∃ i, &{κ,i}P ∗ idx_bor_own 1 i.
Proof.
- rewrite /bor /raw_bor /idx_bor /bor_idx. f_equiv. intros [??].
- rewrite -assoc. f_equiv. by rewrite comm.
+ rewrite /bor /raw_bor /idx_bor /bor_idx. iProof; iSplit.
+ - iIntros "H". iDestruct "H" as (κ') "[? Hraw]". iDestruct "Hraw" as (s) "[??]".
+ iExists (κ', s). by iFrame.
+ - iIntros "H". iDestruct "H" as ([κ' s]) "[[??]?]". iExists κ'. iFrame.
+ iExists s. by iFrame.
Qed.
Lemma bor_shorten κ κ' P: κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
@@ -35,8 +38,8 @@ 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 (raw_bor_fake _ true with "Hdead") as (i) "[Hdead Hbor]"; first solve_ndisj.
- unfold bor. iExists (κ, i). iFrame. rewrite -lft_incl_refl -big_sepS_later.
+ iMod (raw_bor_fake _ true with "Hdead") as "[Hdead Hbor]"; first solve_ndisj.
+ unfold bor. iExists κ. iFrame. rewrite -lft_incl_refl -big_sepS_later.
iApply "Hclose". iExists _, _. iFrame. iApply "Hclose'". iRight. iFrame. eauto.
Qed.
@@ -83,8 +86,8 @@ Proof.
- rewrite /lft_inh. iExists _. iFrame. }
iMod ("Hclose" with "[HA HI Hclose']") as "_"; [by iExists _, _; iFrame|].
iSplitL "HBâ—¯ HsliceB".
- + rewrite /bor /raw_bor /idx_bor_own. iExists (κ, γB); simpl.
- iFrame. by iApply lft_incl_refl.
+ + rewrite /bor /raw_bor /idx_bor_own. iExists κ; simpl.
+ iModIntro. iSplit; first by iApply lft_incl_refl. iExists γB. by iFrame.
+ clear -HE. iIntros "!> H†".
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
iDestruct (own_inh_auth with "HI HE◯") as %Hκ.
@@ -113,8 +116,8 @@ Proof.
set_solver+.
- iFrame "HP". iApply fupd_frame_r. iSplitR ""; last by auto.
rewrite /lft_inv_dead. iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)" .
- iMod (raw_bor_fake _ true with "Hdead") as (i) "[Hdead Hbor]"; first solve_ndisj.
- unfold bor. iExists (κ, i). iFrame. rewrite -lft_incl_refl -big_sepS_later.
+ iMod (raw_bor_fake _ true with "Hdead") as "[Hdead Hbor]"; first solve_ndisj.
+ unfold bor. iExists κ. iFrame. rewrite -lft_incl_refl -big_sepS_later.
iApply "Hclose". iExists _, _. iFrame. iApply "Hclose'". iNext.
rewrite /lft_inv. iRight. rewrite /lft_inv_dead. iFrame. eauto.
Qed.
@@ -125,7 +128,7 @@ Lemma bor_sep E κ P Q :
Proof.
iIntros (HE) "#Hmgmt HP". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
rewrite {1}/bor /raw_bor /idx_bor_own.
- iDestruct "HP" as ([κ' s]) "[#Hκκ' [Hbor Hslice]]".
+ iDestruct "HP" as (κ') "[#Hκκ' Htmp]". iDestruct "Htmp" as (s) "[Hbor Hslice]".
iDestruct (own_bor_auth with "HI Hbor") 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.
@@ -152,9 +155,9 @@ Proof.
-fmap_None -lookup_fmap fmap_delete //. }
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 "∗#". }
+ { rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ1. iFrame. }
iAssert (&{κ}Q)%I with "[H◯2 Hs2]" as "$".
- { rewrite /bor /raw_bor /idx_bor_own. iExists (κ', γ2). iFrame "∗#". }
+ { rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ2. iFrame. }
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â—".
@@ -163,12 +166,12 @@ 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 (raw_bor_fake _ true with "Hdead") as (i1) "[Hdead Hbor1]"; first solve_ndisj.
- iMod (raw_bor_fake _ true with "Hdead") as (i2) "[Hdead Hbor2]"; first solve_ndisj.
+ iMod (raw_bor_fake _ true with "Hdead") as "[Hdead Hbor1]"; first solve_ndisj.
+ iMod (raw_bor_fake _ true with "Hdead") as "[Hdead Hbor2]"; first 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.
+ unfold bor. iSplitL "Hbor1"; iExists _; eauto.
Qed.
Lemma bor_combine E κ P Q :
@@ -176,14 +179,13 @@ Lemma bor_combine E κ P Q :
lft_ctx -∗ &{κ} P -∗ &{κ} Q ={E}=∗ &{κ} (P ∗ Q).
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 _]".
+ iDestruct "HP" as (κ1) "[#Hκ1 Hbor1]". iDestruct "HQ" as (κ2) "[#Hκ2 Hbor2]".
+ iMod (raw_rebor _ _ (κ1 ∪ κ2) with "Hmgmt Hbor1") as "[Hbor1 _]".
done. by apply gmultiset_union_subseteq_l.
- iMod (raw_rebor _ _ (κ1 ∪ κ2) with "Hmgmt Hbor2") as (j2) "[Hbor2 _]".
+ iMod (raw_rebor _ _ (κ1 ∪ κ2) with "Hmgmt 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 "[Hbor1 Hslice1]". iDestruct "Hbor2" as "[Hbor2 Hslice2]".
+ iDestruct "Hbor1" as (j1) "[Hbor1 Hslice1]". iDestruct "Hbor2" as (j2) "[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.
@@ -217,8 +219,9 @@ Proof.
-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"). }
+ { rewrite /bor /raw_bor /idx_bor_own. iExists (κ1 ∪ κ2).
+ iSplit; first by iApply (lft_incl_glb with "Hκ1 Hκ2").
+ iExists γ. iFrame. }
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â—".
@@ -228,10 +231,10 @@ Proof.
rewrite lookup_delete_ne //.
+ rewrite -fmap_None -lookup_fmap !fmap_delete //.
- iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
- iMod (raw_bor_fake _ true with "Hdead") as (i) "[Hdead Hbor]"; first solve_ndisj.
+ iMod (raw_bor_fake _ true with "Hdead") as "[Hdead Hbor]"; first 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").
+ unfold bor. iExists _. iFrame. iApply (lft_incl_glb with "Hκ1 Hκ2").
Qed.
End borrow.
diff --git a/theories/lifetime/definitions.v b/theories/lifetime/definitions.v
index 8441937f..995a2fb3 100644
--- a/theories/lifetime/definitions.v
+++ b/theories/lifetime/definitions.v
@@ -174,10 +174,10 @@ Section defs.
own_bor (i.1) (â—¯ {[ i.2 := (q,DecAgree Bor_in) ]}).
Definition idx_bor (κ : lft) (i : bor_idx) (P : iProp Σ) : iProp Σ :=
(lft_incl κ (i.1) ∗ slice borN (i.2) P)%I.
- Definition raw_bor (i : bor_idx) (P : iProp Σ) : iProp Σ :=
- (idx_bor_own 1 i ∗ slice borN (i.2) P)%I.
+ Definition raw_bor (κ : lft) (P : iProp Σ) : iProp Σ :=
+ (∃ s : slice_name, idx_bor_own 1 (κ, s) ∗ slice borN s P)%I.
Definition bor (κ : lft) (P : iProp Σ) : iProp Σ :=
- (∃ i, lft_incl κ (i.1) ∗ raw_bor i P)%I.
+ (∃ κ', lft_incl κ κ' ∗ raw_bor κ' P)%I.
End defs.
Instance: Params (@lft_bor_alive) 4.
diff --git a/theories/lifetime/rebor.v b/theories/lifetime/rebor.v
index 310dd12b..bba7edee 100644
--- a/theories/lifetime/rebor.v
+++ b/theories/lifetime/rebor.v
@@ -10,45 +10,47 @@ Implicit Types κ : lft.
Lemma raw_bor_fake E q κ P :
↑borN ⊆ E →
- ▷?q lft_bor_dead κ ={E}=∗ ∃ i, ▷?q lft_bor_dead κ ∗ raw_bor (κ, i) P.
+ ▷?q lft_bor_dead κ ={E}=∗ ▷?q lft_bor_dead κ ∗ raw_bor κ P.
Proof.
iIntros (?) "Hdead". rewrite /lft_bor_dead.
iDestruct "Hdead" as (B Pinh) "[>Hown Hbox]".
- iMod (slice_insert_empty _ _ _ _ P with "Hbox") as (γ) "(% & Hslice & Hbox)".
+ iMod (slice_insert_empty _ _ _ _ P with "Hbox") as (γ) "(% & #Hslice & Hbox)".
iMod (own_bor_update with "Hown") as "Hown".
{ eapply auth_update_alloc,
(alloc_local_update _ _ _ (1%Qp, DecAgree Bor_in)); last done.
by do 2 eapply lookup_to_gmap_None. }
- rewrite own_bor_op insert_empty /bor /raw_bor /idx_bor_own /=. iExists γ.
- iDestruct "Hown" as "[Hâ— $]". iFrame "Hslice". iModIntro. iNext.
- iExists ({[γ]} ∪ B), (P ∗ Pinh)%I. rewrite !to_gmap_union_singleton. by iFrame.
+ rewrite own_bor_op insert_empty /bor /raw_bor /idx_bor_own /=.
+ iModIntro. iDestruct "Hown" as "[Hâ— Hâ—¯]". iSplitR "Hâ—¯".
+ - iExists ({[γ]} ∪ B), (P ∗ Pinh)%I. rewrite !to_gmap_union_singleton. by iFrame.
+ - iExists γ. by iFrame.
Qed.
-Lemma raw_bor_unnest A I Pb Pi P κ κ' i :
+Lemma raw_bor_unnest A I Pb Pi P κ κ' :
let Iinv := (
own_ilft_auth I ∗
▷ [∗ set] κ ∈ dom _ I ∖ {[κ']}, lft_inv A κ)%I in
κ ⊆ κ' →
lft_alive_in A κ' →
- Iinv -∗ raw_bor (κ,i) P -∗ ▷ lft_bor_alive κ' Pb -∗
- ▷ lft_vs κ' (Pb ∗ raw_bor (κ,i) P) Pi ={↑borN}=∗ ∃ Pb' j,
- Iinv ∗ raw_bor (κ',j) P ∗ ▷ lft_bor_alive κ' Pb' ∗ ▷ lft_vs κ' Pb' Pi.
+ Iinv -∗ raw_bor κ P -∗ ▷ lft_bor_alive κ' Pb -∗
+ ▷ lft_vs κ' (Pb ∗ raw_bor κ P) Pi ={↑borN}=∗ ∃ Pb',
+ Iinv ∗ raw_bor κ' P ∗ ▷ lft_bor_alive κ' Pb' ∗ ▷ lft_vs κ' Pb' Pi.
Proof.
iIntros (Iinv Hκκ' Haliveκ') "(HI◠& HI) Hraw Hκalive' Hvs".
destruct (decide (κ = κ')) as [<-|Hκneq].
- { iModIntro. iExists Pb, i. rewrite /Iinv. iFrame "HI◠HI Hκalive' Hraw".
+ { iModIntro. iExists Pb. rewrite /Iinv. iFrame "HI◠HI Hκalive' Hraw".
iNext. rewrite !lft_vs_unfold. iDestruct "Hvs" as (n) "[Hn Hvs]".
iExists n. iFrame "Hn". clear Iinv I.
- iIntros (I). rewrite lft_vs_inv_unfold. iIntros "(Hdead & $ & HI) HPb Hκ†".
- iMod (raw_bor_fake _ false _ P with "Hdead") as (i') "?"; first solve_ndisj.
- (* We get the existential too late *)
- admit. }
+ iIntros (I). rewrite {1}lft_vs_inv_unfold. iIntros "(Hdead & HI & Hκs) HPb #Hκ†".
+ iMod (raw_bor_fake _ false _ P with "Hdead") as "[Hdead Hraw]"; first solve_ndisj.
+ iApply ("Hvs" $! I with "[Hdead HI Hκs] [HPb Hraw] Hκ†").
+ - rewrite lft_vs_inv_unfold. by iFrame.
+ - iNext. by iFrame. }
assert (κ ⊂ κ') by (by apply strict_spec_alt).
rewrite lft_vs_unfold. iDestruct "Hvs" as (n) "[>Hcnt Hvs]".
iMod (own_cnt_update with "Hcnt") as "Hcnt".
{ apply auth_update_alloc, (nat_local_update _ 0 (S n) 1); omega. }
rewrite own_cnt_op; iDestruct "Hcnt" as "[Hcnt Hcnt1]".
- rewrite {1}/raw_bor /idx_bor_own /=. iDestruct "Hraw" as "[Hbor #Hislice]".
+ rewrite {1}/raw_bor /idx_bor_own /=. iDestruct "Hraw" as (i) "[Hbor #Hislice]".
iDestruct (own_bor_auth with "HIâ— Hbor") as %?.
rewrite big_sepS_later.
iDestruct (big_sepS_elem_of_acc _ (dom (gset lft) I ∖ _) κ with "HI")
@@ -88,9 +90,9 @@ Proof.
(alloc_singleton_local_update _ j (1%Qp, DecAgree Bor_in)); last done.
rewrite /to_borUR lookup_fmap. by rewrite HBj. }
rewrite own_bor_op. iDestruct "HFOO" as "[HκB Hj]".
- iModIntro. iExists (P ∗ Pb)%I, j. rewrite /Iinv. iFrame "HI◠HI".
+ iModIntro. iExists (P ∗ Pb)%I. rewrite /Iinv. iFrame "HI◠HI".
iSplitL "Hj".
- { rewrite /raw_bor /idx_bor_own. by iFrame. }
+ { rewrite /raw_bor /idx_bor_own. iExists j. by iFrame. }
iSplitL "HB HκB Hbox".
{ rewrite /lft_bor_alive. iNext. iExists (<[j:=Bor_in]> B).
rewrite /to_borUR !fmap_insert big_sepM_insert //. iFrame.
@@ -126,12 +128,12 @@ Proof.
{ rewrite /raw_bor /idx_bor_own /=. iFrame; auto. }
iModIntro. rewrite -[S n]Nat.add_1_l -nat_op_plus auth_frag_op own_cnt_op.
by iFrame.
-Admitted.
+Qed.
-Lemma raw_rebor E κ κ' i P :
+Lemma raw_rebor E κ κ' P :
↑lftN ⊆ E → κ ⊆ κ' →
- lft_ctx -∗ raw_bor (κ, i) P ={E}=∗
- ∃ j, raw_bor (κ', j) P ∗ ([†κ'] ={E}=∗ raw_bor (κ, i) P).
+ lft_ctx -∗ raw_bor κ P ={E}=∗
+ raw_bor κ' P ∗ ([†κ'] ={E}=∗ raw_bor κ P).
Admitted.
Lemma bor_rebor' E κ κ' P :
--
GitLab