From 38d619518a19e101804e251f3fd714e76cb33d3d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 29 Nov 2016 23:28:00 +0100
Subject: [PATCH] Prove "filter" accessor for big_sepS.

---
 base_logic/big_op.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/base_logic/big_op.v b/base_logic/big_op.v
index d09749fd9..67c73bcc7 100644
--- a/base_logic/big_op.v
+++ b/base_logic/big_op.v
@@ -526,6 +526,17 @@ Section gset.
       by rewrite !big_sepS_insert // IH pure_False // False_impl left_id.
   Qed.
 
+  Lemma big_sepS_filter_acc (P : A → Prop) `{∀ y, Decision (P y)} Φ X Y :
+    (∀ y, y ∈ Y → P y → y ∈ X) →
+    ([∗ set] y ∈ X, Φ y) -∗
+      ([∗ set] y ∈ Y, ⌜P y⌝ → Φ y) ∗
+      (([∗ set] y ∈ Y, ⌜P y⌝ → Φ y) -∗ [∗ set] y ∈ X, Φ y).
+  Proof.
+    intros ?. destruct (proj1 (subseteq_disjoint_union_L (filter P Y) X))
+      as (Z&->&?); first set_solver.
+    rewrite big_sepS_union // big_sepS_filter. by apply sep_mono_r, wand_intro_l.
+  Qed.
+
   Lemma big_sepS_sepS Φ Ψ X :
     ([∗ set] y ∈ X, Φ y ∗ Ψ y) ⊣⊢ ([∗ set] y ∈ X, Φ y) ∗ ([∗ set] y ∈ X, Ψ y).
   Proof. apply: big_opS_opS. Qed.
-- 
GitLab