From be413807f5e68357176a3ffb2a38254a13e4b28c Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 21 Aug 2017 15:59:29 +0200
Subject: [PATCH] Simplify proofs
---
theories/lifetime/model/reborrow.v | 5 ++---
theories/typing/type.v | 6 ++----
2 files changed, 4 insertions(+), 7 deletions(-)
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index e9d9674a..4706eb2e 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -60,7 +60,7 @@ 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 Hκ". iSplitL "Hj".
+ 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).
@@ -123,8 +123,7 @@ Proof.
iMod (slice_empty _ _ true with "Hs' Hbox") as "[Hidx Hbox]".
solve_ndisj. by rewrite lookup_fmap EQB.
iAssert (▷ idx_bor_own 1 (κ, i))%I with "[Hidx]" as ">Hidx"; [by iApply "HP'"|].
- iDestruct (raw_bor_inI _ _ P with "HI [Hidx]") as %HI;
- first by rewrite /raw_bor; auto 10 with I.
+ iDestruct (own_bor_auth with "HI [Hidx]") as %HI; [by rewrite /idx_bor_own|].
iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinvκ Hclose']";
first by rewrite elem_of_difference elem_of_dom not_elem_of_singleton;
eauto using strict_ne.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 091e9dc6..2774efcd 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -134,10 +134,8 @@ Next Obligation.
iIntros (?? st E κ l tid ??) "#LFT Hmt Hκ".
iMod (bor_exists with "LFT Hmt") as (vl) "Hmt"; first solve_ndisj.
iMod (bor_sep with "LFT Hmt") as "[Hmt Hown]"; first solve_ndisj.
- iMod (bor_persistent with "LFT Hown") as "[Hown|#H†]"; first solve_ndisj.
- - iFrame "Hκ".
- iMod (bor_fracture with "LFT [Hmt]") as "Hfrac"; by eauto with iFrame.
- - iExFalso. by iApply (lft_tok_dead with "Hκ").
+ iMod (bor_persistent_tok with "LFT Hown Hκ") as "[Hown $]"; first solve_ndisj.
+ iMod (bor_fracture with "LFT [Hmt]") as "Hfrac"; by eauto with iFrame.
Qed.
Next Obligation.
iIntros (?? st κ κ' tid l) "#Hord H".
--
GitLab