From c65aad415bd3fcd94de0280eb0596f3635e358ab Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 5 Dec 2016 23:59:03 +0100
Subject: [PATCH] List big op is compatible with permutations.

---
 algebra/cmra_big_op.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v
index ce7886b01..8a4160431 100644
--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -154,6 +154,13 @@ Section list.
     (∀ k y, l !! k = Some y → f k y ≡ g k y) →
     ([⋅ list] k ↦ y ∈ l, f k y) ≡ ([⋅ list] k ↦ y ∈ l, g k y).
   Proof. apply big_opL_forall; apply _. Qed.
+  Lemma big_opL_permutation (f : A → M) l1 l2 :
+    l1 ≡ₚ l2 → ([⋅ list] x ∈ l1, f x) ≡ ([⋅ list] x ∈ l2, f x).
+  Proof.
+    assert (∀ l, imap (λ _ x, f x) l = map f l) as EQ;
+      last by rewrite /big_opL !EQ=>->.
+    intros l; revert f. induction l as [|?? IH]=>// f. rewrite imap_cons IH //.
+  Qed.
 
   Global Instance big_opL_ne l n :
     Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
-- 
GitLab