From a081edb8818f2b584d2d9feea02510397de3362d Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 9 May 2024 23:06:49 -0700 Subject: [PATCH] Add a proof about filter's distributivity Signed-off-by: Danila Fedorin --- Utils.agda | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/Utils.agda b/Utils.agda index 0e76eb7..ea6b88c 100644 --- a/Utils.agda +++ b/Utils.agda @@ -3,15 +3,16 @@ module Utils where open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_) open import Data.Product as Prod using (_×_) open import Data.Nat using (ℕ; suc) -open import Data.List using (List; cartesianProduct; []; _∷_; _++_; foldr) renaming (map to mapˡ) +open import Data.List using (List; cartesianProduct; []; _∷_; _++_; foldr; filter) renaming (map to mapˡ) open import Data.List.Membership.Propositional using (_∈_) open import Data.List.Membership.Propositional.Properties as ListMemProp using () open import Data.List.Relation.Unary.All using (All; []; _∷_; map) open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map open import Data.Sum using (_⊎_) open import Function.Definitions using (Injective) -open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl) -open import Relation.Nullary using (¬_) +open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl; cong) +open import Relation.Nullary using (¬_; yes; no) +open import Relation.Unary using (Decidable) data Unique {c} {C : Set c} : List C → Set c where empty : Unique [] @@ -83,6 +84,14 @@ concat-∈ : ∀ {a} {A : Set a} {x : A} {l : List A} {ls : List (List A)} → concat-∈ x∈l (here refl) = ListMemProp.∈-++⁺ˡ x∈l concat-∈ {ls = l' ∷ ls'} x∈l (there l∈ls') = ListMemProp.∈-++⁺ʳ l' (concat-∈ x∈l l∈ls') +filter-++ : ∀ {a p} {A : Set a} (l₁ l₂ : List A) {P : A → Set p} (P? : Decidable P) → + filter P? (l₁ ++ l₂) ≡ filter P? l₁ ++ filter P? l₂ +filter-++ [] l₂ P? = refl +filter-++ (x ∷ xs) l₂ P? + with P? x +... | yes _ = cong (x ∷_) (filter-++ xs l₂ P?) +... | no _ = (filter-++ xs l₂ P?) + _⇒_ : ∀ {a p₁ p₂} {A : Set a} (P : A → Set p₁) (Q : A → Set p₂) → Set (a ⊔ℓ p₁ ⊔ℓ p₂) _⇒_ P Q = ∀ a → P a → Q a