------------------------------------------------------------------------
-- The Agda standard library
--
-- Pointwise lifting of relations to vectors
------------------------------------------------------------------------

module Relation.Binary.Vec.Pointwise where

open import Category.Applicative.Indexed
open import Data.Fin
open import Data.Nat
open import Data.Plus as Plus hiding (equivalent; map)
open import Data.Vec as Vec hiding ([_]; head; tail; map)
import Data.Vec.Properties as VecProp
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence as Equiv
  using (_⇔_; ⇔-setoid; module Equivalence)
import Level
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec

-- Functional definition.

record Pointwise {ℓ} {A B : Set ℓ} (_∼_ : REL A B ℓ)
                 {n} (xs : Vec A n) (ys : Vec B n) : Set ℓ where
  constructor ext
  field app : ∀ i → lookup i xs ∼ lookup i ys

-- Inductive definition.

infixr  _∷_

data Pointwise′ {ℓ} {A B : Set ℓ} (_∼_ : REL A B ℓ) :
                ∀ {n} (xs : Vec A n) (ys : Vec B n) → Set ℓ where
  []  : Pointwise′ _∼_ [] []
  _∷_ : ∀ {n x y} {xs : Vec A n} {ys : Vec B n}
        (x∼y : x ∼ y) (xs∼ys : Pointwise′ _∼_ xs ys) →
        Pointwise′ _∼_ (x ∷ xs) (y ∷ ys)

-- The two definitions are equivalent.

equivalent : ∀ {ℓ} {A B : Set ℓ} {_∼_ : REL A B ℓ} {n}
               {xs : Vec A n} {ys : Vec B n} →
             Pointwise _∼_ xs ys ⇔ Pointwise′ _∼_ xs ys
equivalent {A = A} {B} {_∼_} = Equiv.equivalence (to _ _) from
  where
  to : ∀ {n} (xs : Vec A n) (ys : Vec B n) →
       Pointwise _∼_ xs ys → Pointwise′ _∼_ xs ys
  to []       []       xs∼ys = []
  to (x ∷ xs) (y ∷ ys) xs∼ys =
    Pointwise.app xs∼ys zero ∷
    to xs ys (ext (Pointwise.app xs∼ys ∘ suc))

  nil : Pointwise _∼_ [] []
  nil = ext λ()

  cons : ∀ {n x y} {xs : Vec A n} {ys : Vec B n} →
         x ∼ y → Pointwise _∼_ xs ys → Pointwise _∼_ (x ∷ xs) (y ∷ ys)
  cons {x = x} {y} {xs} {ys} x∼y xs∼ys = ext helper
    where
    helper : ∀ i → lookup i (x ∷ xs) ∼ lookup i (y ∷ ys)
    helper zero    = x∼y
    helper (suc i) = Pointwise.app xs∼ys i

  from : ∀ {n} {xs : Vec A n} {ys : Vec B n} →
         Pointwise′ _∼_ xs ys → Pointwise _∼_ xs ys
  from []            = nil
  from (x∼y ∷ xs∼ys) = cons x∼y (from xs∼ys)

-- Some destructors.

head : ∀ {ℓ} {A B : Set ℓ} {_∼_ : REL A B ℓ} {n x y xs} {ys : Vec B n} →
       Pointwise′ _∼_ (x ∷ xs) (y ∷ ys) → x ∼ y
head (x∼y ∷ xs∼ys) = x∼y

tail : ∀ {ℓ} {A B : Set ℓ} {_∼_ : REL A B ℓ} {n x y xs} {ys : Vec B n} →
       Pointwise′ _∼_ (x ∷ xs) (y ∷ ys) → Pointwise′ _∼_ xs ys
tail (x∼y ∷ xs∼ys) = xs∼ys

-- Pointwise preserves reflexivity.

refl : ∀ {ℓ} {A : Set ℓ} {_∼_ : Rel A ℓ} {n} →
       Reflexive _∼_ → Reflexive (Pointwise _∼_ {n = n})
refl rfl = ext (λ _ → rfl)

-- Pointwise preserves symmetry.

