From 2969a11a09c4a8e02cd90fd6d024c77158d4e4f1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Feb 2023 12:26:35 +0100
Subject: [PATCH] Stronger version of `gmap_core_id`.

---
 iris/algebra/gmap.v | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index a7a965776..5ebe71471 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -314,11 +314,15 @@ Global Instance singleton_is_op i a a1 a2 :
   IsOp a a1 a2 → IsOp' ({[ i := a ]} : gmap K A) {[ i := a1 ]} {[ i := a2 ]}.
 Proof. rewrite /IsOp' /IsOp=> ->. by rewrite -singleton_op. Qed.
 
-Global Instance gmap_core_id m : (∀ x : A, CoreId x) → CoreId m.
+Lemma gmap_core_id m : (∀ i x, m !! i = Some x → CoreId x) → CoreId m.
 Proof.
-  intros; apply core_id_total=> i.
-  rewrite lookup_core. apply (core_id_core _).
+  intros Hcore; apply core_id_total=> i.
+  rewrite lookup_core. destruct (m !! i) as [x|] eqn:Hix; rewrite Hix; [|done].
+  by eapply Hcore.
 Qed.
+Global Instance gmap_core_id' m : (∀ x : A, CoreId x) → CoreId m.
+Proof. auto using gmap_core_id. Qed.
+
 Global Instance gmap_singleton_core_id i (x : A) :
   CoreId x → CoreId {[ i := x ]}.
 Proof. intros. by apply core_id_total, singleton_core'. Qed.
-- 
GitLab