blob: b27aeb49e49d1b15417b145a0a67dfbfcb3a4749 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
{-# OPTIONS --without-K --safe #-}
module Data.List.Properties.Ext where
open import Data.Bool using (Bool)
open import Data.Empty using (⊥-elim)
open import Data.List
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.Any using (Any)
open import Data.Product using (Σ)
open import Function using (Equivalence; _⇔_; _∘_)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; cong; cong₂)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Unary using (Pred; Decidable; _≐_)
private
variable
a p : Level
A B : Set a
open Any
open Bool
open Dec
open Equivalence
open _≡_
open Σ
-- Properties of filter -------------------------------------------------------
module _ {P : Pred A p} (P? : Decidable P) where
filter-cong :
∀ {Q : Pred A a} (Q? : Decidable Q) → P ≐ Q → filter P? ≗ filter Q?
filter-cong Q? P≐Q [] = refl
filter-cong Q? P≐Q (x ∷ xs) with P? x | Q? x
... | yes Px | yes Qx = cong (x ∷_) (filter-cong Q? P≐Q xs)
... | yes Px | no ¬Qx = ⊥-elim (¬Qx (P≐Q .proj₁ Px))
... | no ¬Px | yes Qx = ⊥-elim (¬Px (P≐Q .proj₂ Qx))
... | no ¬Px | no ¬Qx = filter-cong Q? P≐Q xs
filter-map :
∀ (f : B → A) xs →
filter P? (map f xs) ≡ map f (filter (P? ∘ f) xs)
filter-map f [] = refl
filter-map f (x ∷ xs) with does (P? (f x))
... | true = cong (f x ∷_) (filter-map f xs)
... | false = filter-map f xs
map-filter-cong :
∀ {f g : A → B} → (f≗g : ∀ {x} → P x → f x ≡ g x) →
map f ∘ filter P? ≗ map g ∘ filter P?
map-filter-cong f≗g [] = refl
map-filter-cong f≗g (x ∷ xs) with P? x
... | yes Px = cong₂ _∷_ (f≗g Px) (map-filter-cong f≗g xs)
... | no ¬Px = map-filter-cong f≗g xs
filter-map-comm :
∀ {Q : Pred B a} (Q? : Decidable Q) {f g : B → A} xs →
(∀ {x} → x ∈ xs → P (f x) ⇔ Q x) →
(∀ {x} → Q x → f x ≡ g x) →
filter P? (map f xs) ≡ map g (filter Q? xs)
filter-map-comm Q? [] P⇔Q f≗g = refl
filter-map-comm Q? {f} (x ∷ xs) P⇔Q f≗g with P? (f x) | Q? x
... | yes Pfx | yes Qx =
cong₂ _∷_ (f≗g Qx) (filter-map-comm Q? xs (P⇔Q ∘ there) f≗g)
... | yes Pfx | no ¬Qx = ⊥-elim (¬Qx (P⇔Q (here refl) .to Pfx))
... | no ¬Pfx | yes Qx = ⊥-elim (¬Pfx (P⇔Q (here refl) .from Qx))
... | no ¬Pfx | no ¬Qx = filter-map-comm Q? xs (P⇔Q ∘ there) f≗g
|
