[ add ] filter-∩, filter-map and filter-swap for Data.List.Properties (#2942)

* [ add ] `filter-∩` and `filter-swap` for `Data.List.Properties`

* [ add ] `filter-map` to `Data.List.Properties`

* also introduced minor readibility rewrites for `filter-∩`  and `filter-swap`

* [ add ] CHANGELOG entry for `filter-map`, `filter-∩` and `filter-swap`

* [ meta-fix ] adjusted changelog formatting

* [ refactor ] naming convention of arbitrary lists

Co-authored-by: jamesmckinna <[email protected]>

---------

Co-authored-by: jamesmckinna <[email protected]>

Author: IchiganCS

CHANGELOG.md

@@ -259,6 +259,13 @@ Additions to existing modules
   map : P ⊆ Q → All P xs → All Q xs
   ```
 
+* In `Data.List.Properties`:
+  ```
+  filter-map  : filter P? ∘ map f ≗ map f ∘ filter (P? ∘ f)
+  filter-∩    : filter (P? ∩? Q?) ≗ filter P? ∘ filter Q?
+  filter-swap : filter P? ∘ filter Q? ≗ filter Q? ∘ filter P?
+  ```
+
 * In `Data.Nat.Divisiblity`:
   ```agad
   m∣n⇒m^o∣n^o : ∀ o → m ∣ n → m ^ o ∣ n ^ o

src/Data/List/Properties.agda

@@ -28,7 +28,7 @@ open import Data.Maybe.Relation.Unary.Any using (just) renaming (Any to MAny)
 open import Data.Nat.Base
 open import Data.Nat.Properties
 open import Data.Product.Base as Product
-  using (_×_; _,_; uncurry; uncurry′; proj₁; proj₂; <_,_>)
+  using (_×_; _,_; uncurry; uncurry′; proj₁; proj₂; swap; <_,_>)
 import Data.Product.Relation.Unary.All as Product using (All)
 open import Data.Sum using (_⊎_; inj₁; inj₂; isInj₁; isInj₂)
 open import Data.These.Base as These using (These; this; that; these)
@@ -47,7 +47,7 @@ open import Relation.Nullary.Negation.Core using (contradiction; ¬_)
 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 (∁?)
+open import Relation.Unary.Properties using (∁?; _∩?_)
 import Data.Nat.GeneralisedArithmetic as ℕ
 
 open ≡-Reasoning
@@ -1258,6 +1258,12 @@ module _ {P : Pred A p} (P? : Decidable P) where
   ... | true  = cong (x ∷_) ih
   ... | false = ih
 
+  filter-map : (f : B → A) → filter P? ∘ map f ≗ map f ∘ filter (P? ∘ f)
+  filter-map f [] = refl
+  filter-map f (x ∷ xs) with ih ← filter-map f xs | does (P? (f x))
+  ... | true  = cong (f 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?
@@ -1266,6 +1272,25 @@ module _ {P : Pred A p} {Q : Pred A q} (P? : Decidable P) (Q? : Decidable Q) whe
   ... | 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)))
 
+  filter-∩ : filter (P? ∩? Q?) ≗ filter P? ∘ filter Q?
+  filter-∩ [] = refl
+  filter-∩ (x ∷ xs) with ih ← filter-∩ xs | P? x | Q? x
+  ... | yes P[x] | yes _  = trans (cong (x ∷_) ih) (sym (filter-accept P? P[x]))
+  ... | no ¬P[x] | yes _  = trans ih (sym (filter-reject P? ¬P[x]))
+  ... | yes _    | no  _  = ih
+  ... | no  _    | no  _  = ih
+
+
+module _ {P : Pred A p} {Q : Pred A q} (P? : Decidable P) (Q? : Decidable Q) where
+
+  filter-swap : filter P? ∘ filter Q? ≗ filter Q? ∘ filter P?
+  filter-swap xs =  begin
+    filter P? (filter Q? xs)   ≡⟨ filter-∩ P? Q? xs ⟨
+    filter (P? ∩? Q?) xs       ≡⟨ filter-≐ (P? ∩? Q?) (Q? ∩? P?) (swap , swap) xs ⟩
+    filter (Q? ∩? P?) xs       ≡⟨ filter-∩ Q? P? xs ⟩
+    filter Q? (filter P? xs)   ∎
+
+
 ------------------------------------------------------------------------
 -- derun and deduplicate