DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add a proof about filter's distributivity

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-05-09 23:06:49 -07:00
parent 3d2a507f2f
commit a081edb881
1 changed files with 12 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
Utils.agda
View File

@ -3,15 +3,16 @@ module Utils where
open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_) open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_)
open import Data.Product as Prod using (_×_) open import Data.Product as Prod using (_×_)
open import Data.Nat using (ℕ; suc) 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 using (_∈_)
open import Data.List.Membership.Propositional.Properties as ListMemProp 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.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.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map
open import Data.Sum using (_⊎_) open import Data.Sum using (_⊎_)
open import Function.Definitions using (Injective) open import Function.Definitions using (Injective)
open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl) open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl; cong)
open import Relation.Nullary using (¬_) open import Relation.Nullary using (¬_; yes; no)
open import Relation.Unary using (Decidable)
data Unique {c} {C : Set c} : List C → Set c where data Unique {c} {C : Set c} : List C → Set c where
empty : Unique [] 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-∈ x∈l (here refl) = ListMemProp.∈-++⁺ˡ x∈l
concat-∈ {ls = l' ∷ ls'} x∈l (there l∈ls') = ListMemProp.∈-++⁺ʳ l' (concat-∈ x∈l l∈ls') 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₂) → _⇒_ : ∀ {a p₁ p₂} {A : Set a} (P : A → Set p₁) (Q : A → Set p₂) →
Set (a ⊔ℓ p₁ ⊔ℓ p₂) Set (a ⊔ℓ p₁ ⊔ℓ p₂)
_⇒_ P Q = ∀ a → P a → Q a _⇒_ P Q = ∀ a → P a → Q a