{-# OPTIONS --cubical-compatible --safe #-}
module Data.Vec.Relation.Unary.Any.Properties where
open import Data.Nat.Base using (suc; zero)
open import Data.Fin.Base using (Fin; zero; suc)
open import Data.Empty using (⊥)
open import Data.List.Base using ([]; _∷_)
import Data.List.Relation.Unary.Any as List
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
open import Data.Sum.Function.Propositional using (_⊎-cong_)
open import Data.Product.Base as Product using (∃; ∃₂; _×_; _,_; proj₁; proj₂)
open import Data.Vec.Base hiding (here; there)
open import Data.Vec.Relation.Unary.Any as Any using (Any; here; there)
open import Data.Vec.Membership.Propositional
using (_∈_; mapWith∈; find; lose)
open import Data.Vec.Relation.Binary.Pointwise.Inductive
using (Pointwise; []; _∷_)
open import Function.Base
open import Function.Bundles using (_↔_; mk↔ₛ′)
open import Function.Properties.Inverse using (↔-refl; ↔-trans)
open import Level using (Level)
open import Relation.Nullary.Negation using (¬_)
open import Relation.Unary hiding (_∈_)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Definitions using (_Respects_)
open import Relation.Binary.PropositionalEquality.Core
using (_≡_; refl; sym; trans; cong)
private
variable
a b p q r ℓ : Level
A : Set a
B : Set b
module _ {P : Pred A p} {_≈_ : Rel A ℓ} where
lift-resp : ∀ {n} → P Respects _≈_ → (Any P {n}) Respects (Pointwise _≈_)
lift-resp resp (x∼y ∷ xs∼ys) (here px) = here (resp x∼y px)
lift-resp resp (x∼y ∷ xs∼ys) (there pxs) = there (lift-resp resp xs∼ys pxs)
module _ {P : Pred A p} where
here-injective : ∀ {n x xs} {p q : P x} →
here {P = P} {n = n} {xs = xs} p ≡ here q → p ≡ q
here-injective refl = refl
there-injective : ∀ {n x xs} {p q : Any P xs} →
there {n = n} {x = x} p ≡ there q → p ≡ q
there-injective refl = refl
¬Any[] : ¬ Any P []
¬Any[] ()
lookup-index : ∀ {m} {xs : Vec A m} (p : Any P xs) →
P (lookup xs (Any.index p))
lookup-index (here px) = px
lookup-index (there p) = lookup-index p
fromList⁺ : ∀ {xs} → List.Any P xs → Any P (fromList xs)
fromList⁺ (List.here px) = here px
fromList⁺ (List.there v) = there (fromList⁺ v)
fromList⁻ : ∀ {xs} → Any P (fromList xs) → List.Any P xs
fromList⁻ {x ∷ xs} (here px) = List.here px
fromList⁻ {x ∷ xs} (there pxs) = List.there (fromList⁻ pxs)
toList⁺ : ∀ {n} {xs : Vec A n} → Any P xs → List.Any P (toList xs)
toList⁺ (here px) = List.here px
toList⁺ (there v) = List.there (toList⁺ v)
toList⁻ : ∀ {n} {xs : Vec A n} → List.Any P (toList xs) → Any P xs
toList⁻ {xs = x ∷ xs} (List.here px) = here px
toList⁻ {xs = x ∷ xs} (List.there pxs) = there (toList⁻ pxs)
map-id : ∀ {P : Pred A p} (f : P ⊆ P) {n xs} →
(∀ {x} (p : P x) → f p ≡ p) →
(p : Any P {n} xs) → Any.map f p ≡ p
map-id f hyp (here p) = cong here (hyp p)
map-id f hyp (there p) = cong there $ map-id f hyp p
map-∘ : ∀ {P : Pred A p} {Q : A → Set q} {R : A → Set r}
(f : Q ⊆ R) (g : P ⊆ Q)
{n xs} (p : Any P {n} xs) →
Any.map (f ∘ g) p ≡ Any.map f (Any.map g p)
map-∘ f g (here p) = refl
map-∘ f g (there p) = cong there $ map-∘ f g p
module _ {P : A → B → Set ℓ} where
swap : ∀ {n m} {xs : Vec A n} {ys : Vec B m} →
Any (λ x → Any (P x) ys) xs →
Any (λ y → Any (flip P y) xs) ys
swap (here pys) = Any.map here pys
swap (there pxys) = Any.map there (swap pxys)
swap-there : ∀ {n m x xs ys} → (any : Any (λ x → Any (P x) {n} ys) {m} xs) →
swap (Any.map (there {x = x}) any) ≡ there (swap any)
swap-there (here pys) = refl
swap-there (there pxys) = cong (Any.map there) (swap-there pxys)
module _ {P : A → B → Set ℓ} where
swap-invol : ∀ {n m} {xs : Vec A n} {ys : Vec B m} →
(any : Any (λ x → Any (P x) ys) xs) →
swap (swap any) ≡ any
swap-invol (here (here _)) = refl
swap-invol (here (there pys)) = cong (Any.map there) (swap-invol (here pys))
swap-invol (there pxys) = trans (swap-there (swap pxys))
$ cong there (swap-invol pxys)
module _ {P : A → B → Set ℓ} where
swap↔ : ∀ {n m} {xs : Vec A n} {ys : Vec B m} →
Any (λ x → Any (P x) ys) xs ↔ Any (λ y → Any (flip P y) xs) ys
swap↔ = mk↔ₛ′ swap swap swap-invol swap-invol
⊥↔Any⊥ : ∀ {n} {xs : Vec A n} → ⊥ ↔ Any (const ⊥) xs
⊥↔Any⊥ = mk↔ₛ′ (λ ()) (λ p → from p) (λ p → from p) (λ ())
where
from : ∀ {n xs} → Any (const ⊥) {n} xs → ∀ {b} {B : Set b} → B
from (there p) = from p
⊥↔Any[] : ∀ {P : Pred A p} → ⊥ ↔ Any P []
⊥↔Any[] = mk↔ₛ′ (λ()) (λ()) (λ()) (λ())
module _ {P : Pred A p} {Q : A → Set q} where
Any-⊎⁺ : ∀ {n} {xs : Vec A n} → Any P xs ⊎ Any Q xs → Any (λ x → P x ⊎ Q x) xs
Any-⊎⁺ = [ Any.map inj₁ , Any.map inj₂ ]′
Any-⊎⁻ : ∀ {n} {xs : Vec A n} → Any (λ x → P x ⊎ Q x) xs → Any P xs ⊎ Any Q xs
Any-⊎⁻ (here (inj₁ p)) = inj₁ (here p)
Any-⊎⁻ (here (inj₂ q)) = inj₂ (here q)
Any-⊎⁻ (there p) = Sum.map there there (Any-⊎⁻ p)
⊎↔ : ∀ {n} {xs : Vec A n} → (Any P xs ⊎ Any Q xs) ↔ Any (λ x → P x ⊎ Q x) xs
⊎↔ = mk↔ₛ′ Any-⊎⁺ Any-⊎⁻ to∘from from∘to
where
from∘to : ∀ {n} {xs : Vec A n} (p : Any P xs ⊎ Any Q xs) → Any-⊎⁻ (Any-⊎⁺ p) ≡ p
from∘to (inj₁ (here p)) = refl
from∘to (inj₁ (there p)) rewrite from∘to (inj₁ p) = refl
from∘to (inj₂ (here q)) = refl
from∘to (inj₂ (there q)) rewrite from∘to (inj₂ q) = refl
to∘from : ∀ {n} {xs : Vec A n} (p : Any (λ x → P x ⊎ Q x) xs) →
Any-⊎⁺ (Any-⊎⁻ p) ≡ p
to∘from (here (inj₁ p)) = refl
to∘from (here (inj₂ q)) = refl
to∘from (there p) with Any-⊎⁻ p | to∘from p
to∘from (there .(Any.map inj₁ p)) | inj₁ p | refl = refl
to∘from (there .(Any.map inj₂ q)) | inj₂ q | refl = refl
module _ {P : Pred A p} {Q : Pred B q} where
Any-×⁺ : ∀ {n m} {xs : Vec A n} {ys : Vec B m} → Any P xs × Any Q ys →
Any (λ x → Any (λ y → P x × Q y) ys) xs
Any-×⁺ (p , q) = Any.map (λ p → Any.map (p ,_) q) p
Any-×⁻ : ∀ {n m} {xs : Vec A n} {ys : Vec B m} →
Any (λ x → Any (λ y → P x × Q y) ys) xs →
Any P xs × Any Q ys
Any-×⁻ pq with find pq
... | x , x∈xs , pxys with find pxys
... | y , y∈ys , px , py = lose x∈xs px , lose y∈ys py
module _ {P : Pred A p} where
singleton⁺ : ∀ {x} → P x → Any P [ x ]
singleton⁺ Px = here Px
singleton⁻ : ∀ {x} → Any P [ x ] → P x
singleton⁻ (here Px) = Px
singleton⁺∘singleton⁻ : ∀ {x} (p : Any P [ x ]) →
singleton⁺ (singleton⁻ p) ≡ p
singleton⁺∘singleton⁻ (here px) = refl
singleton⁻∘singleton⁺ : ∀ {x} (p : P x) →
singleton⁻ (singleton⁺ p) ≡ p
singleton⁻∘singleton⁺ p = refl
singleton↔ : ∀ {x} → P x ↔ Any P [ x ]
singleton↔ = mk↔ₛ′ singleton⁺ singleton⁻ singleton⁺∘singleton⁻ singleton⁻∘singleton⁺
module _ {f : A → B} where
map⁺ : ∀ {P : Pred B p} {n} {xs : Vec A n} →
Any (P ∘ f) xs → Any P (map f xs)
map⁺ (here p) = here p
map⁺ (there p) = there $ map⁺ p
map⁻ : ∀ {P : Pred B p} {n} {xs : Vec A n} →
Any P (map f xs) → Any (P ∘ f) xs
map⁻ {xs = x ∷ xs} (here p) = here p
map⁻ {xs = x ∷ xs} (there p) = there $ map⁻ p
map⁺∘map⁻ : ∀ {P : Pred B p} {n} {xs : Vec A n} →
(p : Any P (map f xs)) → map⁺ (map⁻ p) ≡ p
map⁺∘map⁻ {xs = x ∷ xs} (here p) = refl
map⁺∘map⁻ {xs = x ∷ xs} (there p) = cong there (map⁺∘map⁻ p)
map⁻∘map⁺ : ∀ (P : Pred B p) {n} {xs : Vec A n} →
(p : Any (P ∘ f) xs) → map⁻ {P = P} (map⁺ p) ≡ p
map⁻∘map⁺ P (here p) = refl
map⁻∘map⁺ P (there p) = cong there (map⁻∘map⁺ P p)
map↔ : ∀ {P : Pred B p} {n} {xs : Vec A n} →
Any (P ∘ f) xs ↔ Any P (map f xs)
map↔ = mk↔ₛ′ map⁺ map⁻ map⁺∘map⁻ (map⁻∘map⁺ _)
module _ {P : Pred A p} where
++⁺ˡ : ∀ {n m} {xs : Vec A n} {ys : Vec A m} → Any P xs → Any P (xs ++ ys)
++⁺ˡ (here p) = here p
++⁺ˡ (there p) = there (++⁺ˡ p)
++⁺ʳ : ∀ {n m} (xs : Vec A n) {ys : Vec A m} → Any P ys → Any P (xs ++ ys)
++⁺ʳ [] p = p
++⁺ʳ (x ∷ xs) p = there (++⁺ʳ xs p)
++⁻ : ∀ {n m} (xs : Vec A n) {ys : Vec A m} → Any P (xs ++ ys) → Any P xs ⊎ Any P ys
++⁻ [] p = inj₂ p
++⁻ (x ∷ xs) (here p) = inj₁ (here p)
++⁻ (x ∷ xs) (there p) = Sum.map there id (++⁻ xs p)
++⁺∘++⁻ : ∀ {n m} (xs : Vec A n) {ys : Vec A m} (p : Any P (xs ++ ys)) →
[ ++⁺ˡ , ++⁺ʳ xs ]′ (++⁻ xs p) ≡ p
++⁺∘++⁻ [] p = refl
++⁺∘++⁻ (x ∷ xs) (here p) = refl
++⁺∘++⁻ (x ∷ xs) (there p) with ++⁻ xs p | ++⁺∘++⁻ xs p
++⁺∘++⁻ (x ∷ xs) (there p) | inj₁ p′ | ih = cong there ih
++⁺∘++⁻ (x ∷ xs) (there p) | inj₂ p′ | ih = cong there ih
++⁻∘++⁺ : ∀ {n m} (xs : Vec A n) {ys : Vec A m} (p : Any P xs ⊎ Any P ys) →
++⁻ xs ([ ++⁺ˡ , ++⁺ʳ xs ]′ p) ≡ p
++⁻∘++⁺ [] (inj₂ p) = refl
++⁻∘++⁺ (x ∷ xs) (inj₁ (here p)) = refl
++⁻∘++⁺ (x ∷ xs) {ys} (inj₁ (there p)) rewrite ++⁻∘++⁺ xs {ys} (inj₁ p) = refl
++⁻∘++⁺ (x ∷ xs) (inj₂ p) rewrite ++⁻∘++⁺ xs (inj₂ p) = refl
++↔ : ∀ {n m} {xs : Vec A n} {ys : Vec A m} →
(Any P xs ⊎ Any P ys) ↔ Any P (xs ++ ys)
++↔ {xs = xs} = mk↔ₛ′ [ ++⁺ˡ , ++⁺ʳ xs ]′ (++⁻ xs) (++⁺∘++⁻ xs) (++⁻∘++⁺ xs)
++-comm : ∀ {n m} (xs : Vec A n) (ys : Vec A m) →
Any P (xs ++ ys) → Any P (ys ++ xs)
++-comm xs ys = [ ++⁺ʳ ys , ++⁺ˡ ]′ ∘ ++⁻ xs
++-comm∘++-comm : ∀ {n m} (xs : Vec A n) {ys : Vec A m} (p : Any P (xs ++ ys)) →
++-comm ys xs (++-comm xs ys p) ≡ p
++-comm∘++-comm [] {ys} p
rewrite ++⁻∘++⁺ ys {ys = []} (inj₁ p) = refl
++-comm∘++-comm (x ∷ xs) {ys} (here p)
rewrite ++⁻∘++⁺ ys {ys = x ∷ xs} (inj₂ (here p)) = refl
++-comm∘++-comm (x ∷ xs) (there p) with ++⁻ xs p | ++-comm∘++-comm xs p
++-comm∘++-comm (x ∷ xs) {ys} (there .([ ++⁺ʳ xs , ++⁺ˡ ]′ (++⁻ ys (++⁺ʳ ys p))))
| inj₁ p | refl
rewrite ++⁻∘++⁺ ys (inj₂ p)
| ++⁻∘++⁺ ys (inj₂ $ there {x = x} p) = refl
++-comm∘++-comm (x ∷ xs) {ys} (there .([ ++⁺ʳ xs , ++⁺ˡ ]′ (++⁻ ys (++⁺ˡ p))))
| inj₂ p | refl
rewrite ++⁻∘++⁺ ys {ys = xs} (inj₁ p)
| ++⁻∘++⁺ ys {ys = x ∷ xs} (inj₁ p) = refl
++↔++ : ∀ {n m} (xs : Vec A n) (ys : Vec A m) → Any P (xs ++ ys) ↔ Any P (ys ++ xs)
++↔++ xs ys = mk↔ₛ′ (++-comm xs ys) (++-comm ys xs)
(++-comm∘++-comm ys) (++-comm∘++-comm xs)
++-insert : ∀ {n m x} (xs : Vec A n) {ys : Vec A m} → P x → Any P (xs ++ [ x ] ++ ys)
++-insert xs Px = ++⁺ʳ xs (++⁺ˡ (singleton⁺ Px))
module _ {P : Pred A p} where
concat⁺ : ∀ {n m} {xss : Vec (Vec A n) m} → Any (Any P) xss → Any P (concat xss)
concat⁺ (here p) = ++⁺ˡ p
concat⁺ (there {x = xs} p) = ++⁺ʳ xs (concat⁺ p)
concat⁻ : ∀ {n m} (xss : Vec (Vec A n) m) → Any P (concat xss) → Any (Any P) xss
concat⁻ (xs ∷ xss) p = [ here , there ∘ concat⁻ xss ]′ (++⁻ xs p)
concat⁻∘++⁺ˡ : ∀ {n m xs} (xss : Vec (Vec A n) m) (p : Any P xs) →
concat⁻ (xs ∷ xss) (++⁺ˡ p) ≡ here p
concat⁻∘++⁺ˡ xss p rewrite ++⁻∘++⁺ _ {concat xss} (inj₁ p) = refl
concat⁻∘++⁺ʳ : ∀ {n m} xs (xss : Vec (Vec A n) m) (p : Any P (concat xss)) →
concat⁻ (xs ∷ xss) (++⁺ʳ xs p) ≡ there (concat⁻ xss p)
concat⁻∘++⁺ʳ xs xss p rewrite ++⁻∘++⁺ xs (inj₂ p) = refl
concat⁺∘concat⁻ : ∀ {n m} (xss : Vec (Vec A n) m) (p : Any P (concat xss)) →
concat⁺ (concat⁻ xss p) ≡ p
concat⁺∘concat⁻ (xs ∷ xss) p with ++⁻ xs p in eq
... | inj₁ pxs
= trans (cong [ ++⁺ˡ , ++⁺ʳ xs ]′ (sym eq))
$ ++⁺∘++⁻ xs p
... | inj₂ pxss rewrite concat⁺∘concat⁻ xss pxss
= trans (cong [ ++⁺ˡ , ++⁺ʳ xs ]′ (sym eq))
$ ++⁺∘++⁻ xs p
concat⁻∘concat⁺ : ∀ {n m} {xss : Vec (Vec A n) m} (p : Any (Any P) xss) →
concat⁻ xss (concat⁺ p) ≡ p
concat⁻∘concat⁺ {xss = xs ∷ xss} (here p)
rewrite ++⁻∘++⁺ xs {concat xss} (inj₁ p) = refl
concat⁻∘concat⁺ {xss = xs ∷ xss} (there p)
rewrite ++⁻∘++⁺ xs {concat xss} (inj₂ (concat⁺ p))
| concat⁻∘concat⁺ p = refl
concat↔ : ∀ {n m} {xss : Vec (Vec A n) m} → Any (Any P) xss ↔ Any P (concat xss)
concat↔ {xss = xss} = mk↔ₛ′ concat⁺ (concat⁻ xss) (concat⁺∘concat⁻ xss) concat⁻∘concat⁺
module _ {P : Pred A p} where
tabulate⁺ : ∀ {n} {f : Fin n → A} i → P (f i) → Any P (tabulate f)
tabulate⁺ zero p = here p
tabulate⁺ (suc i) p = there (tabulate⁺ i p)
tabulate⁻ : ∀ {n} {f : Fin n → A} →
Any P (tabulate f) → ∃ λ i → P (f i)
tabulate⁻ (here p) = zero , p
tabulate⁻ (there p) = Product.map suc id (tabulate⁻ p)
module _ {P : Pred B p} where
mapWith∈⁺ : ∀ {n} {xs : Vec A n} (f : ∀ {x} → x ∈ xs → B) →
(∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)) →
Any P (mapWith∈ xs f)
mapWith∈⁺ f (_ , here refl , p) = here p
mapWith∈⁺ f (_ , there x∈xs , p) =
there $ mapWith∈⁺ (f ∘ there) (_ , x∈xs , p)
mapWith∈⁻ : ∀ {n} (xs : Vec A n) (f : ∀ {x} → x ∈ xs → B) →
Any P (mapWith∈ xs f) →
∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)
mapWith∈⁻ (y ∷ xs) f (here p) = (y , here refl , p)
mapWith∈⁻ (y ∷ xs) f (there p) =
Product.map id (Product.map there id) $ mapWith∈⁻ xs (f ∘ there) p
mapWith∈↔ : ∀ {n} {xs : Vec A n} {f : ∀ {x} → x ∈ xs → B} →
(∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)) ↔ Any P (mapWith∈ xs f)
mapWith∈↔ = mk↔ₛ′ (mapWith∈⁺ _) (mapWith∈⁻ _ _) (to∘from _ _) (from∘to _)
where
from∘to : ∀ {n} {xs : Vec A n} (f : ∀ {x} → x ∈ xs → B)
(p : ∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)) →
mapWith∈⁻ xs f (mapWith∈⁺ f p) ≡ p
from∘to f (_ , here refl , p) = refl
from∘to f (_ , there x∈xs , p)
rewrite from∘to (f ∘ there) (_ , x∈xs , p) = refl
to∘from : ∀ {n} (xs : Vec A n) (f : ∀ {x} → x ∈ xs → B)
(p : Any P (mapWith∈ xs f)) →
mapWith∈⁺ f (mapWith∈⁻ xs f p) ≡ p
to∘from (y ∷ xs) f (here p) = refl
to∘from (y ∷ xs) f (there p) =
cong there $ to∘from xs (f ∘ there) p
∷↔ : ∀ {n} (P : Pred A p) {x} {xs : Vec A n} →
(P x ⊎ Any P xs) ↔ Any P (x ∷ xs)
∷↔ P {x} {xs} = ↔-trans (singleton↔ ⊎-cong ↔-refl) ++↔
module _ {A B : Set a} {P : Pred B p} {m} {f : A → Vec B m} where
open CartesianBind
>>=↔ : ∀ {n} {xs : Vec A n} → Any (Any P ∘ f) xs ↔ Any P (xs >>= f)
>>=↔ = ↔-trans map↔ concat↔