From 64843223117124d45708f2ed2d0617a76a20c701 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 8 Jun 2021 00:44:59 +0200
Subject: [PATCH] Add lemmas `disjoint_filter_complement` and
 `filter_union_complement` (analogous to maps).

---
 theories/fin_sets.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 21c20ecb..2aaa7c53 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -328,6 +328,10 @@ Section filter.
   Proof. set_solver. Qed.
   Lemma filter_union X Y : filter P (X ∪ Y) ≡ filter P X ∪ filter P Y.
   Proof. set_solver. Qed.
+  Lemma disjoint_filter_complement X : filter P X ## filter (λ x, ¬P x) X.
+  Proof. set_solver. Qed.
+  Lemma filter_union_complement X : filter P X ∪ filter (λ x, ¬P x) X ≡ X.
+  Proof. intros x. destruct (decide (P x)); set_solver. Qed.
 
   Section leibniz_equiv.
     Context `{!LeibnizEquiv C}.
@@ -340,6 +344,8 @@ Section filter.
 
     Lemma filter_union_L X Y : filter P (X ∪ Y) = filter P X ∪ filter P Y.
     Proof. unfold_leibniz. apply filter_union. Qed.
+    Lemma filter_union_complement_L X Y : filter P X ∪ filter (λ x, ¬P x) X = X.
+    Proof. unfold_leibniz. apply filter_union_complement. Qed.
   End leibniz_equiv.
 End filter.
 
-- 
GitLab