From 608e43feb89f023001142a24a06a612aad0b5393 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Mon, 9 May 2022 13:01:08 +0000
Subject: [PATCH] strengthen big_sepS_union_2

---
 iris/bi/big_op.v | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index a9c253821..3ec0cdccf 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -2553,15 +2553,18 @@ Section gset.
     Φ 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)} :
+  Lemma big_sepS_union_2 {Φ} X Y
+    `{!∀ x, TCOr (Affine (Φ x)) (Absorbing (Φ 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.
+    apply wand_intro_r. induction X as [|x X ? IH] using set_ind_L.
+    { by rewrite left_id_L big_sepS_empty left_id. }
+    rewrite big_sepS_insert // -assoc IH -assoc_L.
+    destruct (decide (x ∈ Y)).
+    { replace ({[x]} ∪ (X ∪ Y)) with (X ∪ Y) by set_solver.
+      rewrite (big_sepS_delete _ _ x); last set_solver.
+      by rewrite assoc sep_elim_r. }
+    by rewrite big_sepS_insert; last set_solver.
   Qed.
 
   Lemma big_sepS_delete_2 {Φ X} x :
-- 
GitLab