From b3901a5155c1bbf3c76864fae49d59919d86cb8f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 16 Nov 2021 15:29:55 +0100
Subject: [PATCH 1/3] Add `Proper` instance for `Dom` on `gmap`.

---
 iris/algebra/gmap.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 7a7c56546..fb96b834f 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -1,5 +1,6 @@
 From stdpp Require Export list gmap.
 From iris.algebra Require Export list cmra.
+From iris.algebra Require Import gset.
 From iris.algebra Require Import updates local_updates proofmode_classes big_op.
 From iris.prelude Require Import options.
 
@@ -94,6 +95,9 @@ Lemma insert_idN n m i x :
   m !! i ≡{n}≡ Some x → <[i:=x]>m ≡{n}≡ m.
 Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
 
+Global Instance gmap_dom_ne n :
+  Proper ((≡{n}@{gmap K A}≡) ==> (=)) (dom (gset K)).
+Proof. intros m1 m2 Hm. apply set_eq=> k. by rewrite !elem_of_dom Hm. Qed.
 End ofe.
 
 Global Instance map_seq_ne {A : ofe} start :
-- 
GitLab


From 3c2d317ae3ff6bf0c9fa51ef5bf230f95abd655d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 16 Nov 2021 15:30:07 +0100
Subject: [PATCH 2/3] Add test.

---
 tests/proofmode.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 73027cdbd..66cebcc72 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,3 +1,4 @@
+From iris.algebra Require Import gmap.
 From iris.bi Require Import laterable.
 From iris.proofmode Require Import tactics intro_patterns.
 From iris.prelude Require Import options.
@@ -81,6 +82,11 @@ Proof.
   auto.
 Qed.
 
+Lemma test_iRewrite_dom `{!BiInternalEq PROP} {A : ofe} (m1 m2 : gmap nat A) :
+  m1 ≡ m2 ⊢@{PROP}
+  ⌜ dom (gset nat) m1 = dom (gset nat) m2 ⌝.
+Proof. iIntros "H". by iRewrite "H". Qed.
+
 Check "test_iDestruct_and_emp".
 Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} :
   P ∧ emp -∗ emp ∧ Q -∗ <affine> (P ∗ Q).
-- 
GitLab


From f70a6e8d3e16fd472c8d09588b201da93f759db0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 16 Nov 2021 15:57:26 +0100
Subject: [PATCH 3/3] CHANGELOG.

---
 CHANGELOG.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 100f37038..5413e760e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,6 +5,11 @@ lemma.
 
 ## Iris master
 
+**Changes in `algebra`**
+
+* Define non-expansive instance for `dom`. This, in particular, makes it
+  possible to `iRewrite` below `dom` (even if the `dom` appears in `⌜ _ ⌝`).
+
 **Changes in `bi`:**
 
 * Rename `least_fixpoint_ind` into `least_fixpoint_iter`,
-- 
GitLab