From baa59834ceb36f85fe9958e0dfb3530eed2e3ef6 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Tue, 25 Oct 2016 17:04:48 +0200
Subject: [PATCH] Simplify its proof.
---
perm_incl.v | 9 ++-------
1 file changed, 2 insertions(+), 7 deletions(-)
diff --git a/perm_incl.v b/perm_incl.v
index 3f46d966..4d5dd845 100644
--- a/perm_incl.v
+++ b/perm_incl.v
@@ -230,15 +230,10 @@ Section props.
iDestruct "Hown" as (l') "[EQ [Hf Hown]]". iDestruct "EQ" as %[=]. subst l'.
iVs (lft_borrow_create with "Hκ Hown") as "[Hbor Hextract]". done.
iSplitL "Hbor". by simpl; eauto.
- assert ((Some #l ◁ own q ty)%P tid ⊣⊢
- ▷ †{q}l…ty_size ty ★ ▷ l ↦★: ty_own ty tid) as ->.
- { iSplit; iIntros "H/=".
- - iDestruct "H" as (l') "[EQ [Hf Hown]]". iDestruct "EQ" as %[=]. subst l'.
- by iFrame.
- - iExists _. eauto. }
iVs (lft_borrow_create with "Hκ Hf") as "[_ Hf]". done.
iVs (lft_extract_combine with "[-]"). done. by iFrame.
- iVsIntro. iApply lft_extract_mono; last done. by iDestruct 1 as "[$$]".
+ iVsIntro. iApply lft_extract_mono; last done.
+ iIntros "H/=". iExists _. iSplit. done. by iDestruct "H" as "[$$]".
Qed.
Lemma reborrow_uniq_borrowing κ κ' v ty :
--
GitLab