1
1
------------------------------------------------------------------------
2
-- The Agda standard library
2
4
-- Properties related to ◇
3
5
------------------------------------------------------------------------
5
{-# OPTIONS --universe-polymorphism #-}
7
7
module Data.Container.Any where
14
14
open import Data.Sum
15
15
open import Function
16
16
open import Function.Equality using (_⟨$⟩_)
17
open import Function.Inverse as Inv
18
using (_⇿_; Isomorphism; module Inverse)
19
open import Function.Inverse.TypeIsomorphisms
17
open import Function.Inverse as Inv using (_↔_; module Inverse)
18
open import Function.Related as Related using (Related)
19
open import Function.Related.TypeIsomorphisms
20
20
import Relation.Binary.HeterogeneousEquality as H
21
open import Relation.Binary.Product.Pointwise
21
22
open import Relation.Binary.PropositionalEquality as P
22
23
using (_≡_; _≗_; refl)
23
24
import Relation.Binary.Sigma.Pointwise as Σ
25
open Inv.EquationalReasoning
26
open Related.EquationalReasoning
27
28
module ×⊎ {k ℓ} = CommutativeSemiring (×⊎-CommutativeSemiring k ℓ)
29
30
-- ◇ can be expressed using _∈_.
31
⇿∈ : ∀ {c} (C : Container c) {X : Set c}
32
↔∈ : ∀ {c} (C : Container c) {X : Set c}
32
33
{P : X → Set c} {xs : ⟦ C ⟧ X} →
33
◇ P xs ⇿ (∃ λ x → x ∈ xs × P x)
34
⇿∈ _ {P = P} {xs} = record
34
◇ P xs ↔ (∃ λ x → x ∈ xs × P x)
35
↔∈ _ {P = P} {xs} = record
36
37
; from = P.→-to-⟶ from
37
38
; inverse-of = record
49
50
to∘from : to ∘ from ≗ id
50
51
to∘from (.(proj₂ xs p) , (p , refl) , Px) = refl
53
-- ◇ is a congruence for bag and set equality and related preorders.
53
55
cong : ∀ {k c} {C : Container c}
54
56
{X : Set c} {P₁ P₂ : X → Set c} {xs₁ xs₂ : ⟦ C ⟧ X} →
55
(∀ x → Isomorphism k (P₁ x) (P₂ x)) → xs₁ ≈[ k ] xs₂ →
56
Isomorphism k (◇ P₁ xs₁) (◇ P₂ xs₂)
57
cong {C = C} {P₁ = P₁} {P₂} {xs₁} {xs₂} P₁⇿P₂ xs₁≈xs₂ =
59
(∃ λ x → x ∈ xs₁ × P₁ x) ≈⟨ Σ.cong Inv.id (xs₁≈xs₂ ⟨ ×⊎.*-cong ⟩ P₁⇿P₂ _) ⟩
60
(∃ λ x → x ∈ xs₂ × P₂ x) ⇿⟨ sym (⇿∈ C) ⟩
57
(∀ x → Related k (P₁ x) (P₂ x)) → xs₁ ∼[ k ] xs₂ →
58
Related k (◇ P₁ xs₁) (◇ P₂ xs₂)
59
cong {C = C} {P₁ = P₁} {P₂} {xs₁} {xs₂} P₁↔P₂ xs₁≈xs₂ =
61
(∃ λ x → x ∈ xs₁ × P₁ x) ∼⟨ Σ.cong Inv.id (xs₁≈xs₂ ×-cong P₁↔P₂ _) ⟩
62
(∃ λ x → x ∈ xs₂ × P₂ x) ↔⟨ sym (↔∈ C) ⟩
63
65
-- Nested occurrences of ◇ can sometimes be swapped.
67
68
{xs : ⟦ C₁ ⟧ X} {ys : ⟦ C₂ ⟧ Y} →
68
69
let ◈ : ∀ {C : Container c} {X} → ⟦ C ⟧ X → (X → Set c) → Set c
70
◈ xs (◈ ys ∘ P) ⇿ ◈ ys (◈ xs ∘ flip P)
71
◈ xs (◈ ys ∘ P) ↔ ◈ ys (◈ xs ∘ flip P)
71
72
swap {c} {C₁} {C₂} {P = P} {xs} {ys} =
72
◇ (λ x → ◇ (P x) ys) xs ⇿⟨ ⇿∈ C₁ ⟩
73
(∃ λ x → x ∈ xs × ◇ (P x) ys) ⇿⟨ Σ.cong Inv.id (λ {x} → Inv.id ⟨ ×⊎.*-cong {ℓ = c} ⟩ ⇿∈ C₂ {P = P x}) ⟩
74
(∃ λ x → x ∈ xs × ∃ λ y → y ∈ ys × P x y) ⇿⟨ Σ.cong Inv.id (λ {x} → ∃∃⇿∃∃ {A = x ∈ xs} (λ _ y → y ∈ ys × P x y)) ⟩
75
(∃₂ λ x y → x ∈ xs × y ∈ ys × P x y) ⇿⟨ ∃∃⇿∃∃ (λ x y → x ∈ xs × y ∈ ys × P x y) ⟩
76
(∃₂ λ y x → x ∈ xs × y ∈ ys × P x y) ⇿⟨ Σ.cong Inv.id (λ {y} → Σ.cong Inv.id (λ {x} →
77
(x ∈ xs × y ∈ ys × P x y) ⇿⟨ sym $ ×⊎.*-assoc _ _ _ ⟩
78
((x ∈ xs × y ∈ ys) × P x y) ⇿⟨ ×⊎.*-comm _ _ ⟨ ×⊎.*-cong {ℓ = c} ⟩ Inv.id ⟩
79
((y ∈ ys × x ∈ xs) × P x y) ⇿⟨ ×⊎.*-assoc _ _ _ ⟩
73
◇ (λ x → ◇ (P x) ys) xs ↔⟨ ↔∈ C₁ ⟩
74
(∃ λ x → x ∈ xs × ◇ (P x) ys) ↔⟨ Σ.cong Inv.id (λ {x} → Inv.id ⟨ ×⊎.*-cong {ℓ = c} ⟩ ↔∈ C₂ {P = P x}) ⟩
75
(∃ λ x → x ∈ xs × ∃ λ y → y ∈ ys × P x y) ↔⟨ Σ.cong Inv.id (λ {x} → ∃∃↔∃∃ {A = x ∈ xs} (λ _ y → y ∈ ys × P x y)) ⟩
76
(∃₂ λ x y → x ∈ xs × y ∈ ys × P x y) ↔⟨ ∃∃↔∃∃ (λ x y → x ∈ xs × y ∈ ys × P x y) ⟩
77
(∃₂ λ y x → x ∈ xs × y ∈ ys × P x y) ↔⟨ Σ.cong Inv.id (λ {y} → Σ.cong Inv.id (λ {x} →
78
(x ∈ xs × y ∈ ys × P x y) ↔⟨ sym $ ×⊎.*-assoc _ _ _ ⟩
79
((x ∈ xs × y ∈ ys) × P x y) ↔⟨ ×⊎.*-comm _ _ ⟨ ×⊎.*-cong {ℓ = c} ⟩ Inv.id ⟩
80
((y ∈ ys × x ∈ xs) × P x y) ↔⟨ ×⊎.*-assoc _ _ _ ⟩
80
81
(y ∈ ys × x ∈ xs × P x y) ∎)) ⟩
81
(∃₂ λ y x → y ∈ ys × x ∈ xs × P x y) ⇿⟨ Σ.cong Inv.id (λ {y} → ∃∃⇿∃∃ {B = y ∈ ys} (λ x _ → x ∈ xs × P x y)) ⟩
82
(∃ λ y → y ∈ ys × ∃ λ x → x ∈ xs × P x y) ⇿⟨ Σ.cong Inv.id (λ {y} → Inv.id ⟨ ×⊎.*-cong {ℓ = c} ⟩ sym (⇿∈ C₁ {P = flip P y})) ⟩
83
(∃ λ y → y ∈ ys × ◇ (flip P y) xs) ⇿⟨ sym (⇿∈ C₂) ⟩
82
(∃₂ λ y x → y ∈ ys × x ∈ xs × P x y) ↔⟨ Σ.cong Inv.id (λ {y} → ∃∃↔∃∃ {B = y ∈ ys} (λ x _ → x ∈ xs × P x y)) ⟩
83
(∃ λ y → y ∈ ys × ∃ λ x → x ∈ xs × P x y) ↔⟨ Σ.cong Inv.id (λ {y} → Inv.id ⟨ ×⊎.*-cong {ℓ = c} ⟩ sym (↔∈ C₁ {P = flip P y})) ⟩
84
(∃ λ y → y ∈ ys × ◇ (flip P y) xs) ↔⟨ sym (↔∈ C₂) ⟩
84
85
◇ (λ y → ◇ (flip P y) xs) ys ∎
86
87
-- Nested occurrences of ◇ can sometimes be flattened.
88
89
flatten : ∀ {c} {C₁ C₂ : Container c} {X}
89
90
P (xss : ⟦ C₁ ⟧ (⟦ C₂ ⟧ X)) →
91
92
◇ P (Inverse.from (Composition.correct C₁ C₂) ⟨$⟩ xss)
92
93
flatten {C₁ = C₁} {C₂} {X} P xss = record
109
110
-- Sums commute with ◇ (for a fixed instance of a given container).
111
◇⊎⇿⊎◇ : ∀ {c} {C : Container c} {X : Set c} {xs : ⟦ C ⟧ X}
112
◇⊎↔⊎◇ : ∀ {c} {C : Container c} {X : Set c} {xs : ⟦ C ⟧ X}
112
113
{P Q : X → Set c} →
113
◇ (λ x → P x ⊎ Q x) xs ⇿ (◇ P xs ⊎ ◇ Q xs)
114
◇⊎⇿⊎◇ {xs = xs} {P} {Q} = record
114
◇ (λ x → P x ⊎ Q x) xs ↔ (◇ P xs ⊎ ◇ Q xs)
115
◇⊎↔⊎◇ {xs = xs} {P} {Q} = record
115
116
{ to = P.→-to-⟶ to
116
117
; from = P.→-to-⟶ from
117
118
; inverse-of = record
134
135
-- Products "commute" with ◇.
136
×◇⇿◇◇× : ∀ {c} {C₁ C₂ : Container c}
137
×◇↔◇◇× : ∀ {c} {C₁ C₂ : Container c}
137
138
{X Y} {P : X → Set c} {Q : Y → Set c}
138
139
{xs : ⟦ C₁ ⟧ X} {ys : ⟦ C₂ ⟧ Y} →
139
◇ (λ x → ◇ (λ y → P x × Q y) ys) xs ⇿ (◇ P xs × ◇ Q ys)
140
×◇⇿◇◇× {C₁ = C₁} {C₂} {P = P} {Q} {xs} {ys} = record
140
◇ (λ x → ◇ (λ y → P x × Q y) ys) xs ↔ (◇ P xs × ◇ Q ys)
141
×◇↔◇◇× {C₁ = C₁} {C₂} {P = P} {Q} {xs} {ys} = record
141
142
{ to = P.→-to-⟶ to
142
143
; from = P.→-to-⟶ from
143
144
; inverse-of = record
155
156
-- map can be absorbed by the predicate.
157
map⇿∘ : ∀ {c} (C : Container c) {X Y : Set c}
158
map↔∘ : ∀ {c} (C : Container c) {X Y : Set c}
158
159
(P : Y → Set c) {xs : ⟦ C ⟧ X} (f : X → Y) →
159
◇ P (C.map f xs) ⇿ ◇ (P ∘ f) xs
160
◇ P (C.map f xs) ↔ ◇ (P ∘ f) xs
162
163
-- Membership in a mapped container can be expressed without reference
165
∈map⇿∈×≡ : ∀ {c} (C : Container c) {X Y : Set c} {f : X → Y}
166
∈map↔∈×≡ : ∀ {c} (C : Container c) {X Y : Set c} {f : X → Y}
166
167
{xs : ⟦ C ⟧ X} {y} →
167
y ∈ C.map f xs ⇿ (∃ λ x → x ∈ xs × y ≡ f x)
168
∈map⇿∈×≡ {c} C {f = f} {xs} {y} =
169
y ∈ C.map f xs ⇿⟨ map⇿∘ C (_≡_ y) f ⟩
170
◇ (λ x → y ≡ f x) xs ⇿⟨ ⇿∈ C ⟩
168
y ∈ C.map f xs ↔ (∃ λ x → x ∈ xs × y ≡ f x)
169
∈map↔∈×≡ {c} C {f = f} {xs} {y} =
170
y ∈ C.map f xs ↔⟨ map↔∘ C (_≡_ y) f ⟩
171
◇ (λ x → y ≡ f x) xs ↔⟨ ↔∈ C ⟩
171
172
(∃ λ x → x ∈ xs × y ≡ f x) ∎
174
-- map is a congruence for bag and set equality and related preorders.
174
176
map-cong : ∀ {k c} {C : Container c} {X Y : Set c}
175
177
{f₁ f₂ : X → Y} {xs₁ xs₂ : ⟦ C ⟧ X} →
176
f₁ ≗ f₂ → xs₁ ≈[ k ] xs₂ →
177
C.map f₁ xs₁ ≈[ k ] C.map f₂ xs₂
178
f₁ ≗ f₂ → xs₁ ∼[ k ] xs₂ →
179
C.map f₁ xs₁ ∼[ k ] C.map f₂ xs₂
178
180
map-cong {c = c} {C} {f₁ = f₁} {f₂} {xs₁} {xs₂} f₁≗f₂ xs₁≈xs₂ {x} =
179
x ∈ C.map f₁ xs₁ ⇿⟨ map⇿∘ C (_≡_ x) f₁ ⟩
180
◇ (λ y → x ≡ f₁ y) xs₁ ≈⟨ cong {xs₁ = xs₁} {xs₂ = xs₂} (Inv.⇿⇒ ∘ helper) xs₁≈xs₂ ⟩
181
◇ (λ y → x ≡ f₂ y) xs₂ ⇿⟨ sym (map⇿∘ C (_≡_ x) f₂) ⟩
181
x ∈ C.map f₁ xs₁ ↔⟨ map↔∘ C (_≡_ x) f₁ ⟩
182
◇ (λ y → x ≡ f₁ y) xs₁ ∼⟨ cong {xs₁ = xs₁} {xs₂ = xs₂} (Related.↔⇒ ∘ helper) xs₁≈xs₂ ⟩
183
◇ (λ y → x ≡ f₂ y) xs₂ ↔⟨ sym (map↔∘ C (_≡_ x) f₂) ⟩
182
184
x ∈ C.map f₂ xs₂ ∎
184
helper : ∀ y → (x ≡ f₁ y) ⇿ (x ≡ f₂ y)
186
helper : ∀ y → (x ≡ f₁ y) ↔ (x ≡ f₂ y)
185
187
helper y = record
186
188
{ to = P.→-to-⟶ (λ x≡f₁y → P.trans x≡f₁y ( f₁≗f₂ y))
187
189
; from = P.→-to-⟶ (λ x≡f₂y → P.trans x≡f₂y (P.sym $ f₁≗f₂ y))
240
241
linear-identity :
241
242
∀ {c} {C : Container c} {X} {xs : ⟦ C ⟧ X} (m : C ⊸ C) →
242
⟪ m ⟫⊸ xs ≈[ bag ] xs
243
⟪ m ⟫⊸ xs ∼[ bag ] xs
243
244
linear-identity {xs = xs} m {x} =
244
x ∈ ⟪ m ⟫⊸ xs ⇿⟨ remove-linear (_≡_ x) m ⟩
245
x ∈ ⟪ m ⟫⊸ xs ↔⟨ remove-linear (_≡_ x) m ⟩
247
248
-- If join can be expressed using a linear morphism (in a certain
248
249
-- way), then it can be absorbed by the predicate.
250
join⇿◇ : ∀ {c} {C₁ C₂ C₃ : Container c} {X}
251
join↔◇ : ∀ {c} {C₁ C₂ C₃ : Container c} {X}
251
252
P (join′ : (C₁ ⟨∘⟩ C₂) ⊸ C₃) (xss : ⟦ C₁ ⟧ (⟦ C₂ ⟧ X)) →
252
253
let join : ∀ {X} → ⟦ C₁ ⟧ (⟦ C₂ ⟧ X) → ⟦ C₃ ⟧ X
253
254
join = ⟪ join′ ⟫⊸ ∘
254
255
_⟨$⟩_ (Inverse.from (Composition.correct C₁ C₂)) in
255
◇ P (join xss) ⇿ ◇ (◇ P) xss
256
join⇿◇ {C₁ = C₁} {C₂} P join xss =
257
◇ P (⟪ join ⟫⊸ xss′) ⇿⟨ remove-linear P join ⟩
258
◇ P xss′ ⇿⟨ sym $ flatten P xss ⟩
256
◇ P (join xss) ↔ ◇ (◇ P) xss
257
join↔◇ {C₁ = C₁} {C₂} P join xss =
258
◇ P (⟪ join ⟫⊸ xss′) ↔⟨ remove-linear P join ⟩
259
◇ P xss′ ↔⟨ sym $ flatten P xss ⟩
260
261
where xss′ = Inverse.from (Composition.correct C₁ C₂) ⟨$⟩ xss
added
removed
src/Data/Container/Any.agda
