From cbcbaf4cf8b5fcefd966dfe97b46a12458519a90 Mon Sep 17 00:00:00 2001
From: Isaac van Bakel <isaac.vanbakel@inf.ethz.ch>
Date: Mon, 9 Sep 2024 16:24:14 +0200
Subject: [PATCH] Add lft_create_atomic
This lemma exposes the fact that `lft_create` can be used to actually
produce an atomic lifetime. This version of the lemma doesn't need to
include the killing update thanks to the existence of `lft_kill_atomic`
which is always applicable for these atomic lifetimes.
This *could* replace `lft_create`, but we keep that lemma for backwards
compatibility in the API.
---
lifetime/lifetime.v | 12 ++++++++++--
1 file changed, 10 insertions(+), 2 deletions(-)
diff --git a/lifetime/lifetime.v b/lifetime/lifetime.v
index 3ed2db60..3e50e5e2 100644
--- a/lifetime/lifetime.v
+++ b/lifetime/lifetime.v
@@ -29,13 +29,21 @@ Section derived.
Context `{!invGS Σ, !lftGS Σ userE}.
Implicit Types κ : lft.
+Lemma lft_create_atomic E :
+ ↑lftN ⊆ E →
+ lft_ctx ={E}=∗ ∃ Λ, 1.[@Λ].
+Proof.
+ iIntros (?) "#LFT".
+ iMod (lft_create_strong (λ _, True) with "LFT") as (κ _) "$"=>//.
+ by apply pred_infinite_True.
+Qed.
+
Lemma lft_create E :
↑lftN ⊆ E →
lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN ∪ userE}[userE]▷=∗ [†κ]).
Proof.
iIntros (?) "#LFT".
- iMod (lft_create_strong (λ _, True) with "LFT") as (κ _) "$"=>//;
- [by apply pred_infinite_True|].
+ iMod (lft_create_atomic with "LFT") as "[% $]"=>//.
by iApply lft_kill_atomic.
Qed.
--
GitLab