From 75700c3109ecf3ff948ef64348beea1d6950db4b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 16 Apr 2022 19:15:17 -0400
Subject: [PATCH] add big_sepS_insert_2' and big_sepS_union_2

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

diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 3fd8c6016..a9c253821 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -2548,6 +2548,21 @@ Section gset.
     replace ({[x]} ∪ X) with X by set_solver.
     auto.
   Qed.
+  Lemma big_sepS_insert_2' {Φ X} x
+    `{!TCOr (Affine (Φ x)) (Absorbing (Φ x))} :
+    Φ x -∗ ([∗ set] y ∈ X, Φ y) -∗ ([∗ set] y ∈ X ∪ {[ x ]}, Φ y).
+  Proof. rewrite comm_L. by apply big_sepS_insert_2. Qed.
+
+  Lemma big_sepS_union_2 {Φ} X Y `{!∀ x, Affine (Φ x)} :
+    ([∗ set] y ∈ X, Φ y) -∗ ([∗ set] y ∈ Y, Φ y) -∗ ([∗ set] y ∈ X ∪ Y, Φ y).
+  Proof.
+    apply wand_intro_r.
+    rewrite -difference_union_L.
+    rewrite big_sepS_union; last set_solver.
+    apply sep_mono_l.
+    apply big_sepS_subseteq; first done.
+    set_solver.
+  Qed.
 
   Lemma big_sepS_delete_2 {Φ X} x :
     Affine (Φ x) →
-- 
GitLab