From edfdba1518abb44fabe93e1b267e4608a74eae30 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Mon, 26 Aug 2019 12:43:28 +0200
Subject: [PATCH] Add `big_sepL2_swap`

---
 theories/bi/big_op.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index c7dda09a6..6120bf009 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -1475,6 +1475,13 @@ Section list2.
     auto using and_mono, laterN_intro.
   Qed.
 
+  Lemma big_sepL2_flip Φ l1 l2 :
+    ([∗ list] k↦y1;y2 ∈ l2; l1, Φ k y2 y1) ⊣⊢ ([∗ list] k↦y1;y2 ∈ l1; l2, Φ k y1 y2).
+  Proof.
+    revert Φ l2. induction l1 as [|x1 l1 IH]=> Φ -[|x2 l2]//=; simplify_eq.
+    by rewrite IH.
+  Qed.
+
   Global Instance big_sepL2_nil_timeless `{!Timeless (emp%I : PROP)} Φ :
     Timeless ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2).
   Proof. simpl; apply _. Qed.
@@ -1541,6 +1548,14 @@ Section gmap2.
     apply big_sepM2_mono. eauto.
   Qed.
 
+  Lemma big_sepM2_flip Φ m1 m2 :
+    ([∗ map] k↦y1;y2 ∈ m2; m1, Φ k y2 y1) ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2).
+  Proof.
+    rewrite /big_sepM2. apply and_proper; [apply pure_proper; naive_solver |].
+    rewrite -map_zip_with_flip map_zip_with_map_zip big_sepM_fmap.
+    apply big_sepM_proper. by intros k [b a].
+  Qed.
+
   Global Instance big_sepM2_empty_timeless `{!Timeless (emp%I : PROP)} Φ :
     Timeless ([∗ map] k↦x1;x2 ∈ ∅;∅, Φ k x1 x2).
   Proof. rewrite /big_sepM2 map_zip_with_empty. apply _. Qed.
-- 
GitLab