From 4b897d12d0fdcb87728c2fa6965a2786eeca57cd Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Thu, 1 Nov 2018 14:10:46 +0100
Subject: [PATCH] Add `big_opM_union` and `big_sepM_union`.

---
 theories/algebra/big_op.v | 12 ++++++++++++
 theories/bi/big_op.v      |  6 ++++++
 2 files changed, 18 insertions(+)

diff --git a/theories/algebra/big_op.v b/theories/algebra/big_op.v
index 3729d5f48..9f04dd7ed 100644
--- a/theories/algebra/big_op.v
+++ b/theories/algebra/big_op.v
@@ -241,6 +241,18 @@ Section gmap.
     ([^o map] k↦y ∈ <[i:=x]> m, <[i:=P]> f k) ≡ (P `o` [^o map] k↦y ∈ m, f k).
   Proof. apply (big_opM_fn_insert (λ _ _, id)). Qed.
 
+  Lemma big_opM_union f m1 m2 :
+    m1 ##ₘ m2 →
+    ([^o map] k↦y ∈ m1 ∪ m2, f k y) ≡ ([^o map] k↦y ∈ m1, f k y) `o` ([^o map] k↦y ∈ m2, f k y).
+  Proof.
+    intros. induction m1 as [|i x m ? IH] using map_ind.
+    { by rewrite big_opM_empty !left_id. }
+    decompose_map_disjoint.
+    rewrite -insert_union_l !big_opM_insert //;
+      last by apply lookup_union_None.
+    rewrite -assoc IH //.
+  Qed.
+
   Lemma big_opM_opM f g m :
     ([^o map] k↦x ∈ m, f k x `o` g k x)
     ≡ ([^o map] k↦x ∈ m, f k x) `o` ([^o map] k↦x ∈ m, g k x).
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index dd9e84b1c..932247668 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -626,6 +626,12 @@ Section gmap.
     ([∗ map] k↦y ∈ <[i:=x]> m, <[i:=P]> Φ k) ⊣⊢ (P ∗ [∗ map] k↦y ∈ m, Φ k).
   Proof. apply big_opM_fn_insert'. Qed.
 
+  Lemma big_sepM_union Φ m1 m2 :
+    m1 ##ₘ m2 →
+    ([∗ map] k↦y ∈ m1 ∪ m2, Φ k y)
+    ⊣⊢ ([∗ map] k↦y ∈ m1, Φ k y) ∗ ([∗ map] k↦y ∈ m2, Φ k y).
+  Proof. apply big_opM_union. Qed.
+
   Lemma big_sepM_sepM Φ Ψ m :
     ([∗ map] k↦x ∈ m, Φ k x ∗ Ψ k x)
     ⊣⊢ ([∗ map] k↦x ∈ m, Φ k x) ∗ ([∗ map] k↦x ∈ m, Ψ k x).
-- 
GitLab