From 1ddf17971170961d3872c66b6a3bfa26448b055e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 23 Sep 2022 14:45:39 +0200
Subject: [PATCH] Add lemma `filter_app_complement`.

---
 stdpp/list.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/stdpp/list.v b/stdpp/list.v
index 9a084b61..ef5efe4f 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -2033,6 +2033,13 @@ Section filter.
     rewrite reverse_cons, filter_app, IHl, !filter_cons.
     case_decide; [by rewrite reverse_cons|by rewrite filter_nil, app_nil_r].
   Qed.
+
+  Lemma filter_app_complement l : filter P l ++ filter (λ x, ¬P x) l ≡ₚ l.
+  Proof.
+    induction l as [|x l IH]; simpl; [done|]. case_decide.
+    - rewrite decide_False by naive_solver. simpl. by rewrite IH.
+    - rewrite decide_True by done. by rewrite <-Permutation_middle, IH.
+  Qed.
 End filter.
 
 Lemma list_filter_iff (P1 P2 : A → Prop)
-- 
GitLab