46
46
------------------------------------------------------------------------
47
47
-- Properties relating _∈_ to various list functions
49
map-∈⇿ : ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y xs} →
50
(∃ λ x → x ∈ xs × y ≡ f x) ⇿ y ∈ List.map f xs
51
map-∈⇿ {a} {b} {f = f} {y} {xs} =
52
(∃ λ x → x ∈ xs × y ≡ f x) ⇿⟨ Any⇿ {a = a} {p = b} ⟩
53
Any (λ x → y ≡ f x) xs ⇿⟨ map⇿ {a = a} {b = b} {p = b} ⟩
49
map-∈↔ : ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y xs} →
50
(∃ λ x → x ∈ xs × y ≡ f x) ↔ y ∈ List.map f xs
51
map-∈↔ {a} {b} {f = f} {y} {xs} =
52
(∃ λ x → x ∈ xs × y ≡ f x) ↔⟨ Any↔ {a = a} {p = b} ⟩
53
Any (λ x → y ≡ f x) xs ↔⟨ map↔ {a = a} {b = b} {p = b} ⟩
54
54
y ∈ List.map f xs ∎
55
where open Inv.EquationalReasoning
55
where open Related.EquationalReasoning
57
concat-∈⇿ : ∀ {a} {A : Set a} {x : A} {xss} →
58
(∃ λ xs → x ∈ xs × xs ∈ xss) ⇿ x ∈ concat xss
59
concat-∈⇿ {a} {x = x} {xss} =
60
(∃ λ xs → x ∈ xs × xs ∈ xss) ⇿⟨ Σ.cong {a₁ = a} {b₁ = a} {b₂ = a} Inv.id $ ×⊎.*-comm _ _ ⟩
61
(∃ λ xs → xs ∈ xss × x ∈ xs) ⇿⟨ Any⇿ {a = a} {p = a} ⟩
62
Any (Any (_≡_ x)) xss ⇿⟨ concat⇿ {a = a} {p = a} ⟩
57
concat-∈↔ : ∀ {a} {A : Set a} {x : A} {xss} →
58
(∃ λ xs → x ∈ xs × xs ∈ xss) ↔ x ∈ concat xss
59
concat-∈↔ {a} {x = x} {xss} =
60
(∃ λ xs → x ∈ xs × xs ∈ xss) ↔⟨ Σ.cong {a₁ = a} {b₁ = a} {b₂ = a} Inv.id $ ×⊎.*-comm _ _ ⟩
61
(∃ λ xs → xs ∈ xss × x ∈ xs) ↔⟨ Any↔ {a = a} {p = a} ⟩
62
Any (Any (_≡_ x)) xss ↔⟨ concat↔ {a = a} {p = a} ⟩
64
where open Inv.EquationalReasoning
64
where open Related.EquationalReasoning
66
>>=-∈⇿ : ∀ {ℓ} {A B : Set ℓ} {xs} {f : A → List B} {y} →
67
(∃ λ x → x ∈ xs × y ∈ f x) ⇿ y ∈ (xs >>= f)
68
>>=-∈⇿ {ℓ} {xs = xs} {f} {y} =
69
(∃ λ x → x ∈ xs × y ∈ f x) ⇿⟨ Any⇿ {a = ℓ} {p = ℓ} ⟩
70
Any (Any (_≡_ y) ∘ f) xs ⇿⟨ >>=⇿ {ℓ = ℓ} {p = ℓ} ⟩
66
>>=-∈↔ : ∀ {ℓ} {A B : Set ℓ} {xs} {f : A → List B} {y} →
67
(∃ λ x → x ∈ xs × y ∈ f x) ↔ y ∈ (xs >>= f)
68
>>=-∈↔ {ℓ} {xs = xs} {f} {y} =
69
(∃ λ x → x ∈ xs × y ∈ f x) ↔⟨ Any↔ {a = ℓ} {p = ℓ} ⟩
70
Any (Any (_≡_ y) ∘ f) xs ↔⟨ >>=↔ {ℓ = ℓ} {p = ℓ} ⟩
72
where open Inv.EquationalReasoning
72
where open Related.EquationalReasoning
74
⊛-∈⇿ : ∀ {ℓ} {A B : Set ℓ} (fs : List (A → B)) {xs y} →
75
(∃₂ λ f x → f ∈ fs × x ∈ xs × y ≡ f x) ⇿ y ∈ fs ⊛ xs
76
⊛-∈⇿ {ℓ} fs {xs} {y} =
77
(∃₂ λ f x → f ∈ fs × x ∈ xs × y ≡ f x) ⇿⟨ Σ.cong {a₁ = ℓ} {b₁ = ℓ} {b₂ = ℓ} Inv.id (∃∃⇿∃∃ {a = ℓ} {b = ℓ} {p = ℓ} _) ⟩
78
(∃ λ f → f ∈ fs × ∃ λ x → x ∈ xs × y ≡ f x) ⇿⟨ Σ.cong {a₁ = ℓ} {b₁ = ℓ} {b₂ = ℓ}
79
Inv.id ((_ ∎) ⟨ ×⊎.*-cong {ℓ = ℓ} ⟩ Any⇿ {a = ℓ} {p = ℓ}) ⟩
80
(∃ λ f → f ∈ fs × Any (_≡_ y ∘ f) xs) ⇿⟨ Any⇿ {a = ℓ} {p = ℓ} ⟩
81
Any (λ f → Any (_≡_ y ∘ f) xs) fs ⇿⟨ ⊛⇿ ⟩
74
⊛-∈↔ : ∀ {ℓ} {A B : Set ℓ} (fs : List (A → B)) {xs y} →
75
(∃₂ λ f x → f ∈ fs × x ∈ xs × y ≡ f x) ↔ y ∈ fs ⊛ xs
76
⊛-∈↔ {ℓ} fs {xs} {y} =
77
(∃₂ λ f x → f ∈ fs × x ∈ xs × y ≡ f x) ↔⟨ Σ.cong {a₁ = ℓ} {b₁ = ℓ} {b₂ = ℓ} Inv.id (∃∃↔∃∃ {a = ℓ} {b = ℓ} {p = ℓ} _) ⟩
78
(∃ λ f → f ∈ fs × ∃ λ x → x ∈ xs × y ≡ f x) ↔⟨ Σ.cong {a₁ = ℓ} {b₁ = ℓ} {b₂ = ℓ}
79
Inv.id ((_ ∎) ⟨ ×⊎.*-cong {ℓ = ℓ} ⟩ Any↔ {a = ℓ} {p = ℓ}) ⟩
80
(∃ λ f → f ∈ fs × Any (_≡_ y ∘ f) xs) ↔⟨ Any↔ {a = ℓ} {p = ℓ} ⟩
81
Any (λ f → Any (_≡_ y ∘ f) xs) fs ↔⟨ ⊛↔ ⟩
83
where open Inv.EquationalReasoning
83
where open Related.EquationalReasoning
85
⊗-∈⇿ : ∀ {A B : Set} {xs ys} {x : A} {y : B} →
86
(x ∈ xs × y ∈ ys) ⇿ (x , y) ∈ (xs ⊗ ys)
87
⊗-∈⇿ {A} {B} {xs} {ys} {x} {y} =
88
(x ∈ xs × y ∈ ys) ⇿⟨ ⊗⇿′ ⟩
89
Any (_≡_ x ⟨×⟩ _≡_ y) (xs ⊗ ys) ⇿⟨ Any-cong helper (_ ∎) ⟩
85
⊗-∈↔ : ∀ {A B : Set} {xs ys} {x : A} {y : B} →
86
(x ∈ xs × y ∈ ys) ↔ (x , y) ∈ (xs ⊗ ys)
87
⊗-∈↔ {A} {B} {xs} {ys} {x} {y} =
88
(x ∈ xs × y ∈ ys) ↔⟨ ⊗↔′ ⟩
89
Any (_≡_ x ⟨×⟩ _≡_ y) (xs ⊗ ys) ↔⟨ Any-cong helper (_ ∎) ⟩
90
90
(x , y) ∈ (xs ⊗ ys) ∎
92
open Inv.EquationalReasoning
92
open Related.EquationalReasoning
94
helper : (p : A × B) → (x ≡ proj₁ p × y ≡ proj₂ p) ⇿ (x , y) ≡ p
94
helper : (p : A × B) → (x ≡ proj₁ p × y ≡ proj₂ p) ↔ (x , y) ≡ p
95
95
helper (x′ , y′) = record
96
96
{ to = P.→-to-⟶ (uncurry $ P.cong₂ _,_)
97
97
; from = P.→-to-⟶ < P.cong proj₁ , P.cong proj₂ >
108
108
mono : ∀ {a p} {A : Set a} {P : A → Set p} {xs ys} →
109
109
xs ⊆ ys → Any P xs → Any P ys
111
_⟨$⟩_ (Inverse.to Any⇿) ∘′
111
_⟨$⟩_ (Inverse.to Any↔) ∘′
112
112
Prod.map id (Prod.map xs⊆ys id) ∘
113
_⟨$⟩_ (Inverse.from Any⇿)
113
_⟨$⟩_ (Inverse.from Any↔)
115
115
map-mono : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {xs ys} →
116
116
xs ⊆ ys → List.map f xs ⊆ List.map f ys
117
117
map-mono f xs⊆ys =
118
_⟨$⟩_ (Inverse.to map-∈⇿) ∘
118
_⟨$⟩_ (Inverse.to map-∈↔) ∘
119
119
Prod.map id (Prod.map xs⊆ys id) ∘
120
_⟨$⟩_ (Inverse.from map-∈⇿)
120
_⟨$⟩_ (Inverse.from map-∈↔)
122
122
_++-mono_ : ∀ {a} {A : Set a} {xs₁ xs₂ ys₁ ys₂ : List A} →
123
123
xs₁ ⊆ ys₁ → xs₂ ⊆ ys₂ → xs₁ ++ xs₂ ⊆ ys₁ ++ ys₂
124
124
_++-mono_ xs₁⊆ys₁ xs₂⊆ys₂ =
125
_⟨$⟩_ (Inverse.to ++⇿) ∘
125
_⟨$⟩_ (Inverse.to ++↔) ∘
126
126
Sum.map xs₁⊆ys₁ xs₂⊆ys₂ ∘
127
_⟨$⟩_ (Inverse.from ++⇿)
127
_⟨$⟩_ (Inverse.from ++↔)
129
129
concat-mono : ∀ {a} {A : Set a} {xss yss : List (List A)} →
130
130
xss ⊆ yss → concat xss ⊆ concat yss
131
131
concat-mono {a} xss⊆yss =
132
_⟨$⟩_ (Inverse.to $ concat-∈⇿ {a = a}) ∘
132
_⟨$⟩_ (Inverse.to $ concat-∈↔ {a = a}) ∘
133
133
Prod.map id (Prod.map id xss⊆yss) ∘
134
_⟨$⟩_ (Inverse.from $ concat-∈⇿ {a = a})
134
_⟨$⟩_ (Inverse.from $ concat-∈↔ {a = a})
136
136
>>=-mono : ∀ {ℓ} {A B : Set ℓ} (f g : A → List B) {xs ys} →
137
137
xs ⊆ ys → (∀ {x} → f x ⊆ g x) →
138
138
(xs >>= f) ⊆ (ys >>= g)
139
139
>>=-mono {ℓ} f g xs⊆ys f⊆g =
140
_⟨$⟩_ (Inverse.to $ >>=-∈⇿ {ℓ = ℓ}) ∘
140
_⟨$⟩_ (Inverse.to $ >>=-∈↔ {ℓ = ℓ}) ∘
141
141
Prod.map id (Prod.map xs⊆ys f⊆g) ∘
142
_⟨$⟩_ (Inverse.from $ >>=-∈⇿ {ℓ = ℓ})
142
_⟨$⟩_ (Inverse.from $ >>=-∈↔ {ℓ = ℓ})
144
144
_⊛-mono_ : ∀ {ℓ} {A B : Set ℓ}
145
145
{fs gs : List (A → B)} {xs ys : List A} →
146
146
fs ⊆ gs → xs ⊆ ys → (fs ⊛ xs) ⊆ (gs ⊛ ys)
147
147
_⊛-mono_ {fs = fs} {gs} fs⊆gs xs⊆ys =
148
_⟨$⟩_ (Inverse.to $ ⊛-∈⇿ gs) ∘
148
_⟨$⟩_ (Inverse.to $ ⊛-∈↔ gs) ∘
149
149
Prod.map id (Prod.map id (Prod.map fs⊆gs (Prod.map xs⊆ys id))) ∘
150
_⟨$⟩_ (Inverse.from $ ⊛-∈⇿ fs)
150
_⟨$⟩_ (Inverse.from $ ⊛-∈↔ fs)
152
152
_⊗-mono_ : {A B : Set} {xs₁ ys₁ : List A} {xs₂ ys₂ : List B} →
153
153
xs₁ ⊆ ys₁ → xs₂ ⊆ ys₂ → (xs₁ ⊗ xs₂) ⊆ (ys₁ ⊗ ys₂)
154
154
xs₁⊆ys₁ ⊗-mono xs₂⊆ys₂ =
155
_⟨$⟩_ (Inverse.to ⊗-∈⇿) ∘
155
_⟨$⟩_ (Inverse.to ⊗-∈↔) ∘
156
156
Prod.map xs₁⊆ys₁ xs₂⊆ys₂ ∘
157
_⟨$⟩_ (Inverse.from ⊗-∈⇿)
157
_⟨$⟩_ (Inverse.from ⊗-∈↔)
159
159
any-mono : ∀ {a} {A : Set a} (p : A → Bool) →
160
160
∀ {xs ys} → xs ⊆ ys → T (any p xs) → T (any p ys)
161
161
any-mono {a} p xs⊆ys =
162
_⟨$⟩_ (Equivalent.to $ any⇔ {a = a}) ∘
162
_⟨$⟩_ (Equivalence.to $ any⇔ {a = a}) ∘
164
_⟨$⟩_ (Equivalent.from $ any⇔ {a = a})
164
_⟨$⟩_ (Equivalence.from $ any⇔ {a = a})
166
166
map-with-∈-mono :
167
167
∀ {a b} {A : Set a} {B : Set b}
added
removed
src/Data/List/Any/Membership.agda