sym : ∀ {ℓ} {A B : Set ℓ} {P : REL A B ℓ} {Q : REL B A ℓ} {n} →
      Sym P Q → Sym (Pointwise P) (Pointwise Q {n = n})
sym sm xs∼ys = ext λ i → sm (Pointwise.app xs∼ys i)

-- Pointwise preserves transitivity.

trans : ∀ {ℓ} {A B C : Set ℓ}
          {P : REL A B ℓ} {Q : REL B C ℓ} {R : REL A C ℓ} {n} →
        Trans P Q R →
        Trans (Pointwise P) (Pointwise Q) (Pointwise R {n = n})
trans trns xs∼ys ys∼zs = ext λ i →
  trns (Pointwise.app xs∼ys i) (Pointwise.app ys∼zs i)

-- Pointwise preserves equivalences.

isEquivalence :
  ∀ {ℓ} {A : Set ℓ} {_∼_ : Rel A ℓ} {n} →
  IsEquivalence _∼_ → IsEquivalence (Pointwise _∼_ {n = n})
isEquivalence equiv = record
  { refl  = refl  (IsEquivalence.refl  equiv)
  ; sym   = sym   (IsEquivalence.sym   equiv)
  ; trans = trans (IsEquivalence.trans equiv)
  }

-- Pointwise preserves decidability.

decidable : ∀ {ℓ} {A B : Set ℓ} {_∼_ : REL A B ℓ} →
            Decidable _∼_ → ∀ {n} → Decidable (Pointwise _∼_ {n = n})
decidable {_∼_ = _∼_} dec xs ys =
  Dec.map (Setoid.sym (⇔-setoid _) equivalent) (decidable′ xs ys)
  where
  decidable′ : ∀ {n} → Decidable (Pointwise′ _∼_ {n = n})
  decidable′ []       []       = yes []
  decidable′ (x ∷ xs) (y ∷ ys) with dec x y
  ... | no ¬x∼y = no (¬x∼y ∘ head)
  ... | yes x∼y with decidable′ xs ys
  ...   | no ¬xs∼ys = no (¬xs∼ys ∘ tail)
  ...   | yes xs∼ys = yes (x∼y ∷ xs∼ys)

-- Pointwise _≡_ is equivalent to _≡_.

Pointwise-≡ : ∀ {ℓ} {A : Set ℓ} {n} {xs ys : Vec A n} →
              Pointwise _≡_ xs ys ⇔ xs ≡ ys
Pointwise-≡ {ℓ} {A} =
  Equiv.equivalence
    (to ∘ _⟨$⟩_ {f₂ = ℓ} (Equivalence.to equivalent))
    (λ xs≡ys → P.subst (Pointwise _≡_ _) xs≡ys (refl P.refl))
  where
  to : ∀ {n} {xs ys : Vec A n} → Pointwise′ _≡_ xs ys → xs ≡ ys
  to []               = P.refl
  to (P.refl ∷ xs∼ys) = P.cong (_∷_ _) $ to xs∼ys

-- Pointwise and Plus commute when the underlying relation is
-- reflexive.

⁺∙⇒∙⁺ : ∀ {ℓ} {A : Set ℓ} {_∼_ : Rel A ℓ} {n} {xs ys : Vec A n} →
        Plus (Pointwise _∼_) xs ys → Pointwise (Plus _∼_) xs ys
⁺∙⇒∙⁺ [ ρ≈ρ′ ]             = ext (λ x → [ Pointwise.app ρ≈ρ′ x ])
⁺∙⇒∙⁺ (ρ ∼⁺⟨ ρ≈ρ′ ⟩ ρ′≈ρ″) =
  ext (λ x → _ ∼⁺⟨ Pointwise.app (⁺∙⇒∙⁺ ρ≈ρ′ ) x ⟩
                   Pointwise.app (⁺∙⇒∙⁺ ρ′≈ρ″) x)

∙⁺⇒⁺∙ : ∀ {ℓ} {A : Set ℓ} {_∼_ : Rel A ℓ} {n} {xs ys : Vec A n} →
        Reflexive _∼_ →
        Pointwise (Plus _∼_) xs ys → Plus (Pointwise _∼_) xs ys
