Merge branch 'robbert/iRewrite_dom' into 'master'

Define `Proper` for `dom` and enable `iRewrite` on goals involving `dom`

See merge request !754

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`,

iris/algebra/gmap.v

 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 :

tests/proofmode.v

+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).