From 22c355864d2c4a1cbc1879464db5b5b43af166b5 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sat, 19 Aug 2017 10:52:03 +0200
Subject: [PATCH] The inheritance of raw reborrowing is not (no longer)
necessary. Let's remove it and call it shorten.
---
theories/lifetime/model/borrow_sep.v | 4 ++--
theories/lifetime/model/creation.v | 2 +-
theories/lifetime/model/reborrow.v | 24 +++++++++---------------
3 files changed, 12 insertions(+), 18 deletions(-)
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 20be9317..fd37a3f7 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/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]".
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index da80d4ee..befd40f2 100644
--- a/theories/lifetime/model/creation.v
+++ b/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".
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index e4707ecc..e9d9674a 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/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|].
--
GitLab