From 0dafeb8340c5d60ab12d3cd738e8f463b2121dea Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 14 Mar 2024 12:14:05 +0100
Subject: [PATCH] WIP.

---
 iris/algebra/reservation_map.v |  6 ++++++
 iris/base_logic/lib/gen_heap.v | 12 ++++++++++++
 2 files changed, 18 insertions(+)

diff --git a/iris/algebra/reservation_map.v b/iris/algebra/reservation_map.v
index 37b32e3b9..cdebeae48 100644
--- a/iris/algebra/reservation_map.v
+++ b/iris/algebra/reservation_map.v
@@ -253,6 +253,12 @@ Section cmra.
     - by rewrite left_id.
     - intros i. rewrite lookup_op lookup_empty. auto.
   Qed.
+  Lemma reservation_map_token_data_valid E k a :
+    k ∈ E → ✓ (reservation_map_token E ⋅ reservation_map_data k a) → False.
+  Proof.
+    rewrite reservation_map_valid_eq /= right_id_L left_id_L.
+    move=> ? [_] /(_ k). rewrite lookup_singleton. set_solver.
+  Qed.
 
   Lemma reservation_map_alloc E k a :
     k ∈ E → ✓ a → reservation_map_token E ~~> reservation_map_data k a.
diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 680d6c7ff..f06c87a93 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -260,6 +260,18 @@ Section gen_heap.
     rewrite namespaces.nclose_unseal. apply elem_coPset_suffixes.
     exists 1%positive. by rewrite left_id_L.
   Qed.
+  Lemma meta_token_meta `{Countable A} E l (x : A) N :
+    ↑ N ⊆ E → meta_token l E -∗ meta l N x -∗ False.
+  Proof.
+    rewrite meta_token_unseal meta_unseal /meta_token_def /meta_def.
+    iIntros (?) "(%γm & Hγm & Hm) (%γm' & Hγm' & Hm')".
+    iCombine "Hγm Hγm'" gives %[_ <-].
+    iCombine "Hm Hm'" gives %[]%reservation_map_token_data_valid.
+    (* Same as what's proven above, at line 258; factor into lemma *)
+    cut (positives_flatten N ∈@{coPset} ↑N); first by set_solver.
+    rewrite namespaces.nclose_unseal. apply elem_coPset_suffixes.
+    exists 1%positive. by rewrite left_id_L.
+  Qed.
 
   (** Update lemmas *)
   Lemma gen_heap_alloc σ l v :
-- 
GitLab