From 6ec65ea9cdcd4a16849e66f009440afd105ade30 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Mon, 18 Nov 2024 10:40:41 +0100
Subject: [PATCH 1/2] =?UTF-8?q?Add=20filter-=E2=89=90?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md                  |  1 +
 src/Data/List/Properties.agda | 14 +++++++++++---
 2 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b63a2e32d9..f3e17fa961 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -185,6 +185,7 @@ Additions to existing modules
   product≢0    : All NonZero ns → NonZero (product ns)
   ∈⇒≤product   : All NonZero ns → n ∈ ns → n ≤ product ns
   concatMap-++ : concatMap f (xs ++ ys) ≡ concatMap f xs ++ concatMap f ys
+  filter-≐     : P ≐ Q → filter P? ≗ filter Q?
   ```
 
 * In `Data.List.Relation.Unary.Any.Properties`:
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 71d7b90b7f..4f591b656c 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -45,8 +45,8 @@ open import Relation.Binary.PropositionalEquality.Properties as ≡
 open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary using (¬_; Dec; does; _because_; yes; no; contradiction)
-open import Relation.Nullary.Decidable as Decidable using (isYes; map′; ⌊_⌋; ¬?; _×-dec_)
-open import Relation.Unary using (Pred; Decidable; ∁)
+open import Relation.Nullary.Decidable as Decidable using (isYes; map′; ⌊_⌋; ¬?; _×-dec_; dec-true; dec-false)
+open import Relation.Unary using (Pred; Decidable; ∁; _≐_)
 open import Relation.Unary.Properties using (∁?)
 import Data.Nat.GeneralisedArithmetic as ℕ
 
@@ -54,7 +54,7 @@ open ≡-Reasoning
 
 private
   variable
-    a b c d e p ℓ : Level
+    a b c d e p q ℓ : Level
     A : Set a
     B : Set b
     C : Set c
@@ -1236,6 +1236,14 @@ module _ {P : Pred A p} (P? : Decidable P) where
   ... | true  = cong (x ∷_) ih
   ... | false = ih
 
+module _ {P : Pred A p} {Q : Pred A q} (P? : Decidable P) (Q? : Decidable Q) where
+
+  filter-≐ : P ≐ Q → filter P? ≗ filter Q?
+  filter-≐ P≐Q [] = refl
+  filter-≐ P≐Q (x ∷ xs) with P? x
+  ... | yes P[x] rewrite dec-true (Q? x) (proj₁ P≐Q P[x]) = cong (x ∷_) (filter-≐ P≐Q xs)
+  ... | no ¬P[x] rewrite dec-false (Q? x) (¬P[x] ∘ proj₂ P≐Q) = filter-≐ P≐Q xs
+
 ------------------------------------------------------------------------
 -- derun and deduplicate
 

From 0f7260d8f868a3bb4f97f20441805822c3f6b894 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Mon, 18 Nov 2024 22:31:35 +0100
Subject: [PATCH 2/2] Avoid rewrite

---
 src/Data/List/Properties.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 4f591b656c..ab5aff8904 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -1241,8 +1241,8 @@ module _ {P : Pred A p} {Q : Pred A q} (P? : Decidable P) (Q? : Decidable Q) whe
   filter-≐ : P ≐ Q → filter P? ≗ filter Q?
   filter-≐ P≐Q [] = refl
   filter-≐ P≐Q (x ∷ xs) with P? x
-  ... | yes P[x] rewrite dec-true (Q? x) (proj₁ P≐Q P[x]) = cong (x ∷_) (filter-≐ P≐Q xs)
-  ... | no ¬P[x] rewrite dec-false (Q? x) (¬P[x] ∘ proj₂ P≐Q) = filter-≐ P≐Q xs
+  ... | yes P[x] = trans (cong (x ∷_) (filter-≐ P≐Q xs)) (sym (filter-accept Q? (proj₁ P≐Q P[x])))
+  ... | no ¬P[x] = trans (filter-≐ P≐Q xs) (sym (filter-reject Q? (¬P[x] ∘ proj₂ P≐Q)))
 
 ------------------------------------------------------------------------
 -- derun and deduplicate