------------------------------------------------------------------------
-- 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 ([_]; map)
import Data.Vec.Properties as VecProp
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence as Equiv
  using (_⇔_; module Equivalence)
import Level
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary

private
 module Dummy {a} {A : Set a} where

  -- Functional definition.

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

  -- Inductive definition.

  infixr  _∷_

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

  -- The two definitions are equivalent.

  equivalent : ∀ {_∼_ : Rel A a} {n} {xs ys : Vec A n} →
               Pointwise _∼_ xs ys ⇔ Pointwise′ _∼_ xs ys
  equivalent {_∼_} = Equiv.equivalence (to _ _) from
    where
    to : ∀ {n} (xs ys : Vec A 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 ys : Vec A 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 ys : Vec A n} →
           Pointwise′ _∼_ xs ys → Pointwise _∼_ xs ys
    from []            = nil
    from (x∼y ∷ xs∼ys) = cons x∼y (from xs∼ys)

  -- Pointwise preserves reflexivity.

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

  -- Pointwise preserves symmetry.

  sym : ∀ {_∼_ : Rel A a} {n} →
        Symmetric _∼_ → Symmetric (Pointwise _∼_ {n = n})
  sym sm xs∼ys = ext λ i → sm (Pointwise.app xs∼ys i)

  -- Pointwise preserves transitivity.

  trans : ∀ {_∼_ : Rel A a} {n} →
        Transitive _∼_ → Transitive (Pointwise _∼_ {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 :
    ∀ {_∼_ : Rel A 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 _≡_ is equivalent to _≡_.

  Pointwise-≡ : ∀ {n} {xs ys : Vec A n} →
                Pointwise _≡_ xs ys ⇔ xs ≡ ys
  Pointwise-≡ =
    Equiv.equivalence
      (to ∘ _⟨$⟩_ (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.

  ⁺∙⇒∙⁺ : ∀ {_∼_ : Rel A 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)

  ∙⁺⇒⁺∙ : ∀ {_∼_ : Rel A a} {n} {xs ys : Vec A n} →
          Reflexive _∼_ →
          Pointwise (Plus _∼_) xs ys → Plus (Pointwise _∼_) xs ys
  ∙⁺⇒⁺∙ {_∼_} x∼x =
    Plus.map (_⟨$⟩_ (Equivalence.from equivalent)) ∘
    helper ∘
    _⟨$⟩_ (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 = Equivalence.to equivalent ⟨$⟩ refl x∼x

open Dummy public

-- 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} {A : Set a} {_R_ _R′_ : Rel A 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 A′ : Set a}
         {_R_ : Rel A a} {_R′_ : Rel A′ 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))