From f81c0f3a9e4141b9edbbfd0e5b425573cc40b66a Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 23 Jan 2017 13:39:14 +0100
Subject: [PATCH] Simplify proofs related to unique borrows by making borrows
respectfull of iff.
---
opam.pins | 2 +-
theories/lifetime/lifetime.v | 11 ----
theories/lifetime/lifetime_sig.v | 2 +
theories/lifetime/model/accessors.v | 36 +++++++-----
theories/lifetime/model/borrow.v | 29 +++++++---
theories/lifetime/model/definitions.v | 4 +-
theories/lifetime/model/faking.v | 2 +-
theories/lifetime/model/primitive.v | 21 +++++++
theories/lifetime/model/raw_reborrow.v | 20 ++++---
theories/lifetime/model/reborrow.v | 12 ++--
theories/typing/borrow.v | 29 ++++------
theories/typing/lft_contexts.v | 3 +-
theories/typing/product_split.v | 15 ++---
theories/typing/type_sum.v | 9 +--
theories/typing/uniq_bor.v | 78 ++++++++------------------
15 files changed, 136 insertions(+), 137 deletions(-)
diff --git a/opam.pins b/opam.pins
index 57ff8356..996ed0d8 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 9fa0b57d44cbba40d7bb272b45cc0875bc68940d
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq da3aa7e4497878a70b00f17bf109e18ef2a079d3
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index c618222f..bae90946 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -67,17 +67,6 @@ Proof.
iModIntro. iNext. iApply ("Hclose" with "* HP []"). by iIntros "!> $".
Qed.
-Lemma bor_iff (P Q : iProp Σ) E κ :
- ↑lftN ⊆ E →
- lft_ctx -∗ ▷ □ (P ↔ Q) -∗ &{κ}P ={E}=∗ &{κ}Q.
-Proof.
- iIntros (?) "#LFT #Heq Hb".
- iMod (bor_acc_atomic_cons with "LFT Hb") as "[[HP Hclose]|[H†Hclose]]". done.
- - iApply ("Hclose" with "[HP] []").
- by iApply "Heq". by iIntros "!>HQ!>"; iApply "Heq".
- - iMod "Hclose". by iApply (bor_fake with "LFT").
-Qed.
-
Lemma bor_persistent P `{!PersistentP P} E κ :
↑lftN ⊆ E →
lft_ctx -∗ &{κ}P ={E}=∗ ▷ P ∨ [†κ].
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index d9f55c4d..a290347a 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -67,9 +67,11 @@ Module Type lifetime_sig.
Global Declare Instance bor_ne κ n : Proper (dist n ==> dist n) (bor κ).
Global Declare Instance bor_contractive κ : Contractive (bor κ).
Global Declare Instance bor_proper κ : Proper ((≡) ==> (≡)) (bor κ).
+ Parameter bor_iff_proper : ∀ κ P P', ▷ □ (P ↔ P') -∗ &{κ}P -∗ &{κ}P'.
Global Declare Instance idx_bor_ne κ i n : Proper (dist n ==> dist n) (idx_bor κ i).
Global Declare Instance idx_bor_contractive κ i : Contractive (idx_bor κ i).
Global Declare Instance idx_bor_proper κ i : Proper ((≡) ==> (≡)) (idx_bor κ i).
+ Parameter idx_bor_iff_proper : ∀ κ i P P', ▷ □ (P ↔ P') -∗ &{κ,i}P -∗ &{κ,i}P'.
Global Declare Instance lft_tok_fractional κ : Fractional (λ q, q.[κ])%I.
Global Declare Instance lft_tok_as_fractional κ q :
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 6b53811d..82b9e942 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -75,6 +75,7 @@ Lemma idx_bor_acc E q κ i P :
▷ P ∗ (▷ P ={E}=∗ idx_bor_own 1 i ∗ q.[κ]).
Proof.
unfold idx_bor. iIntros (HE) "#LFT [#Hle #Hs] Hbor Htok".
+ iDestruct "Hs" as (P') "[#HPP' 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.
@@ -82,12 +83,13 @@ 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 & Hf & $)".
+ iMod (bor_open_internal with "Hs Halive Hbor Htok") as "(Halive & Hf & HP')".
solve_ndisj.
+ iDestruct ("HPP'" with "HP'") as "$".
iMod ("Hclose'" with "[-Hf Hclose]") as "_".
{ iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
iLeft. iFrame "%". iExists _, _. iFrame. }
- iIntros "!>HP". clear -HE.
+ iIntros "!>HP'". iDestruct ("HPP'" with "HP'") as "HP". clear -HE.
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
iDestruct (own_bor_auth with "HI Hf") as %Hκ'.
rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
@@ -116,6 +118,7 @@ Lemma idx_bor_atomic_acc E q κ i P :
([†κ] ∗ |={E∖↑lftN,E}=> idx_bor_own q i).
Proof.
unfold idx_bor, idx_bor_own. iIntros (HE) "#LFT [#Hle #Hs] Hbor".
+ iDestruct "Hs" as (P') "[#HPP' Hs]".
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 //
@@ -126,9 +129,11 @@ Proof.
iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
iDestruct (own_bor_valid_2 with "Hown Hbor")
as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
- iMod (slice_empty _ _ true with "Hs Hbox") as "[$ Hbox]".
+ iMod (slice_empty _ _ true with "Hs Hbox") as "[HP' Hbox]".
solve_ndisj. by rewrite lookup_fmap EQB.
- iMod fupd_intro_mask' as "Hclose"; last iIntros "!>HP". solve_ndisj.
+ iDestruct ("HPP'" with "HP'") as "$".
+ iMod fupd_intro_mask' as "Hclose"; last iIntros "!>HP'". solve_ndisj.
+ iDestruct ("HPP'" with "HP'") as "HP".
iMod "Hclose" as "_". iMod (slice_fill _ _ true with "Hs HP Hbox") as "Hbox".
solve_ndisj. by rewrite lookup_insert. iFrame.
iApply "Hclose'". iExists _, _. iFrame. rewrite big_sepS_later.
@@ -151,6 +156,7 @@ Lemma bor_acc_strong E q κ P :
Proof.
unfold bor, raw_bor. iIntros (HE) "#LFT Hbor Htok".
iDestruct "Hbor" as (κ'') "(#Hle & Htmp)". iDestruct "Htmp" as (s'') "(Hbor & #Hs)".
+ iDestruct "Hs" as (P') "[#HPP' 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.
@@ -158,8 +164,9 @@ 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 _ _ (κ'', s'') with "Hs Halive Hbor Htok") as "(Halive & Hbor & $)".
- solve_ndisj.
+ iMod (bor_open_internal _ _ (κ'', s'') with "Hs Halive Hbor Htok")
+ as "(Halive & Hbor & HP')". solve_ndisj.
+ iDestruct ("HPP'" with "HP'") as "$".
iMod ("Hclose'" with "[-Hbor Hclose]") as "_".
{ iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
iLeft. iFrame "%". iExists _, _. iFrame. }
@@ -176,7 +183,8 @@ Proof.
as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
iMod (slice_delete_empty _ _ true with "Hs Hbox") as (Pb') "[EQ Hbox]".
solve_ndisj. by rewrite lookup_fmap EQB.
- iDestruct (add_vs with "EQ Hvs HvsQ") as "Hvs".
+ iDestruct (add_vs with "EQ Hvs [HvsQ]") as "Hvs".
+ { iNext. iIntros "HQ H†". iApply "HPP'". iApply ("HvsQ" with "HQ H†"). }
iMod (slice_insert_empty _ _ true with "Hbox") as (j) "(% & #Hs' & Hbox)".
iMod (own_bor_update_2 with "Hown Hbor") as "Hown".
{ apply auth_update. etrans.
@@ -196,7 +204,8 @@ Proof.
{ iExists _, _. iFrame. rewrite big_sepS_later /lft_bor_alive. iApply "Hclose''".
iLeft. iFrame "%". iExists _, _. iFrame. }
iMod ("Hclose" with "Htok") as "$". iExists κ''. iModIntro.
- iSplit; first by iApply lft_incl_refl. iExists j. iFrame "∗#".
+ iSplit; first by iApply lft_incl_refl. iExists j. iFrame.
+ iExists Q. rewrite -uPred.iff_refl. eauto.
+ 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.
@@ -215,6 +224,7 @@ Lemma bor_acc_atomic_strong E κ P :
Proof.
iIntros (HE) "#LFT Hbor". rewrite bor_unfold_idx /idx_bor /bor /raw_bor.
iDestruct "Hbor" as (i) "((#Hle & #Hs) & Hbor)".
+ iDestruct "Hs" as (P') "[#HPP' Hs]".
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 //
@@ -226,10 +236,11 @@ Proof.
iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
iDestruct (own_bor_valid_2 with "Hown Hbor")
as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
- iMod (slice_delete_full _ _ true with "Hs Hbox") as (Pb') "($ & EQ & Hbox)".
- solve_ndisj. by rewrite lookup_fmap EQB.
+ iMod (slice_delete_full _ _ true with "Hs Hbox") as (Pb') "(HP' & EQ & Hbox)".
+ solve_ndisj. by rewrite lookup_fmap EQB. iDestruct ("HPP'" with "HP'") as "$".
iMod fupd_intro_mask' as "Hclose"; last iIntros "!>*HQ HvsQ". solve_ndisj.
- iMod "Hclose" as "_". iDestruct (add_vs with "EQ Hvs HvsQ") as "Hvs".
+ iMod "Hclose" as "_". iDestruct (add_vs with "EQ Hvs [HvsQ]") as "Hvs".
+ { iNext. iIntros "HQ H†". iApply "HPP'". iApply ("HvsQ" with "HQ H†"). }
iMod (slice_insert_full _ _ true with "HQ Hbox") as (j) "(% & #Hs' & Hbox)".
solve_ndisj.
iMod (own_bor_update_2 with "Hown Hbor") as "Hown".
@@ -241,7 +252,7 @@ Proof.
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 j. iFrame. iExists Q. rewrite -uPred.iff_refl. auto. }
iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
iLeft. iFrame "%". iExists _, _. iFrame. iNext.
rewrite -!fmap_delete -fmap_insert -(fmap_insert _ _ _ Bor_in).
@@ -281,5 +292,4 @@ Proof.
- iLeft. iIntros "!> {$HP} HP". iMod ("Hclose" with "* HP []"); auto.
- iRight. by iFrame.
Qed.
-
End accessors.
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 4fba2a91..1f220cda 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -44,7 +44,8 @@ Proof.
iMod ("Hclose" with "[HA HI Hclose']") as "_"; [by iExists _, _; iFrame|].
iSplitL "HBâ—¯ HsliceB".
+ rewrite /bor /raw_bor /idx_bor_own. iExists κ; simpl.
- iModIntro. iSplit; first by iApply lft_incl_refl. iExists γB. by iFrame.
+ iModIntro. iSplit; first by iApply lft_incl_refl. iExists γB. iFrame.
+ iExists P. rewrite -uPred.iff_refl. auto.
+ clear -HE. iIntros "!> H†".
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
iDestruct ("HIlookup" with "* HI") as %Hκ.
@@ -74,6 +75,7 @@ Proof.
iIntros (HE) "#LFT Hbor". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
rewrite {1}/bor. iDestruct "Hbor" as (κ') "[#Hκκ' Hbor]".
rewrite /raw_bor /idx_bor_own. iDestruct "Hbor" as (s) "[Hbor Hslice]".
+ iDestruct "Hslice" as (P') "[#HPP' 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.
@@ -83,9 +85,16 @@ Proof.
iDestruct "H" as (B) "(Hbox & >Hown & HB)".
iDestruct (own_bor_valid_2 with "Hown Hbor")
as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
- iMod (slice_split _ _ true with "Hslice Hbox")
- as (γ1 γ2) "(% & % & % & Hs1 & Hs2 & Hbox)"; first solve_ndisj.
+ iMod (slice_iff _ _ true with "HPP' Hslice Hbox")
+ 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 false 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.
+ { by rewrite lookup_insert. }
+ rewrite delete_insert //. iDestruct "Hγ1" as %Hγ1. iDestruct "Hγ2" as %Hγ2.
iMod (own_bor_update_2 with "Hown Hbor") as "Hbor".
{ etrans; last etrans.
- apply auth_update_dealloc. by apply delete_singleton_local_update, _.
@@ -100,11 +109,13 @@ 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 κ'. iFrame "#". iExists γ1. iFrame. }
+ { rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ1.
+ iFrame. iExists P. rewrite -uPred.iff_refl. auto. }
iAssert (&{κ}Q)%I with "[H◯2 Hs2]" as "$".
- { rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ2. iFrame. }
+ { rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ2.
+ iFrame. iExists Q. rewrite -uPred.iff_refl. auto. }
iApply "Hclose". iExists A, I. iFrame. rewrite big_sepS_later.
- iApply "Hclose'". iLeft. iFrame "%". iExists Pb, Pi. iFrame. iExists _.
+ iApply "Hclose'". iLeft. iFrame "%". iExists Pb', Pi. iFrame. iExists _.
rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "Hbox Hâ—".
rewrite !big_sepM_insert /=.
+ by rewrite left_id -(big_sepM_delete _ _ _ _ EQB).
@@ -131,6 +142,8 @@ Proof.
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]".
+ iDestruct "Hslice1" as (P') "[#HPP' Hslice1]".
+ iDestruct "Hslice2" as (Q') "[#HQQ' 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.
@@ -166,7 +179,8 @@ Proof.
iAssert (&{κ}(P ∗ Q))%I with "[H◯ Hslice]" as "$".
{ rewrite /bor /raw_bor /idx_bor_own. iExists (κ1 ∪ κ2).
iSplit; first by iApply (lft_incl_glb with "Hκ1 Hκ2").
- iExists γ. iFrame. }
+ iExists γ. iFrame. iExists _. iFrame. iNext. iAlways.
+ by iSplit; iIntros "[HP HQ]"; iSplitL "HP"; (iApply "HPP'" || iApply "HQQ'"). }
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â—".
@@ -182,5 +196,4 @@ Proof.
iRight. iSplit; last by auto. iExists _. iFrame. }
unfold bor. iExists _. iFrame. iApply (lft_incl_glb with "Hκ1 Hκ2").
Qed.
-
End borrow.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index d5677a85..e4a59714 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -183,9 +183,9 @@ Section defs.
Definition idx_bor_own (q : frac) (i : bor_idx) : iProp Σ :=
own_bor (i.1) (â—¯ {[ i.2 := (q, to_agree Bor_in) ]}).
Definition idx_bor (κ : lft) (i : bor_idx) (P : iProp Σ) : iProp Σ :=
- (lft_incl κ (i.1) ∗ slice borN (i.2) P)%I.
+ (lft_incl κ (i.1) ∗ ∃ P', ▷ □ (P' ↔ P) ∗ 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.
+ (∃ s : slice_name, idx_bor_own 1 (κ, s) ∗ ∃ P', ▷ □ (P' ↔ P) ∗ slice borN s P')%I.
Definition bor (κ : lft) (P : iProp Σ) : iProp Σ :=
(∃ κ', lft_incl κ κ' ∗ raw_bor κ' P)%I.
End defs.
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 07e170e1..95287fd0 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -90,7 +90,7 @@ Proof.
by do 2 eapply lookup_to_gmap_None. }
rewrite /bor /raw_bor /idx_bor_own /=. iModIntro. iSplitR "Hâ—¯".
- iExists ({[γ]} ∪ B), (P ∗ Pinh)%I. rewrite !to_gmap_union_singleton. by iFrame.
- - iExists γ. by iFrame.
+ - iExists γ. iFrame. iExists P. rewrite -uPred.iff_refl. eauto.
Qed.
Lemma raw_bor_fake' E κ P :
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 84ddb63f..8d99817c 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -373,6 +373,21 @@ Lemma lft_incl_intro κ κ' :
Proof. reflexivity. Qed.
(** Basic rules about borrows *)
+Lemma raw_bor_iff_proper i P P' : ▷ □ (P ↔ P') -∗ raw_bor i P -∗ raw_bor i P'.
+Proof.
+ iIntros "#HPP' HP". unfold raw_bor. iDestruct "HP" as (s) "[HiP HP]".
+ iExists s. iFrame. iDestruct "HP" as (P0) "[#Hiff ?]". iExists P0. iFrame.
+ iNext. iAlways. iSplit; iIntros.
+ by iApply "HPP'"; iApply "Hiff". by iApply "Hiff"; iApply "HPP'".
+Qed.
+
+Lemma idx_bor_iff_proper κ i P P' : ▷ □ (P ↔ P') -∗ &{κ,i}P -∗ &{κ,i}P'.
+Proof.
+ unfold idx_bor. iIntros "#HPP' [$ HP]". iDestruct "HP" as (P0) "[#HP0P Hs]".
+ iExists P0. iFrame. iNext. iAlways. iSplit; iIntros.
+ by iApply "HPP'"; iApply "HP0P". by iApply "HP0P"; iApply "HPP'".
+Qed.
+
Lemma bor_unfold_idx κ P : &{κ}P ⊣⊢ ∃ i, &{κ,i}P ∗ idx_bor_own 1 i.
Proof.
rewrite /bor /raw_bor /idx_bor /bor_idx. iSplit.
@@ -382,6 +397,12 @@ Proof.
iExists κ'. iFrame. iExists s. by iFrame.
Qed.
+Lemma bor_iff_proper κ P P' : ▷ □ (P ↔ P') -∗ &{κ}P -∗ &{κ}P'.
+Proof.
+ rewrite !bor_unfold_idx. iIntros "#HPP' HP". iDestruct "HP" as (i) "[??]".
+ iExists i. iFrame. by iApply (idx_bor_iff_proper with "HPP'").
+Qed.
+
Lemma bor_shorten κ κ' P : κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
Proof.
rewrite /bor. iIntros "#Hκκ'". iDestruct 1 as (i) "[#? ?]".
diff --git a/theories/lifetime/model/raw_reborrow.v b/theories/lifetime/model/raw_reborrow.v
index 7dbf4a55..a3be4ed6 100644
--- a/theories/lifetime/model/raw_reborrow.v
+++ b/theories/lifetime/model/raw_reborrow.v
@@ -62,9 +62,10 @@ 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.
+ iModIntro. iExists (P ∗ Pb)% I. rewrite /Iinv. iFrame "HI". iFrame.
iSplitL "Hj".
- { rewrite /raw_bor /idx_bor_own. iExists j. by iFrame. }
+ { rewrite /raw_bor /idx_bor_own. 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.
@@ -125,11 +126,14 @@ Proof.
iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinv Hclose]".
{ rewrite elem_of_difference elem_of_dom not_elem_of_singleton. done. }
rewrite {1}/raw_bor. iDestruct "Hraw" as (i) "[Hi #Hislice]".
- iMod (raw_bor_unnest with "[$HI $Hinv] Hi Hislice Hκalive' [Hvs]") as (Pb') "([HI Hκ] & ? & ? & ?)"; [done..| |].
+ iDestruct "Hislice" as (P') "[#HPP' Hislice]".
+ iMod (raw_bor_unnest with "[$HI $Hinv] Hi Hislice Hκalive' [Hvs]")
+ as (Pb') "([HI Hκ] & ? & ? & ?)"; [done..| |].
{ iApply (lft_vs_cons with "[]"); last done.
iIntros "[$ [>? $]]". iModIntro. iNext. rewrite /raw_bor.
- iExists i. by iFrame. }
- iExists Pb'. iModIntro. iFrame. iNext. by iApply "Hclose".
+ iExists i. iFrame. iExists _. iFrame "#". }
+ iExists Pb'. iModIntro. iFrame. iSplitL "Hclose Hκ". by iApply "Hclose".
+ by iApply (raw_bor_iff_proper with "HPP'").
Qed.
Lemma raw_rebor E κ κ' P :
@@ -156,6 +160,7 @@ Proof.
iSplit; last done. iExists Pi. by iFrame. }
rewrite lft_inv_alive_unfold; iDestruct "Hκinv'" as (Pb Pi) "(Hbor & Hvs & Hinh)".
rewrite {1}/raw_bor. iDestruct "Hκ" as (i) "[Hi #Hislice]".
+ iDestruct "Hislice" as (P') "[#HPP' Hislice]".
iMod (lft_inh_extend _ _ (idx_bor_own 1 (κ, i)) with "Hinh")
as "(Hinh & HIlookup & Hinh_close)"; first solve_ndisj.
iDestruct (own_bor_auth with "HI [Hi]") as %?.
@@ -164,8 +169,9 @@ Proof.
{ by rewrite elem_of_difference elem_of_dom not_elem_of_singleton. }
iMod (raw_bor_unnest _ true _ _ _ (idx_bor_own 1 (κ, i) ∗ Pi)%I
with "[$HI $Hκ] Hi Hislice Hbor [Hvs]")
- as (Pb') "([HI Hκ] & $ & Halive & Hvs)"; [solve_ndisj|done|done|..].
+ as (Pb') "([HI Hκ] & HP' & Halive & Hvs)"; [solve_ndisj|done|done|..].
{ iNext. by iApply lft_vs_frame. }
+ iDestruct (raw_bor_iff_proper with "HPP' HP'") as "$".
iDestruct ("Hκclose" with "Hκ") as "Hinv".
iMod ("Hclose" with "[HA HI Hinv Halive Hinh Hvs]") as "_".
{ iNext. rewrite {2}/lfts_inv. iExists A, I. iFrame "HA HI".
@@ -190,6 +196,6 @@ Proof.
iApply (big_sepS_delete _ _ κ'); first by apply elem_of_dom. iFrame "Hinv".
rewrite /lft_inv /lft_inv_dead. iRight. iSplit; last done.
iExists Pi'. iFrame. }
- iModIntro. rewrite /raw_bor. iExists i. by iFrame.
+ iModIntro. rewrite /raw_bor. iExists i. iFrame. iExists _. auto.
Qed.
End rebor.
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 59d91f25..ad98e4d8 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -35,7 +35,7 @@ Proof.
by iApply (lft_incl_trans with "H⊑").
- iIntros "Hκ†". iMod ("Hclose" with "[Hκ†]") as "Hκ''".
{ iApply lft_dead_or; auto. }
- iModIntro. rewrite /bor. eauto.
+ iModIntro. rewrite /bor. eauto.
Qed.
Lemma bor_unnest E κ κ' P :
@@ -70,13 +70,16 @@ Proof.
iApply (lft_incl_dead with "[] H†"); first done.
by iApply (lft_incl_mono with "Hκ⊑"). }
rewrite {1}/raw_bor /idx_bor_own /=; iDestruct "Hκ" as (i) "[Hi #Hislice]".
+ iDestruct "Hislice" as (P') "[#HPP' Hislice]".
rewrite lft_inv_alive_unfold;
iDestruct "Hinv'" as (Pb Pi) "(Halive & Hvs & Hinh)".
rewrite /lft_bor_alive; iDestruct "Halive" as (B) "(Hbox & >HBâ— & HB)".
iDestruct (own_bor_valid_2 with "HBâ— Hi")
as %[HB%to_borUR_included _]%auth_valid_discrete_2.
- iMod (slice_delete_full _ _ true with "Hislice Hbox") as (Pb') "(HP & #EQ & Hbox)"; first solve_ndisj.
- { by rewrite lookup_fmap HB. }
+ iMod (slice_delete_full _ _ true with "Hislice Hbox")
+ as (Pb') "(HP & #EQ & Hbox)"; first solve_ndisj.
+ { by rewrite lookup_fmap HB. }
+ iDestruct ("HPP'" with "HP") as "HP".
iMod (own_bor_update_2 with "HBâ— Hi") as "HBâ—".
{ apply auth_update_dealloc, delete_singleton_local_update. apply _. }
iMod (fupd_intro_mask') as "Hclose'"; last iModIntro; first solve_ndisj.
@@ -90,7 +93,7 @@ Proof.
[solve_ndisj|exact: gmultiset_union_subseteq_l|done| |].
{ (* TODO: Use iRewrite supporting contractive rewriting. *)
iApply (lft_vs_cons with "[]"); last done.
- iIntros "[$ Hbor]". iModIntro. iNext. by iRewrite "EQ". }
+ iIntros "[$ [Hbor HPb']]". iModIntro. iNext. iRewrite "EQ". iFrame. by iApply "HPP'". }
iMod ("Hclose" with "[-HP]") as "_".
{ iNext. simpl. rewrite /lfts_inv. iExists A, I. iFrame.
rewrite (big_sepS_delete _ (dom _ I) κ''); last by apply elem_of_dom.
@@ -99,5 +102,4 @@ Proof.
iModIntro. rewrite /bor. iExists κ''. iFrame. subst κ''.
by iApply (lft_incl_mono with "Hκ⊑").
Qed.
-
End reborrow.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 0d04c3ed..cc94d5a1 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -20,8 +20,8 @@ Section borrow.
iDestruct "H" as ([[]|]) "[% Hown]"; try iDestruct "Hown" as "[]".
iDestruct "Hown" as "[Hmt ?]". iMod (bor_create with "LFT Hmt") as "[Hbor Hext]". done.
iModIntro. iSplitL "Hbor".
- - iExists _. iSplit. done. iExists _. erewrite <-uPred.iff_refl. eauto.
- - iExists _. iSplit. done. iIntros "H†". by iMod ("Hext" with "H†") as "$".
+ - iExists _. auto.
+ - iExists _. iSplit. done. by iFrame.
Qed.
Lemma tctx_extract_hasty_borrow E L p n ty ty' κ T :
@@ -51,18 +51,17 @@ Section borrow.
rewrite tctx_interp_singleton.
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown";
- (try iDestruct "Hown" as "[]"). iDestruct "Hown" as (P) "[#HPiff HP]".
- iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
- iMod (bor_acc_cons with "LFT H↦ Htok") as "[H↦ Hclose']". done.
+ (try iDestruct "Hown" as "[]").
+ iMod (bor_acc_cons with "LFT Hown Htok") as "[H↦ Hclose']". done.
iDestruct "H↦" as ([|[[|l'|]|][]]) "[>H↦ Hown]"; try iDestruct "Hown" as ">[]".
iDestruct "Hown" as "[Hown H†]". rewrite heap_mapsto_vec_singleton. wp_read.
- iMod ("Hclose'" with "*[H↦ Hown H†][]") as "[Hbor Htok]"; last 1 first.
+ iMod ("Hclose'" $! (l↦#l' ∗ freeable_sz n (ty_size ty) l' ∗ _)%I
+ with "*[H↦ Hown H†][]") as "[Hbor Htok]"; last 1 first.
- iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
- iMod (bor_sep _ _ _ (l' ↦∗: ty_own ty tid) with "LFT Hbor") as "[_ Hbor]". done.
+ iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
iMod ("Hclose" with "Htok") as "($ & $)".
- rewrite tctx_interp_singleton tctx_hasty_val' //. iExists _.
- erewrite <-uPred.iff_refl. auto.
- - iFrame "H↦ H†Hown".
+ by rewrite tctx_interp_singleton tctx_hasty_val' //=.
+ - iFrame.
- iIntros "!>(?&?&?)!>". iNext. iExists _.
rewrite -heap_mapsto_vec_singleton. iFrame. by iFrame.
Qed.
@@ -115,15 +114,11 @@ Section borrow.
{ by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown";
- try iDestruct "Hown" as "[]". iDestruct "Hown" as (P) "[#HPiff HP]".
- iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
- iMod (bor_exists with "LFT H↦") as (vl) "Hbor". done.
+ try iDestruct "Hown" as "[]".
+ iMod (bor_exists with "LFT Hown") as (vl) "Hbor". done.
iMod (bor_sep with "LFT Hbor") as "[H↦ Hbor]". done.
destruct vl as [|[[]|][]];
try by iMod (bor_persistent_tok with "LFT Hbor Htok") as "[>[] _]".
- iMod (bor_exists with "LFT Hbor") as (P') "Hbor". done.
- iMod (bor_sep with "LFT Hbor") as "[H Hbor]". done.
- iMod (bor_persistent_tok with "LFT H Htok") as "[#HP'iff Htok]". done.
iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
rewrite heap_mapsto_vec_singleton.
iApply (wp_fupd_step _ (⊤∖↑lftN) with "[Hbor]"); try done.
@@ -132,7 +127,7 @@ Section borrow.
iMod ("Hclose'" with "[H↦]") as "[H↦ Htok]"; first by auto.
iMod ("Hclose" with "Htok") as "($ & $)".
rewrite tctx_interp_singleton tctx_hasty_val' //.
- iExists _. iSplitR; first by auto. iApply (bor_shorten with "[] Hbor").
+ iApply (bor_shorten with "[] Hbor").
iApply (lft_incl_glb with "Hincl"). iApply lft_incl_refl.
Qed.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 23c75dd3..7f91f578 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -158,7 +158,8 @@ Section lft_contexts.
Proof.
iIntros "#LFT Hκ". rewrite /llctx_elt_interp /=. (* TODO: Why is this unfold necessary? *)
iDestruct "Hκ" as (κ) "(% & Hκ & _)".
- iMod (bor_create _ κ2 with "LFT [Hκ]") as "[Hκ _]"; first done; first by iFrame.
+ iMod (bor_create _ κ2 (qL).[κ] with "LFT [Hκ]") as "[Hκ _]";
+ first done; first by iFrame.
iMod (bor_fracture (λ q, (qL * q).[_])%I with "LFT [Hκ]") as "#Hκ"; first done.
{ rewrite Qp_mult_1_r. done. }
iModIntro. subst κ1. iSplit.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index fc08cf18..a47facfe 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -146,12 +146,9 @@ Section product_split.
iIntros (tid q1 q2) "#LFT $ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
iDestruct "H" as ([[]|]) "[Hp H]"; try iDestruct "H" as "[]". iDestruct "Hp" as %Hp.
- iDestruct "H" as (P) "[#HPiff HP]".
- iMod (bor_iff with "LFT [] HP") as "Hown". set_solver. by eauto.
- rewrite /= split_prod_mt. iMod (bor_sep with "LFT Hown") as "[H1 H2]".
+ rewrite /= split_prod_mt. iMod (bor_sep with "LFT H") as "[H1 H2]".
set_solver. rewrite /tctx_elt_interp /=.
- iSplitL "H1"; iExists _; (iSplitR; first by rewrite Hp);
- iExists _; erewrite <-uPred.iff_refl; auto.
+ iSplitL "H1"; iExists _; (iSplitR; first by rewrite Hp); auto.
Qed.
Lemma tctx_merge_uniq_prod2 E L p κ ty1 ty2 :
@@ -162,13 +159,9 @@ Section product_split.
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 H1]";
try iDestruct "H1" as "[]". iDestruct "Hp1" as %Hp1.
- iDestruct "H1" as (P) "[#HPiff HP]".
- iMod (bor_iff with "LFT [] HP") as "Hown1". set_solver. by eauto.
iDestruct "H2" as (v2) "(Hp2 & H2)". rewrite /= Hp1. iDestruct "Hp2" as %[=<-].
- iDestruct "H2" as (Q) "[#HQiff HQ]".
- iMod (bor_iff with "LFT [] HQ") as "Hown2". set_solver. by eauto.
- iExists #l. iFrame "%". iExists _. erewrite <-uPred.iff_refl; auto. iSplitR. done.
- rewrite split_prod_mt. iApply (bor_combine with "LFT Hown1 Hown2"). set_solver.
+ iExists #l. iFrame "%". iMod (bor_combine with "LFT H1 H2") as "H". set_solver.
+ by rewrite /= split_prod_mt.
Qed.
Lemma uniq_is_ptr κ ty tid (vl : list val) :
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 419447bb..2d21fb76 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -66,9 +66,8 @@ Section case.
iIntros (Halive Hel) "!#". iIntros (tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try iDestruct "Hp" as "[]".
- iDestruct "Hp" as (P) "[HP Hb]". iMod (bor_iff with "LFT HP Hb") as "Hb". done.
iMod (Halive with "HE HL") as (q) "[Htok Hclose]". done.
- iMod (bor_acc_cons with "LFT Hb Htok") as "[H↦ Hclose']". done.
+ iMod (bor_acc_cons with "LFT Hp Htok") as "[H↦ Hclose']". done.
iDestruct "H↦" as (vl) "[H↦ Hown]".
iDestruct "Hown" as (i vl' vl'') "(>% & >EQlen & Hown)". subst.
iDestruct "EQlen" as %[=EQlen].
@@ -90,8 +89,7 @@ Section case.
rewrite /= -EQlen !app_length EQlenvl' EQlenvl'2 nth_lookup EQty /=. auto. }
iMod ("Hclose" with "Htok") as "[HE HL]".
iApply (Hety with "HEAP LFT Hna HE HL HC").
- rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //. iFrame "HT".
- iExists _. erewrite <-uPred.iff_refl. auto.
+ rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //. iFrame.
- iMod ("Hclose'" with "* [H↦i H↦vl' H↦vl'' Hown] []") as "[Hb Htok]";
[|by iIntros "!>$"|].
{ iExists (#i::vl'++vl'').
@@ -99,8 +97,7 @@ Section case.
iExists i, vl', vl''. rewrite nth_lookup EQty. auto. }
iMod ("Hclose" with "Htok") as "[HE HL]".
iApply (Hety with "HEAP LFT Hna HE HL HC").
- rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //. iFrame "HT".
- iExists _. erewrite <-uPred.iff_refl. auto.
+ rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //. iFrame.
Qed.
Lemma type_case_uniq E L C T T' p κ tyl el :
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 5a40d780..e9292f81 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -11,17 +11,9 @@ Section uniq_bor.
Program Definition uniq_bor (κ:lft) (ty:type) :=
{| ty_size := 1;
- (* We quantify over [P]s so that the Proper lemma
- (wrt. subtyping) works without an update.
-
- An obvious alternative definition would be to allow
- an update in the ownership here, i.e. `|={lftE}=> &{κ} P`.
- The trouble with this definition is that bor_unnest as proven is too
- weak. The original unnesting with open borrows was strong enough. *)
ty_own tid vl :=
match vl return _ with
- | [ #(LitLoc l) ] =>
- ∃ P, ▷ □ (P ↔ l ↦∗: ty.(ty_own) tid) ∗ &{κ} P
+ | [ #(LitLoc l) ] => &{κ} l ↦∗: ty.(ty_own) tid
| _ => False
end%I;
ty_shr κ' tid l :=
@@ -37,21 +29,16 @@ Section uniq_bor.
iMod (bor_exists with "LFT Hshr") as ([|[[|l'|]|][]]) "Hb"; first set_solver;
(iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]"; first set_solver);
try (iMod (bor_persistent_tok with "LFT Hb2 Htok") as "[>[] _]"; set_solver).
- iMod (bor_exists with "LFT Hb2") as (P) "Hb2". set_solver.
- iMod (bor_sep with "LFT Hb2") as "[H Hb2]". set_solver.
- iMod (bor_persistent_tok with "LFT H Htok") as "[#HPiff $]". set_solver.
- iExists l'. subst. rewrite heap_mapsto_vec_singleton.
+ iFrame. iExists l'. subst. rewrite heap_mapsto_vec_singleton.
iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "$". set_solver.
rewrite {1}bor_unfold_idx. iDestruct "Hb2" as (i) "[#Hpb Hpbown]".
iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty (κ∪κ') tid l')%I
with "[Hpbown]") as "#Hinv"; first by eauto.
iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- - iMod (bor_unnest _ _ _ P with "LFT [Hbtok]") as "Hb". solve_ndisj.
+ - iMod (bor_unnest with "LFT [Hbtok]") as "Hb". solve_ndisj.
{ iApply bor_unfold_idx. eauto. }
iModIntro. iNext. iMod "Hb".
- iMod (bor_iff with "LFT [] Hb") as "Hb". solve_ndisj.
- { by eauto. }
iMod (ty.(ty_share) with "LFT Hb Htok") as "[#Hshr $]". solve_ndisj.
iMod ("Hclose" with "[]") as "_"; auto.
- iMod ("Hclose" with "[]") as "_". by eauto.
@@ -76,17 +63,13 @@ Section uniq_bor.
Global Instance uniq_mono E L :
Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) uniq_bor.
Proof.
- intros κ1 κ2 Hκ ty1 ty2 [Hty1 Hty2]. iIntros. iSplit; first done.
- iDestruct (Hty1 with "* [] [] []") as "(_ & #Ho1 & #Hs1)"; [done..|clear Hty1].
- iDestruct (Hty2 with "* [] [] []") as "(_ & #Ho2 & #Hs2)"; [done..|clear Hty2].
- iDestruct (Hκ with "[] []") as "#Hκ"; [done..|].
- iSplit; iAlways.
+ intros κ1 κ2 Hκ ty1 ty2 Hty%eqtype_unfold. iIntros. iSplit; first done.
+ iDestruct (Hty with "* [] [] []") as "(_ & #Ho & #Hs)"; [done..|clear Hty].
+ iDestruct (Hκ with "[] []") as "#Hκ"; [done..|]. iSplit; iAlways.
- iIntros (? [|[[]|][]]) "H"; try iDestruct "H" as "[]".
- iDestruct "H" as (P) "[#HPiff Hown]". iExists _.
- iSplitR; last by iApply (bor_shorten with "Hκ"). iNext.
- iIntros "!#". iSplit; iIntros "H".
- + iDestruct ("HPiff" with "H") as (vl) "[??]". iExists vl. iFrame. by iApply "Ho1".
- + iDestruct "H" as (vl) "[??]". iApply "HPiff". iExists vl. iFrame. by iApply "Ho2".
+ iApply (bor_shorten with "Hκ"). iApply (bor_iff_proper with "[] H").
+ iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]";
+ iExists vl; iFrame; by iApply "Ho".
- iIntros (κ ??) "H". iAssert (κ2 ∪ κ ⊑ κ1 ∪ κ)%I as "#Hincl'".
{ iApply (lft_incl_glb with "[] []").
- iApply (lft_incl_trans with "[] Hκ"). iApply lft_le_incl.
@@ -96,7 +79,7 @@ Section uniq_bor.
iMod (lft_incl_acc with "Hincl' Htok") as (q') "[Htok Hclose]"; first set_solver.
iMod ("Hupd" with "* [%] Htok") as "Hupd'"; try done. iModIntro. iNext.
iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
- iApply (ty_shr_mono with "[] Hincl'"); [done..|]. by iApply "Hs1".
+ iApply (ty_shr_mono with "[] Hincl'"); [done..|]. by iApply "Hs".
Qed.
Global Instance uniq_mono_flip E L :
Proper (lctx_lft_incl E L ==> eqtype E L ==> flip (subtype E L)) uniq_bor.
@@ -119,11 +102,8 @@ Section uniq_bor.
Send ty → Send (uniq_bor κ ty).
Proof.
iIntros (Hsend tid1 tid2 [|[[]|][]]) "H"; try iDestruct "H" as "[]".
- iDestruct "H" as (P) "[#HPiff H]". iExists _. iFrame. iNext. iAlways. iSplit.
- - iIntros "HP". iApply (heap_mapsto_pred_wand with "[HP]").
- { by iApply "HPiff". } { iIntros (vl). by iApply Hsend. }
- - iIntros "HP". iApply "HPiff". iApply (heap_mapsto_pred_wand with "HP").
- iIntros (vl). by iApply Hsend.
+ iApply (bor_iff_proper with "[] H"). iNext. iAlways. iApply uPred.equiv_iff.
+ do 3 f_equiv. iSplit; iIntros "."; by iApply Hsend.
Qed.
Global Instance uniq_sync κ ty :
@@ -157,9 +137,7 @@ Section typing.
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; [try done..|].
rewrite !tctx_interp_singleton /=.
iDestruct "Huniq" as ([[]|]) "[% Huniq]"; try iDestruct "Huniq" as "[]".
- iDestruct "Huniq" as (P) "[#HPiff HP]".
- iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
- iMod (ty.(ty_share) with "LFT H↦ Htok") as "[Hown Htok]"; [solve_ndisj|].
+ iMod (ty.(ty_share) with "LFT Huniq Htok") as "[Hown Htok]"; [solve_ndisj|].
iMod ("Hclose" with "Htok") as "[$ $]". iExists _. by iFrame "%∗".
Qed.
@@ -172,13 +150,9 @@ Section typing.
iDestruct (llctx_interp_persist with "HL") as "#HL'". iFrame "HE HL".
iDestruct (Hκκ' with "HE' HL'") as "Hκκ'".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
- iDestruct "H" as ([[]|]) "[% Hown]"; try iDestruct "Hown" as "[]".
- iDestruct "Hown" as (P) "[#Hiff Hb]".
- iMod (bor_iff with "LFT [] Hb") as "Hb". done. by eauto.
- iMod (rebor with "LFT Hκκ' Hb") as "[Hb Hext]". done. iModIntro. iSplitL "Hb".
- - iExists _. iSplit. done. iExists _. erewrite <-uPred.iff_refl. eauto.
- - iExists _. iSplit. done. iIntros "#H†". iMod ("Hext" with "H†") as "Hb".
- iExists _. erewrite <-uPred.iff_refl. eauto.
+ iDestruct "H" as ([[]|]) "[% Hb]"; try iDestruct "Hb" as "[]".
+ iMod (rebor with "LFT Hκκ' Hb") as "[Hb Hext]". done. iModIntro.
+ iSplitL "Hb"; iExists _; auto.
Qed.
(* When sharing during extraction, we do the (arbitrary) choice of
@@ -224,32 +198,28 @@ Section typing.
Copy ty → lctx_lft_alive E L κ → typed_read E L (&uniq{κ}ty) ty (&uniq{κ}ty).
Proof.
iIntros (Hcopy Halive) "!#". iIntros ([[]|] tid F qE qL ?) "#LFT Htl HE HL Hown";
- try iDestruct "Hown" as "[]". iDestruct "Hown" as (P) "[#HP H↦]".
+ try iDestruct "Hown" as "[]".
iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first set_solver.
- iMod (bor_iff with "LFT [] H↦") as "H↦". set_solver. by eauto.
- iMod (bor_acc with "LFT H↦ Hκ") as "[H↦ Hclose']"; first set_solver.
+ iMod (bor_acc with "LFT Hown Hκ") as "[H↦ Hclose']"; first set_solver.
iDestruct "H↦" as (vl) "[>H↦ #Hown]".
iDestruct (ty_size_eq with "Hown") as "#>%". iIntros "!>".
iExists _, _, _. iSplit; first done. iFrame "∗#". iIntros "H↦".
- iMod ("Hclose'" with "[H↦]") as "[H↦ Htok]". by iExists _; iFrame.
- iMod ("Hclose" with "Htok") as "($ & $ & $)".
- iExists _. erewrite <-uPred.iff_refl. auto.
+ iMod ("Hclose'" with "[H↦]") as "[$ Htok]". by iExists _; iFrame.
+ by iMod ("Hclose" with "Htok") as "($ & $ & $)".
Qed.
Lemma write_uniq E L κ ty :
lctx_lft_alive E L κ → typed_write E L (&uniq{κ}ty) ty (&uniq{κ}ty).
Proof.
iIntros (Halive) "!#". iIntros ([[]|] tid F qE qL ?) "#LFT HE HL Hown";
- try iDestruct "Hown" as "[]". iDestruct "Hown" as (P) "[#HP H↦]".
+ try iDestruct "Hown" as "[]".
iMod (Halive with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
- iMod (bor_iff with "LFT [] H↦") as "H↦". set_solver. by eauto.
- iMod (bor_acc with "LFT H↦ Htok") as "[H↦ Hclose']". set_solver.
+ iMod (bor_acc with "LFT Hown Htok") as "[H↦ Hclose']". set_solver.
iDestruct "H↦" as (vl) "[>H↦ Hown]". rewrite ty.(ty_size_eq).
iDestruct "Hown" as ">%". iModIntro. iExists _, _. iSplit; first done.
iFrame. iIntros "Hown". iDestruct "Hown" as (vl') "[H↦ Hown]".
- iMod ("Hclose'" with "[H↦ Hown]") as "[Hbor Htok]". by iExists _; iFrame.
- iMod ("Hclose" with "Htok") as "($ & $ & $)".
- iExists _. erewrite <-uPred.iff_refl. auto.
+ iMod ("Hclose'" with "[H↦ Hown]") as "[$ Htok]". by iExists _; iFrame.
+ by iMod ("Hclose" with "Htok") as "($ & $ & $)".
Qed.
End typing.
--
GitLab