Add filter-↭ (#2589)

Author: Taneb

CHANGELOG.md

@@ -130,10 +130,16 @@ Additions to existing modules
   quasiring                       : Quasiring c ℓ → Quasiring (a ⊔ c) (a ⊔ ℓ)
   commutativeRing                 : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
   ```
+
 * In `Data.List.Properties`:
   ```agda
   map-applyUpTo : ∀ (f : ℕ → A) (g : A → B) n → map g (applyUpTo f n) ≡ applyUpTo (g ∘ f) n
   map-applyDownFrom : ∀ (f : ℕ → A) (g : A → B) n → map g (applyDownFrom f n) ≡ applyDownFrom (g ∘ f) n
   map-upTo : ∀ (f : ℕ → A) n → map f (upTo n) ≡ applyUpTo f n
   map-downFrom : ∀ (f : ℕ → A) n → map f (downFrom n) ≡ applyDownFrom f n
   ```
+
+* In `Data.List.Relation.Binary.Permutation.PropositionalProperties`:
+  ```agda
+  filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
+  ```

src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda

@@ -26,7 +26,7 @@ open import Data.Product.Base using (_,_; _×_; ∃; ∃₂)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Function.Base using (_∘_; _⟨_⟩_; _$_)
 open import Level using (Level)
-open import Relation.Unary using (Pred)
+open import Relation.Unary as Pred using (Pred)
 open import Relation.Binary.Core using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
 open import Relation.Binary.Definitions using (_Respects_; Decidable)
 open import Relation.Binary.PropositionalEquality.Core as ≡
@@ -372,6 +372,21 @@ module _ {ℓ} {R : Rel A ℓ} (R? : Decidable R) where
     x ∷ xs ++ y ∷ ys         ∎
     where open PermutationReasoning
 
+------------------------------------------------------------------------
+-- filter
+
+filter-↭ : ∀ {p} {P : Pred A p} (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
+filter-↭ P? refl = refl
+filter-↭ P? (prep x xs↭ys) with P? x
+... | yes _ = prep x (filter-↭ P? xs↭ys)
+... | no _  = filter-↭ P? xs↭ys
+filter-↭ P? (swap x y xs↭ys) with P? x in eqˣ | P? y in eqʸ
+... | yes _ | yes _ rewrite eqˣ rewrite eqʸ = swap x y (filter-↭ P? xs↭ys)
+... | yes _ | no  _ rewrite eqˣ rewrite eqʸ = prep x (filter-↭ P? xs↭ys)
+... | no _  | yes _ rewrite eqˣ rewrite eqʸ = prep y (filter-↭ P? xs↭ys)
+... | no _  | no _  rewrite eqˣ rewrite eqʸ = filter-↭ P? xs↭ys
+filter-↭ P? (trans xs↭ys ys↭zs) = ↭-trans (filter-↭ P? xs↭ys) (filter-↭ P? ys↭zs)
+
 ------------------------------------------------------------------------
 -- catMaybes