```------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the Any predicate on colists
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --guardedness #-}

module Codata.Musical.Colist.Relation.Unary.Any.Properties where

open import Codata.Musical.Colist.Base
open import Codata.Musical.Colist.Bisimilarity
open import Codata.Musical.Colist.Relation.Unary.Any
open import Codata.Musical.Notation
open import Data.Maybe using (Is-just)
open import Data.Maybe.Relation.Unary.Any using (just)
open import Data.Nat.Base using (suc; _≥′_; ≤′-refl; ≤′-step)
open import Data.Nat.Properties using (s≤′s)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′; [_,_])
open import Function.Base using (_∋_; _∘_)
open import Function.Equality using (_⟨\$⟩_)
open import Function.Inverse as Inv using (_↔_; _↔̇_; Inverse; inverse)
open import Level using (Level; _⊔_)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.PropositionalEquality as P
using (_≡_; refl; cong)
open import Relation.Unary using (Pred)

private
variable
a b p q : Level
A : Set a
B : Set b
P : Pred A p
Q : Pred A q

------------------------------------------------------------------------
-- Equality properties

here-injective : ∀ {x xs p q} → (Any P (x ∷ xs) ∋ here p) ≡ here q → p ≡ q
here-injective refl = refl

there-injective : ∀ {x xs p q} → (Any P (x ∷ xs) ∋ there p) ≡ there q → p ≡ q
there-injective refl = refl

Any-resp : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q}
{xs ys} → (∀ {x} → P x → Q x) → xs ≈ ys →
Any P xs → Any Q ys
Any-resp f (x ∷ xs≈) (here px) = here (f px)
Any-resp f (x ∷ xs≈) (there p) = there (Any-resp f (♭ xs≈) p)

-- Any maps pointwise isomorphic predicates and equal colists to
-- isomorphic types.

Any-cong : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q}
{xs ys} → P ↔̇ Q → xs ≈ ys → Any P xs ↔ Any Q ys
Any-cong {A = A} {P} {Q} {xs} {ys} P↔Q = λ xs≈ys → record
{ to         = P.→-to-⟶ (to xs≈ys)
; from       = P.→-to-⟶ (from xs≈ys)
; inverse-of = record
{ left-inverse-of  = from∘to _
; right-inverse-of = to∘from _
}
}
where
open Setoid (setoid _) using (sym)

to : ∀ {xs ys} → xs ≈ ys → Any P xs → Any Q ys
to xs≈ys = Any-resp (Inverse.to P↔Q ⟨\$⟩_) xs≈ys

from : ∀ {xs ys} → xs ≈ ys → Any Q ys → Any P xs
from xs≈ys = Any-resp (Inverse.from P↔Q ⟨\$⟩_) (sym xs≈ys)

to∘from : ∀ {xs ys} (xs≈ys : xs ≈ ys) (q : Any Q ys) →
to xs≈ys (from xs≈ys q) ≡ q
to∘from (x ∷ xs≈) (there q) = P.cong there (to∘from (♭ xs≈) q)
to∘from (x ∷ xs≈) (here qx) =
P.cong here (Inverse.right-inverse-of P↔Q qx)

from∘to : ∀ {xs ys} (xs≈ys : xs ≈ ys) (p : Any P xs) →
from xs≈ys (to xs≈ys p) ≡ p
from∘to (x ∷ xs≈) (there p) = P.cong there (from∘to (♭ xs≈) p)
from∘to (x ∷ xs≈) (here px) =
P.cong here (Inverse.left-inverse-of P↔Q px)

------------------------------------------------------------------------
-- map

module _ {f : A → B} where

map⁻ : ∀ {xs} → Any P (map f xs) → Any (P ∘ f) xs
map⁻ {xs = x ∷ xs} (here px) = here px
map⁻ {xs = x ∷ xs} (there p) = there (map⁻ p)

map⁺ : ∀ {xs} → Any (P ∘ f) xs → Any P (map f xs)
map⁺ (here px) = here px
map⁺ (there p) = there (map⁺ p)

Any-map : ∀ {xs} → Any P (map f xs) ↔ Any (P ∘ f) xs
Any-map {xs = xs} = inverse map⁻ map⁺ from∘to to∘from where

from∘to : ∀ {xs} (p : Any P (map f xs)) → map⁺ (map⁻ p) ≡ p
from∘to {xs = x ∷ xs} (here px) = refl
from∘to {xs = x ∷ xs} (there p) = cong there (from∘to p)

to∘from : ∀ {xs} (p : Any (P ∘ f) xs) → map⁻ {P = P} (map⁺ p) ≡ p
to∘from (here px) = refl
to∘from (there p) = cong there (to∘from p)

------------------------------------------------------------------------
-- _⋎_

⋎⁻ : ∀ xs {ys} → Any P (xs ⋎ ys) → Any P xs ⊎ Any P ys
⋎⁻ []       p         = inj₂ p
⋎⁻ (x ∷ xs) (here px) = inj₁ (here px)
⋎⁻ (x ∷ xs) (there p) = [ inj₂ , inj₁ ∘ there ]′ (⋎⁻ _ p)

mutual

⋎⁺₁ : ∀ {xs ys} → Any P xs → Any P (xs ⋎ ys)
⋎⁺₁           (here px) = here px
⋎⁺₁ {ys = ys} (there p) = there (⋎⁺₂ ys p)

⋎⁺₂ : ∀ xs {ys} → Any P ys → Any P (xs ⋎ ys)
⋎⁺₂ []       p = p
⋎⁺₂ (x ∷ xs) p = there (⋎⁺₁ p)

⋎⁺ : ∀ xs {ys} → Any P xs ⊎ Any P ys → Any P (xs ⋎ ys)
⋎⁺ xs = [ ⋎⁺₁ , ⋎⁺₂ xs ]

Any-⋎ : ∀ {a p} {A : Set a} {P : A → Set p} xs {ys} →
Any P (xs ⋎ ys) ↔ (Any P xs ⊎ Any P ys)
Any-⋎ {P = P} = λ xs → record
{ to         = P.→-to-⟶ (⋎⁻ xs)
; from       = P.→-to-⟶ (⋎⁺ xs)
; inverse-of = record
{ left-inverse-of  = from∘to xs
; right-inverse-of = to∘from xs
}
}
where

from∘to : ∀ xs {ys} (p : Any P (xs ⋎ ys)) → ⋎⁺ xs (⋎⁻ xs p) ≡ p
from∘to []                 p                          = refl
from∘to (x ∷ xs)           (here px)                  = refl
from∘to (x ∷ xs) {ys = ys} (there p)                  with ⋎⁻ ys p | from∘to ys p
from∘to (x ∷ xs) {ys = ys} (there .(⋎⁺₁ q))     | inj₁ q | refl = refl
from∘to (x ∷ xs) {ys = ys} (there .(⋎⁺₂ ys q)) | inj₂ q | refl = refl

mutual

to∘from₁ : ∀ {xs ys} (p : Any P xs) →
⋎⁻ xs {ys = ys} (⋎⁺₁ p) ≡ inj₁ p
to∘from₁           (here px) = refl
to∘from₁ {ys = ys} (there p)
rewrite to∘from₂ ys p = refl

to∘from₂ : ∀ xs {ys} (p : Any P ys) →
⋎⁻ xs (⋎⁺₂ xs p) ≡ inj₂ p
to∘from₂ []                 p = refl
to∘from₂ (x ∷ xs) {ys = ys} p
rewrite to∘from₁ {xs = ys} {ys = ♭ xs} p = refl

to∘from : ∀ xs {ys} (p : Any P xs ⊎ Any P ys) → ⋎⁻ xs (⋎⁺ xs p) ≡ p
to∘from xs = [ to∘from₁ , to∘from₂ xs ]

------------------------------------------------------------------------
-- index

-- The position returned by index is guaranteed to be within bounds.

lookup-index : ∀ {xs} (p : Any P xs) → Is-just (lookup xs (index p))
lookup-index (here px) = just _
lookup-index (there p) = lookup-index p

-- Any-resp preserves the index.

index-Any-resp : ∀ {f : ∀ {x} → P x → Q x} {xs ys}
(xs≈ys : xs ≈ ys) (p : Any P xs) →
index (Any-resp f xs≈ys p) ≡ index p
index-Any-resp (x ∷ xs≈) (here px) = P.refl
index-Any-resp (x ∷ xs≈) (there p) =
cong suc (index-Any-resp (♭ xs≈) p)

-- The left-to-right direction of Any-⋎ returns a proof whose size is
-- no larger than that of the input proof.

index-Any-⋎ : ∀ xs {ys} (p : Any P (xs ⋎ ys)) →
index p ≥′ [ index , index ]′ (Inverse.to (Any-⋎ xs) ⟨\$⟩ p)
index-Any-⋎ []                 p         = ≤′-refl
index-Any-⋎ (x ∷ xs)           (here px) = ≤′-refl
index-Any-⋎ (x ∷ xs) {ys = ys} (there p)
with Inverse.to (Any-⋎ ys) ⟨\$⟩ p | index-Any-⋎ ys p
... | inj₁ q | q≤p = ≤′-step q≤p
... | inj₂ q | q≤p = s≤′s    q≤p
```