From 566e5d61dec3ad8cf57da309d9e90665c9671cea Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 16 Aug 2017 23:36:57 +0200
Subject: [PATCH] Be more coherent in lft_kill by naming K and K' the same way
they are named in lfts_kill
---
theories/lifetime/model/creation.v | 14 +++++++-------
1 file changed, 7 insertions(+), 7 deletions(-)
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 50c25adc..2d9ef1ab 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -13,13 +13,13 @@ Implicit Types κ : lft.
Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) :
let Iinv := (
own_ilft_auth I ∗
- ([∗ set] κ' ∈ K, lft_inv_alive κ') ∗
- ([∗ set] κ' ∈ K', lft_inv_dead κ'))%I in
- (∀ κ', is_Some (I !! κ') → κ' ⊂ κ → κ' ∈ K) →
- (∀ κ', is_Some (I !! κ') → κ ⊂ κ' → κ' ∈ K') →
+ ([∗ set] κ' ∈ K, lft_inv_dead κ') ∗
+ ([∗ set] κ' ∈ K', lft_inv_alive κ'))%I in
+ (∀ κ', is_Some (I !! κ') → κ ⊂ κ' → κ' ∈ K) →
+ (∀ κ', is_Some (I !! κ') → κ' ⊂ κ → κ' ∈ K') →
Iinv -∗ lft_inv_alive κ -∗ [†κ] ={↑borN ∪ ↑inhN}=∗ Iinv ∗ lft_inv_dead κ.
Proof.
- iIntros (Iinv HK HK') "(HI & Halive & Hdead) Hlalive Hκ".
+ iIntros (Iinv HK HK') "(HI & Hdead & Halive) Hlalive Hκ".
rewrite lft_inv_alive_unfold;
iDestruct "Hlalive" as (P Q) "(Hbor & Hvs & Hinh)".
rewrite /lft_bor_alive; iDestruct "Hbor" as (B) "(Hbox & Hbor & HB)".
@@ -94,12 +94,12 @@ Proof.
iDestruct (@big_sepS_insert with "Halive") as "[Hκalive Halive]"; first done.
iMod (lft_kill with "[$HI $Halive $Hdead] Hκalive Hκ")
as "[(HI&Halive&Hdead) Hκdead]".
+ { intros κ' ? [??]%strict_spec_alt.
+ rewrite elem_of_difference elem_of_singleton; eauto. }
{ intros κ' ??. eapply (HK' κ); eauto.
intros ?. eapply (minimal_strict_1 _ _ _ Hκmin); eauto.
apply elem_of_filter; split; last done.
eapply lft_alive_in_subseteq, gmultiset_subset_subseteq; eauto. }
- { intros κ' ? [??]%strict_spec_alt.
- rewrite elem_of_difference elem_of_singleton; eauto. }
iModIntro. rewrite /Iinv (big_sepS_delete _ K) //. iFrame.
Qed.
--
GitLab