------------------------------------------------------------------------
-- 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.Bundles
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} → (∀ {i} → P i ↔ Q i) → xs ≈ ys → Any P xs ↔ Any Q ys
Any-cong {A = A} {P} {Q} {xs} {ys} P↔Q xs≈ys =
  mk↔ₛ′ (to xs≈ys) (from xs≈ys) (to∘from _) (from∘to _)
  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.strictlyInverseˡ 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.strictlyInverseʳ 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} = mk↔ₛ′ map⁻ map⁺ to∘from from∘to
    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 = mk↔ₛ′ (⋎⁻ xs) (⋎⁺ xs) (to∘from xs) (from∘to 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