From 1c0ecc8f5fd0389b1677092a48c245042b6e0072 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 2 Nov 2020 09:29:30 +0100
Subject: [PATCH] Add lemma `big_sepM2_lookup_iff`.

---
 theories/bi/big_op.v | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index dfe8408bf..9441f1a52 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -1091,11 +1091,17 @@ Section map2.
   Context `{Countable K} {A B : Type}.
   Implicit Types Φ Ψ : K → A → B → PROP.
 
+  Lemma big_sepM2_lookup_iff Φ m1 m2 :
+    ([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2) ⊢
+    ⌜ ∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k) ⌝.
+  Proof. by rewrite big_sepM2_eq /big_sepM2_def and_elim_l. Qed.
+
   Lemma big_sepM2_dom Φ m1 m2 :
-    ([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2) -∗ ⌜ dom (gset K) m1 = dom (gset K) m2 ⌝.
+    ([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2) ⊢
+    ⌜ dom (gset K) m1 = dom (gset K) m2 ⌝.
   Proof.
-    rewrite big_sepM2_eq /big_sepM2_def and_elim_l. apply pure_mono=>Hm.
-    set_unfold=>k. by rewrite !elem_of_dom.
+    rewrite big_sepM2_lookup_iff. apply pure_mono=>Hm.
+    apply elem_of_equiv_L=> k. by rewrite !elem_of_dom.
   Qed.
 
   Lemma big_sepM2_flip Φ m1 m2 :
-- 
GitLab