From 85b891cb4699ee792dbefdace4ab1d39bd1c415d Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Fri, 17 Apr 2020 14:35:08 -0500
Subject: [PATCH] Add filter_app lemma
---
theories/list.v | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/theories/list.v b/theories/list.v
index 3285b173..bf29b3ce 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1656,6 +1656,13 @@ Section filter.
Lemma filter_cons_False x l : ¬P x → filter P (x :: l) = filter P l.
Proof. intros. by rewrite filter_cons, decide_False. Qed.
+ Lemma filter_app l1 l2 : filter P (l1 ++ l2) = filter P l1 ++ filter P l2.
+ Proof.
+ induction l1 as [|x l1 IH]; simpl; [done| ].
+ case_decide; [|done].
+ by rewrite IH.
+ Qed.
+
Lemma elem_of_list_filter l x : x ∈ filter P l ↔ P x ∧ x ∈ l.
Proof.
induction l; simpl; repeat case_decide;
--
GitLab