21
21
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
22
22
open import Function
23
23
open import Function.Equality using (_⟨$⟩_)
24
open import Function.Equivalence
25
using (_⇔_; equivalent; module Equivalent)
26
open import Function.Inverse as Inv
27
using (Isomorphism; _⇿_; module Inverse)
28
open import Function.Inverse.TypeIsomorphisms
24
open import Function.Equivalence as Eq using (_⇔_; module Equivalence)
25
open import Function.Inverse as Inv using (_↔_; module Inverse)
26
open import Function.Related as Related using (Related)
27
open import Function.Related.TypeIsomorphisms
30
29
open import Relation.Binary
31
30
import Relation.Binary.HeterogeneousEquality as H
31
open import Relation.Binary.Product.Pointwise
32
32
open import Relation.Binary.PropositionalEquality as P
33
using (_≡_; refl; inspect; _with-≡_)
33
using (_≡_; refl; inspect) renaming ([_] to P[_])
34
34
open import Relation.Unary using (_⟨×⟩_; _⟨→⟩_) renaming (_⊆_ to _⋐_)
35
35
import Relation.Binary.Sigma.Pointwise as Σ
36
open import Relation.Binary.Sum
37
38
open Any.Membership-≡
38
open Inv.EquationalReasoning
39
open Related.EquationalReasoning
40
41
module ×⊎ {k ℓ} = CommutativeSemiring (×⊎-CommutativeSemiring k ℓ)
41
42
open module ListMonad {ℓ} = RawMonad (List.monad {ℓ = ℓ})
103
104
-- Any can be expressed using _∈_.
105
Any⇿ : ∀ {a p} {A : Set a} {P : A → Set p} {xs} →
106
(∃ λ x → x ∈ xs × P x) ⇿ Any P xs
107
Any⇿ {P = P} {xs} = record
106
Any↔ : ∀ {a p} {A : Set a} {P : A → Set p} {xs} →
107
(∃ λ x → x ∈ xs × P x) ↔ Any P xs
108
Any↔ {P = P} {xs} = record
108
109
{ to = P.→-to-⟶ to
109
110
; from = P.→-to-⟶ (find {P = P})
110
111
; inverse-of = record
121
122
-- Any is a congruence
123
124
Any-cong : ∀ {k ℓ} {A : Set ℓ} {P₁ P₂ : A → Set ℓ} {xs₁ xs₂ : List A} →
124
(∀ x → Isomorphism k (P₁ x) (P₂ x)) → xs₁ ≈[ k ] xs₂ →
125
Isomorphism k (Any P₁ xs₁) (Any P₂ xs₂)
126
Any-cong {P₁ = P₁} {P₂} {xs₁} {xs₂} P₁⇿P₂ xs₁≈xs₂ =
127
Any P₁ xs₁ ⇿⟨ sym $ Any⇿ {P = P₁} ⟩
128
(∃ λ x → x ∈ xs₁ × P₁ x) ≈⟨ Σ.cong Inv.id (xs₁≈xs₂ ⟨ ×⊎.*-cong ⟩ P₁⇿P₂ _) ⟩
129
(∃ λ x → x ∈ xs₂ × P₂ x) ⇿⟨ Any⇿ {P = P₂} ⟩
125
(∀ x → Related k (P₁ x) (P₂ x)) → xs₁ ∼[ k ] xs₂ →
126
Related k (Any P₁ xs₁) (Any P₂ xs₂)
127
Any-cong {P₁ = P₁} {P₂} {xs₁} {xs₂} P₁↔P₂ xs₁≈xs₂ =
128
Any P₁ xs₁ ↔⟨ sym $ Any↔ {P = P₁} ⟩
129
(∃ λ x → x ∈ xs₁ × P₁ x) ∼⟨ Σ.cong Inv.id (xs₁≈xs₂ ×-cong P₁↔P₂ _) ⟩
130
(∃ λ x → x ∈ xs₂ × P₂ x) ↔⟨ Any↔ {P = P₂} ⟩
132
133
------------------------------------------------------------------------
136
-- Nested occurrences of Any can sometimes be swapped. See also ×↔.
136
138
swap : ∀ {ℓ} {A B : Set ℓ} {P : A → B → Set ℓ} {xs ys} →
137
Any (λ x → Any (P x) ys) xs ⇿ Any (λ y → Any (flip P y) xs) ys
139
Any (λ x → Any (P x) ys) xs ↔ Any (λ y → Any (flip P y) xs) ys
138
140
swap {ℓ} {P = P} {xs} {ys} =
139
Any (λ x → Any (P x) ys) xs ⇿⟨ sym $ Any⇿ {a = ℓ} {p = ℓ} ⟩
140
(∃ λ x → x ∈ xs × Any (P x) ys) ⇿⟨ sym $ Σ.cong Inv.id (λ {x} → (x ∈ xs ∎) ⟨ ×⊎.*-cong {ℓ = ℓ} ⟩ Any⇿ {a = ℓ} {p = ℓ}) ⟩
141
(∃ λ x → x ∈ xs × ∃ λ y → y ∈ ys × P x y) ⇿⟨ Σ.cong {a₁ = ℓ} Inv.id (∃∃⇿∃∃ {a = ℓ} {b = ℓ} {p = ℓ} _) ⟩
142
(∃₂ λ x y → x ∈ xs × y ∈ ys × P x y) ⇿⟨ ∃∃⇿∃∃ {a = ℓ} {b = ℓ} {p = ℓ} _ ⟩
143
(∃₂ λ y x → x ∈ xs × y ∈ ys × P x y) ⇿⟨ Σ.cong Inv.id (λ {y} → Σ.cong Inv.id (λ {x} →
144
(x ∈ xs × y ∈ ys × P x y) ⇿⟨ sym $ ×⊎.*-assoc _ _ _ ⟩
145
((x ∈ xs × y ∈ ys) × P x y) ⇿⟨ ×⊎.*-comm (x ∈ xs) (y ∈ ys) ⟨ ×⊎.*-cong ⟩ (P x y ∎) ⟩
146
((y ∈ ys × x ∈ xs) × P x y) ⇿⟨ ×⊎.*-assoc _ _ _ ⟩
141
Any (λ x → Any (P x) ys) xs ↔⟨ sym $ Any↔ {a = ℓ} {p = ℓ} ⟩
142
(∃ λ x → x ∈ xs × Any (P x) ys) ↔⟨ sym $ Σ.cong Inv.id (λ {x} → (x ∈ xs ∎) ⟨ ×⊎.*-cong {ℓ = ℓ} ⟩ Any↔ {a = ℓ} {p = ℓ}) ⟩
143
(∃ λ x → x ∈ xs × ∃ λ y → y ∈ ys × P x y) ↔⟨ Σ.cong {a₁ = ℓ} Inv.id (∃∃↔∃∃ {a = ℓ} {b = ℓ} {p = ℓ} _) ⟩
144
(∃₂ λ x y → x ∈ xs × y ∈ ys × P x y) ↔⟨ ∃∃↔∃∃ {a = ℓ} {b = ℓ} {p = ℓ} _ ⟩
145
(∃₂ λ y x → x ∈ xs × y ∈ ys × P x y) ↔⟨ Σ.cong Inv.id (λ {y} → Σ.cong Inv.id (λ {x} →
146
(x ∈ xs × y ∈ ys × P x y) ↔⟨ sym $ ×⊎.*-assoc _ _ _ ⟩
147
((x ∈ xs × y ∈ ys) × P x y) ↔⟨ ×⊎.*-comm (x ∈ xs) (y ∈ ys) ⟨ ×⊎.*-cong ⟩ (P x y ∎) ⟩
148
((y ∈ ys × x ∈ xs) × P x y) ↔⟨ ×⊎.*-assoc _ _ _ ⟩
147
149
(y ∈ ys × x ∈ xs × P x y) ∎)) ⟩
148
(∃₂ λ y x → y ∈ ys × x ∈ xs × P x y) ⇿⟨ Σ.cong {a₁ = ℓ} Inv.id (∃∃⇿∃∃ {a = ℓ} {b = ℓ} {p = ℓ} _) ⟩
149
(∃ λ y → y ∈ ys × ∃ λ x → x ∈ xs × P x y) ⇿⟨ Σ.cong Inv.id (λ {y} → (y ∈ ys ∎) ⟨ ×⊎.*-cong {ℓ = ℓ} ⟩ Any⇿ {a = ℓ} {p = ℓ}) ⟩
150
(∃ λ y → y ∈ ys × Any (flip P y) xs) ⇿⟨ Any⇿ {a = ℓ} {p = ℓ} ⟩
150
(∃₂ λ y x → y ∈ ys × x ∈ xs × P x y) ↔⟨ Σ.cong {a₁ = ℓ} Inv.id (∃∃↔∃∃ {a = ℓ} {b = ℓ} {p = ℓ} _) ⟩
151
(∃ λ y → y ∈ ys × ∃ λ x → x ∈ xs × P x y) ↔⟨ Σ.cong Inv.id (λ {y} → (y ∈ ys ∎) ⟨ ×⊎.*-cong {ℓ = ℓ} ⟩ Any↔ {a = ℓ} {p = ℓ}) ⟩
152
(∃ λ y → y ∈ ys × Any (flip P y) xs) ↔⟨ Any↔ {a = ℓ} {p = ℓ} ⟩
151
153
Any (λ y → Any (flip P y) xs) ys ∎
153
155
------------------------------------------------------------------------
154
156
-- Lemmas relating Any to ⊥
156
⊥⇿Any⊥ : ∀ {a} {A : Set a} {xs : List A} → ⊥ ⇿ Any (const ⊥) xs
157
⊥⇿Any⊥ {A = A} = record
158
⊥↔Any⊥ : ∀ {a} {A : Set a} {xs : List A} → ⊥ ↔ Any (const ⊥) xs
159
⊥↔Any⊥ {A = A} = record
158
160
{ to = P.→-to-⟶ (λ ())
159
161
; from = P.→-to-⟶ (λ p → from p)
160
162
; inverse-of = record
219
220
-- Products "commute" with Any.
221
×⇿ : {A B : Set} {P : A → Set} {Q : B → Set}
222
×↔ : {A B : Set} {P : A → Set} {Q : B → Set}
222
223
{xs : List A} {ys : List B} →
223
(Any P xs × Any Q ys) ⇿ Any (λ x → Any (λ y → P x × Q y) ys) xs
224
×⇿ {P = P} {Q} {xs} {ys} = record
224
(Any P xs × Any Q ys) ↔ Any (λ x → Any (λ y → P x × Q y) ys) xs
225
×↔ {P = P} {Q} {xs} {ys} = record
225
226
{ to = P.→-to-⟶ to
226
227
; from = P.→-to-⟶ from
227
228
; inverse-of = record
304
305
map⁻∘map⁺ P (here p) = refl
305
306
map⁻∘map⁺ P (there p) = P.cong there (map⁻∘map⁺ P p)
307
map⇿ : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p}
308
map↔ : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p}
308
309
{f : A → B} {xs} →
309
Any (P ∘ f) xs ⇿ Any P (List.map f xs)
310
map⇿ {P = P} {f = f} = record
310
Any (P ∘ f) xs ↔ Any P (List.map f xs)
311
map↔ {P = P} {f = f} = record
311
312
{ to = P.→-to-⟶ $ map⁺ {P = P} {f = f}
312
313
; from = P.→-to-⟶ $ map⁻ {P = P} {f = f}
313
314
; inverse-of = record
354
355
++⁻∘++⁺ (x ∷ xs) {ys} (inj₁ (there p)) rewrite ++⁻∘++⁺ xs {ys} (inj₁ p) = refl
355
356
++⁻∘++⁺ (x ∷ xs) (inj₂ p) rewrite ++⁻∘++⁺ xs (inj₂ p) = refl
357
++⇿ : ∀ {a p} {A : Set a} {P : A → Set p} {xs ys} →
358
(Any P xs ⊎ Any P ys) ⇿ Any P (xs ++ ys)
359
++⇿ {P = P} {xs = xs} = record
358
++↔ : ∀ {a p} {A : Set a} {P : A → Set p} {xs ys} →
359
(Any P xs ⊎ Any P ys) ↔ Any P (xs ++ ys)
360
++↔ {P = P} {xs = xs} = record
360
361
{ to = P.→-to-⟶ [ ++⁺ˡ {P = P}, ++⁺ʳ {P = P} xs ]′
361
362
; from = P.→-to-⟶ $ ++⁻ {P = P} xs
362
363
; inverse-of = record
445
455
rewrite concat⁻∘++⁺ʳ xs xss (concat⁺ p) =
446
456
P.cong there $ concat⁻∘concat⁺ p
448
concat⇿ : ∀ {a p} {A : Set a} {P : A → Set p} {xss} →
449
Any (Any P) xss ⇿ Any P (concat xss)
450
concat⇿ {P = P} {xss = xss} = record
458
concat↔ : ∀ {a p} {A : Set a} {P : A → Set p} {xss} →
459
Any (Any P) xss ↔ Any P (concat xss)
460
concat↔ {P = P} {xss = xss} = record
451
461
{ to = P.→-to-⟶ $ concat⁺ {P = P}
452
462
; from = P.→-to-⟶ $ concat⁻ {P = P} xss
453
463
; inverse-of = record
461
>>=⇿ : ∀ {ℓ p} {A B : Set ℓ} {P : B → Set p} {xs} {f : A → List B} →
462
Any (Any P ∘ f) xs ⇿ Any P (xs >>= f)
463
>>=⇿ {P = P} {xs} {f} =
464
Any (Any P ∘ f) xs ⇿⟨ map⇿ {P = Any P} {f = f} ⟩
465
Any (Any P) (List.map f xs) ⇿⟨ concat⇿ {P = P} ⟩
471
>>=↔ : ∀ {ℓ p} {A B : Set ℓ} {P : B → Set p} {xs} {f : A → List B} →
472
Any (Any P ∘ f) xs ↔ Any P (xs >>= f)
473
>>=↔ {P = P} {xs} {f} =
474
Any (Any P ∘ f) xs ↔⟨ map↔ {P = Any P} {f = f} ⟩
475
Any (Any P) (List.map f xs) ↔⟨ concat↔ {P = P} ⟩
466
476
Any P (xs >>= f) ∎
470
⊛⇿ : ∀ {ℓ} {A B : Set ℓ} {P : B → Set ℓ}
480
⊛↔ : ∀ {ℓ} {A B : Set ℓ} {P : B → Set ℓ}
471
481
{fs : List (A → B)} {xs : List A} →
472
Any (λ f → Any (P ∘ f) xs) fs ⇿ Any P (fs ⊛ xs)
473
⊛⇿ {ℓ} {P = P} {fs} {xs} =
474
Any (λ f → Any (P ∘ f) xs) fs ⇿⟨ Any-cong (λ _ → Any-cong (λ _ → return⇿ {a = ℓ} {p = ℓ}) (_ ∎)) (_ ∎) ⟩
475
Any (λ f → Any (Any P ∘ return ∘ f) xs) fs ⇿⟨ Any-cong (λ _ → >>=⇿ {ℓ = ℓ} {p = ℓ}) (_ ∎) ⟩
476
Any (λ f → Any P (xs >>= return ∘ f)) fs ⇿⟨ >>=⇿ {ℓ = ℓ} {p = ℓ} ⟩
482
Any (λ f → Any (P ∘ f) xs) fs ↔ Any P (fs ⊛ xs)
483
⊛↔ {ℓ} {P = P} {fs} {xs} =
484
Any (λ f → Any (P ∘ f) xs) fs ↔⟨ Any-cong (λ _ → Any-cong (λ _ → return↔ {a = ℓ} {p = ℓ}) (_ ∎)) (_ ∎) ⟩
485
Any (λ f → Any (Any P ∘ return ∘ f) xs) fs ↔⟨ Any-cong (λ _ → >>=↔ {ℓ = ℓ} {p = ℓ}) (_ ∎) ⟩
486
Any (λ f → Any P (xs >>= return ∘ f)) fs ↔⟨ >>=↔ {ℓ = ℓ} {p = ℓ} ⟩
477
487
Any P (fs ⊛ xs) ∎
479
489
-- An alternative introduction rule for _⊛_.
482
492
{fs : List (A → B)} {xs} →
483
493
Any (P ⟨→⟩ Q) fs → Any P xs → Any Q (fs ⊛ xs)
485
Inverse.to (⊛⇿ {ℓ = ℓ}) ⟨$⟩
495
Inverse.to (⊛↔ {ℓ = ℓ}) ⟨$⟩
486
496
Any.map (λ pq → Any.map (λ {x} → pq {x}) p) pq
490
⊗⇿ : ∀ {ℓ} {A B : Set ℓ} {P : A × B → Set ℓ}
500
⊗↔ : ∀ {ℓ} {A B : Set ℓ} {P : A × B → Set ℓ}
491
501
{xs : List A} {ys : List B} →
492
Any (λ x → Any (λ y → P (x , y)) ys) xs ⇿ Any P (xs ⊗ ys)
493
⊗⇿ {ℓ} {P = P} {xs} {ys} =
494
Any (λ x → Any (λ y → P (x , y)) ys) xs ⇿⟨ return⇿ {a = ℓ} {p = ℓ} ⟩
495
Any (λ _,_ → Any (λ x → Any (λ y → P (x , y)) ys) xs) (return _,_) ⇿⟨ ⊛⇿ ⟩
496
Any (λ x, → Any (P ∘ x,) ys) (_,_ <$> xs) ⇿⟨ ⊛⇿ ⟩
502
Any (λ x → Any (λ y → P (x , y)) ys) xs ↔ Any P (xs ⊗ ys)
503
⊗↔ {ℓ} {P = P} {xs} {ys} =
504
Any (λ x → Any (λ y → P (x , y)) ys) xs ↔⟨ return↔ {a = ℓ} {p = ℓ} ⟩
505
Any (λ _,_ → Any (λ x → Any (λ y → P (x , y)) ys) xs) (return _,_) ↔⟨ ⊛↔ ⟩
506
Any (λ x, → Any (P ∘ x,) ys) (_,_ <$> xs) ↔⟨ ⊛↔ ⟩
497
507
Any P (xs ⊗ ys) ∎
499
⊗⇿′ : {A B : Set} {P : A → Set} {Q : B → Set}
509
⊗↔′ : {A B : Set} {P : A → Set} {Q : B → Set}
500
510
{xs : List A} {ys : List B} →
501
(Any P xs × Any Q ys) ⇿ Any (P ⟨×⟩ Q) (xs ⊗ ys)
502
⊗⇿′ {P = P} {Q} {xs} {ys} =
503
(Any P xs × Any Q ys) ⇿⟨ ×⇿ ⟩
504
Any (λ x → Any (λ y → P x × Q y) ys) xs ⇿⟨ ⊗⇿ ⟩
511
(Any P xs × Any Q ys) ↔ Any (P ⟨×⟩ Q) (xs ⊗ ys)
512
⊗↔′ {P = P} {Q} {xs} {ys} =
513
(Any P xs × Any Q ys) ↔⟨ ×↔ ⟩
514
Any (λ x → Any (λ y → P x × Q y) ys) xs ↔⟨ ⊗↔ ⟩
505
515
Any (P ⟨×⟩ Q) (xs ⊗ ys) ∎
510
520
∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p} {xs : List A}
511
521
{f : ∀ {x} → x ∈ xs → B} →
512
(∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)) ⇿ Any P (map-with-∈ xs f)
513
map-with-∈⇿ {A = A} {B} {P} = record
522
(∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)) ↔ Any P (map-with-∈ xs f)
523
map-with-∈↔ {A = A} {B} {P} = record
514
524
{ to = P.→-to-⟶ (map-with-∈⁺ _)
515
525
; from = P.→-to-⟶ (map-with-∈⁻ _ _)
516
526
; inverse-of = record
568
578
any⁻ : ∀ {a} {A : Set a} (p : A → Bool) xs →
569
579
T (any p xs) → Any (T ∘ p) xs
571
any⁻ p (x ∷ xs) px∷xs with inspect (p x)
572
any⁻ p (x ∷ xs) px∷xs | true with-≡ eq = here (Equivalent.from T-≡ ⟨$⟩ eq)
573
any⁻ p (x ∷ xs) px∷xs | false with-≡ eq with p x
574
any⁻ p (x ∷ xs) pxs | false with-≡ refl | .false =
575
there (any⁻ p xs pxs)
581
any⁻ p (x ∷ xs) px∷xs with p x | inspect p x
582
any⁻ p (x ∷ xs) px∷xs | true | P[ eq ] = here (Equivalence.from T-≡ ⟨$⟩ eq)
583
any⁻ p (x ∷ xs) px∷xs | false | _ = there (any⁻ p xs px∷xs)
577
585
any⇔ : ∀ {a} {A : Set a} {p : A → Bool} {xs} →
578
586
Any (T ∘ p) xs ⇔ T (any p xs)
579
any⇔ = equivalent (any⁺ _) (any⁻ _ _)
587
any⇔ = Eq.equivalence (any⁺ _) (any⁻ _ _)
581
589
------------------------------------------------------------------------
582
590
-- _++_ is commutative
604
612
rewrite ++⁻∘++⁺ ys {ys = xs} (inj₁ p)
605
613
| ++⁻∘++⁺ ys {ys = x ∷ xs} (inj₁ p) = P.refl
607
++⇿++ : ∀ {a p} {A : Set a} {P : A → Set p} xs ys →
608
Any P (xs ++ ys) ⇿ Any P (ys ++ xs)
609
++⇿++ {P = P} xs ys = record
615
++↔++ : ∀ {a p} {A : Set a} {P : A → Set p} xs ys →
616
Any P (xs ++ ys) ↔ Any P (ys ++ xs)
617
++↔++ {P = P} xs ys = record
610
618
{ to = P.→-to-⟶ $ ++-comm {P = P} xs ys
611
619
; from = P.→-to-⟶ $ ++-comm {P = P} ys xs
612
620
; inverse-of = record
added
removed
src/Data/List/Any/Properties.agda