∙⁺⇒⁺∙ {ℓ} {A} {_∼_} x∼x =
  Plus.map (_⟨$⟩_ {f₂ = ℓ} (Equivalence.from equivalent)) ∘
  helper ∘
  _⟨$⟩_ {f₂ = ℓ} (Equivalence.to equivalent)
  where
  helper : ∀ {n} {xs ys : Vec A n} →
           Pointwise′ (Plus _∼_) xs ys → Plus (Pointwise′ _∼_) xs ys
  helper []                                                  = [ [] ]
  helper (_∷_ {x = x} {y = y} {xs = xs} {ys = ys} x∼y xs∼ys) =
    x ∷ xs  ∼⁺⟨ Plus.map (λ x∼y   → x∼y ∷ xs∼xs) x∼y ⟩
    y ∷ xs  ∼⁺⟨ Plus.map (λ xs∼ys → x∼x ∷ xs∼ys) (helper xs∼ys) ⟩∎
    y ∷ ys  ∎
    where
    xs∼xs : Pointwise′ _∼_ xs xs
    xs∼xs = _⟨$⟩_ {f₂ = ℓ} (Equivalence.to equivalent) (refl x∼x)

-- Note that ∙⁺⇒⁺∙ cannot be defined if the requirement of reflexivity
-- is dropped.

private

 module Counterexample where

  data D : Set where
    i j x y z : D

  data _R_ : Rel D Level.zero where
    iRj : i R j
    xRy : x R y
    yRz : y R z

  xR⁺z : x [ _R_ ]⁺ z
  xR⁺z =
    x  ∼⁺⟨ [ xRy ] ⟩
    y  ∼⁺⟨ [ yRz ] ⟩∎
    z  ∎

  ix : Vec D 
  ix = i ∷ x ∷ []

  jz : Vec D 
  jz = j ∷ z ∷ []

  ix∙⁺jz : Pointwise′ (Plus _R_) ix jz
  ix∙⁺jz = [ iRj ] ∷ xR⁺z ∷ []

  ¬ix⁺∙jz : ¬ Plus′ (Pointwise′ _R_) ix jz
  ¬ix⁺∙jz [ iRj ∷ () ∷ [] ]
  ¬ix⁺∙jz ((iRj ∷ xRy ∷ []) ∷ [ () ∷ yRz ∷ [] ])
  ¬ix⁺∙jz ((iRj ∷ xRy ∷ []) ∷ (() ∷ yRz ∷ []) ∷ _)

  counterexample :
    ¬ (∀ {n} {xs ys : Vec D n} →
         Pointwise (Plus _R_) xs ys →
         Plus (Pointwise _R_) xs ys)
  counterexample ∙⁺⇒⁺∙ =
    ¬ix⁺∙jz (Equivalence.to Plus.equivalent ⟨$⟩
               Plus.map (_⟨$⟩_ (Equivalence.to equivalent))
                 (∙⁺⇒⁺∙ (Equivalence.from equivalent ⟨$⟩ ix∙⁺jz)))

-- Map.

map : ∀ {ℓ} {A : Set ℓ} {_R_ _R′_ : Rel A ℓ} {n} →
      _R_ ⇒ _R′_ → Pointwise _R_ ⇒ Pointwise _R′_ {n}
map R⇒R′ xsRys = ext λ i →
  R⇒R′ (Pointwise.app xsRys i)

-- A variant.

gmap : ∀ {ℓ} {A A′ : Set ℓ}
         {_R_ : Rel A ℓ} {_R′_ : Rel A′ ℓ} {f : A → A′} {n} →
       _R_ =[ f ]⇒ _R′_ →
       Pointwise _R_ =[ Vec.map {n = n} f ]⇒ Pointwise _R′_
gmap {_R′_ = _R′_} {f} R⇒R′ {i = xs} {j = ys} xsRys = ext λ i →
  let module M = Morphism (VecProp.lookup-morphism i) in
  P.subst₂ _R′_ (P.sym $ M.op-<$> f xs)
                (P.sym $ M.op-<$> f ys)
                (R⇒R′ (Pointwise.app xsRys i))