From 1270ae088a1b95d71fb9dbbfc4a63e9939de6570 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 28 Sep 2016 14:05:06 +0200
Subject: [PATCH] Leibniz equality variants of the commute lemmas for big ops.

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

diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v
index 335174fb7..9e55a3ae2 100644
--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -427,3 +427,30 @@ Proof.
   - by rewrite !big_opS_insert // !big_opS_empty !right_id.
   - by rewrite !big_opS_insert // cmra_homomorphism -IH //.
 Qed.
+
+Lemma big_opL_commute_L {M1 M2 : ucmraT} `{!LeibnizEquiv M2} {A}
+    (h : M1 → M2) `{!UCMRAHomomorphism h} (f : nat → A → M1) l :
+  h ([⋅ list] k↦x ∈ l, f k x) = ([⋅ list] k↦x ∈ l, h (f k x)).
+Proof. unfold_leibniz. by apply big_opL_commute. Qed.
+Lemma big_opL_commute1_L {M1 M2 : ucmraT} `{!LeibnizEquiv M2} {A}
+    (h : M1 → M2) `{!CMRAHomomorphism h} (f : nat → A → M1) l :
+  l ≠ [] → h ([⋅ list] k↦x ∈ l, f k x) = ([⋅ list] k↦x ∈ l, h (f k x)).
+Proof. unfold_leibniz. by apply big_opL_commute1. Qed.
+
+Lemma big_opM_commute_L {M1 M2 : ucmraT} `{!LeibnizEquiv M2, Countable K} {A}
+    (h : M1 → M2) `{!UCMRAHomomorphism h} (f : K → A → M1) m :
+  h ([⋅ map] k↦x ∈ m, f k x) = ([⋅ map] k↦x ∈ m, h (f k x)).
+Proof. unfold_leibniz. by apply big_opM_commute. Qed.
+Lemma big_opM_commute1_L {M1 M2 : ucmraT} `{!LeibnizEquiv M2, Countable K} {A}
+    (h : M1 → M2) `{!CMRAHomomorphism h} (f : K → A → M1) m :
+  m ≠ ∅ → h ([⋅ map] k↦x ∈ m, f k x) = ([⋅ map] k↦x ∈ m, h (f k x)).
+Proof. unfold_leibniz. by apply big_opM_commute1. Qed.
+
+Lemma big_opS_commute_L {M1 M2 : ucmraT} `{!LeibnizEquiv M2, Countable A}
+    (h : M1 → M2) `{!UCMRAHomomorphism h} (f : A → M1) X :
+  h ([⋅ set] x ∈ X, f x) = ([⋅ set] x ∈ X, h (f x)).
+Proof. unfold_leibniz. by apply big_opS_commute. Qed.
+Lemma big_opS_commute1_L {M1 M2 : ucmraT} `{!LeibnizEquiv M2, Countable A}
+    (h : M1 → M2) `{!CMRAHomomorphism h} (f : A → M1) X :
+  X ≠ ∅ → h ([⋅ set] x ∈ X, f x) = ([⋅ set] x ∈ X, h (f x)).
+Proof. intros. rewrite <-leibniz_equiv_iff. by apply big_opS_commute1. Qed.
-- 
GitLab