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

{-# OPTIONS --cubical-compatible --safe #-}

module Data.List.Relation.Binary.Pointwise where

open import Algebra.Core using (Op₂)
open import Function.Base
open import Function.Inverse using (Inverse)
open import Data.Bool.Base using (true; false)
open import Data.Product hiding (map)
open import Data.List.Base as List hiding (map; head; tail; uncons)
open import Data.List.Properties using (≡-dec; length-++)
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_)
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.Fin.Base using (Fin; toℕ; cast) renaming (zero to fzero; suc to fsuc)
open import Data.Nat.Base using (; zero; suc)
open import Data.Nat.Properties
open import Level
open import Relation.Nullary hiding (Irrelevant)
import Relation.Nullary.Decidable as Dec using (map′)
open import Relation.Unary as U using (Pred)
open import Relation.Binary renaming (Rel to Rel₂)
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
import Relation.Binary.PropositionalEquality.Properties as P

private
  variable
    a b c d p q  ℓ₁ ℓ₂ : Level
    A B C D : Set d
    x y z : A
    ws xs ys zs : List A
    R S T : REL A B 

------------------------------------------------------------------------
-- Re-exporting the definition and basic operations
------------------------------------------------------------------------

open import Data.List.Relation.Binary.Pointwise.Base public
open import Data.List.Relation.Binary.Pointwise.Properties public

------------------------------------------------------------------------
-- Structures

isEquivalence : IsEquivalence R  IsEquivalence (Pointwise R)
isEquivalence eq = record
  { refl  = refl       Eq.refl
  ; sym   = symmetric  Eq.sym
  ; trans = transitive Eq.trans
  } where module Eq = IsEquivalence eq

isDecEquivalence : IsDecEquivalence R  IsDecEquivalence (Pointwise R)
isDecEquivalence eq = record
  { isEquivalence = isEquivalence DE.isEquivalence
  ; _≟_           = decidable     DE._≟_
  } where module DE = IsDecEquivalence eq

isPreorder : IsPreorder R S  IsPreorder (Pointwise R) (Pointwise S)
isPreorder pre = record
  { isEquivalence = isEquivalence Pre.isEquivalence
  ; reflexive     = reflexive     Pre.reflexive
  ; trans         = transitive    Pre.trans
  } where module Pre = IsPreorder pre

isPartialOrder : IsPartialOrder R S 
                 IsPartialOrder (Pointwise R) (Pointwise S)
isPartialOrder po = record
  { isPreorder = isPreorder    PO.isPreorder
  ; antisym    = antisymmetric PO.antisym
  } where module PO = IsPartialOrder po

------------------------------------------------------------------------
-- Bundles

setoid : Setoid a   Setoid a (a  )
setoid s = record
  { isEquivalence = isEquivalence (Setoid.isEquivalence s)
  }

decSetoid : DecSetoid a   DecSetoid a (a  )
decSetoid d = record
  { isDecEquivalence = isDecEquivalence (DecSetoid.isDecEquivalence d)
  }

preorder : Preorder a ℓ₁ ℓ₂  Preorder _ _ _
preorder p = record
  { isPreorder = isPreorder (Preorder.isPreorder p)
  }

poset : Poset a ℓ₁ ℓ₂  Poset _ _ _
poset p = record
  { isPartialOrder = isPartialOrder (Poset.isPartialOrder p)
  }

------------------------------------------------------------------------
-- Relationships to other list predicates
------------------------------------------------------------------------

All-resp-Pointwise :  {P : Pred A p}  P Respects R 
                     (All P) Respects (Pointwise R)
All-resp-Pointwise resp []         []         = []
All-resp-Pointwise resp (x∼y  xs) (px  pxs) =
  resp x∼y px  All-resp-Pointwise resp xs pxs

Any-resp-Pointwise :  {P : Pred A p}  P Respects R 
                     (Any P) Respects (Pointwise R)
Any-resp-Pointwise resp (x∼y  xs) (here px)   = here (resp x∼y px)
Any-resp-Pointwise resp (x∼y  xs) (there pxs) =
  there (Any-resp-Pointwise resp xs pxs)

AllPairs-resp-Pointwise : R Respects₂ S 
                          (AllPairs R) Respects (Pointwise S)
AllPairs-resp-Pointwise _                    []         []         = []
AllPairs-resp-Pointwise resp@(respₗ , respᵣ) (x∼y  xs) (px  pxs) =
  All-resp-Pointwise respₗ xs (All.map (respᵣ x∼y) px) 
  (AllPairs-resp-Pointwise resp xs pxs)

------------------------------------------------------------------------
-- Relationship to functions over lists
------------------------------------------------------------------------
-- length

Pointwise-length : Pointwise R xs ys  length xs  length ys
Pointwise-length []            = P.refl
Pointwise-length (x∼y  xs∼ys) = P.cong ℕ.suc (Pointwise-length xs∼ys)

------------------------------------------------------------------------
-- tabulate

tabulate⁺ :  {n} {f : Fin n  A} {g : Fin n  B} 
            (∀ i  R (f i) (g i))  Pointwise R (tabulate f) (tabulate g)
tabulate⁺ {n = zero}  f∼g = []
tabulate⁺ {n = suc n} f∼g = f∼g fzero  tabulate⁺ (f∼g  fsuc)

tabulate⁻ :  {n} {f : Fin n  A} {g : Fin n  B} 
            Pointwise R (tabulate f) (tabulate g)  (∀ i  R (f i) (g i))
tabulate⁻ {n = suc n} (x∼y  xs∼ys) fzero    = x∼y
tabulate⁻ {n = suc n} (x∼y  xs∼ys) (fsuc i) = tabulate⁻ xs∼ys i

------------------------------------------------------------------------
-- _++_

++⁺ : Pointwise R ws xs  Pointwise R ys zs 
      Pointwise R (ws ++ ys) (xs ++ zs)
++⁺ []            ys∼zs = ys∼zs
++⁺ (w∼x  ws∼xs) ys∼zs = w∼x  ++⁺ ws∼xs ys∼zs

++-cancelˡ :  xs  Pointwise R (xs ++ ys) (xs ++ zs)  Pointwise R ys zs
++-cancelˡ []       ys∼zs               = ys∼zs
++-cancelˡ (x  xs) (_  xs++ys∼xs++zs) = ++-cancelˡ xs xs++ys∼xs++zs

++-cancelʳ :  ys zs  Pointwise R (ys ++ xs) (zs ++ xs)  Pointwise R ys zs
++-cancelʳ []       []       _             = []
++-cancelʳ (y  ys) (z  zs) (y∼z  ys∼zs) = y∼z  (++-cancelʳ ys zs ys∼zs)
-- Impossible cases
++-cancelʳ {xs = xs}     []       (z  zs) eq   =
  contradiction (P.trans (Pointwise-length eq) (length-++ (z  zs))) (m≢1+n+m (length xs))
++-cancelʳ {xs = xs}     (y  ys) []       eq   =
  contradiction (P.trans (P.sym (length-++ (y  ys))) (Pointwise-length eq)) (m≢1+n+m (length xs)  P.sym)

------------------------------------------------------------------------
-- concat

concat⁺ :  {xss yss}  Pointwise (Pointwise R) xss yss 
          Pointwise R (concat xss) (concat yss)
concat⁺ []                = []
concat⁺ (xs∼ys  xss∼yss) = ++⁺ xs∼ys (concat⁺ xss∼yss)

------------------------------------------------------------------------
-- reverse

reverseAcc⁺ : Pointwise R ws xs  Pointwise R ys zs 
              Pointwise R (reverseAcc ws ys) (reverseAcc xs zs)
reverseAcc⁺ rs′ []       = rs′
reverseAcc⁺ rs′ (r  rs) = reverseAcc⁺ (r  rs′) rs

ʳ++⁺ : Pointwise R ws xs  Pointwise R ys zs 
       Pointwise R (ws ʳ++ ys) (xs ʳ++ zs)
ʳ++⁺ rs rs′ = reverseAcc⁺ rs′ rs

reverse⁺ : Pointwise R xs ys  Pointwise R (reverse xs) (reverse ys)
reverse⁺ = reverseAcc⁺ []

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

map⁺ :  (f : A  C) (g : B  D) 
       Pointwise  a b  R (f a) (g b)) xs ys 
       Pointwise R (List.map f xs) (List.map g ys)
map⁺ f g []       = []
map⁺ f g (r  rs) = r  map⁺ f g rs

map⁻ :  (f : A  C) (g : B  D) 
       Pointwise R (List.map f xs) (List.map g ys) 
       Pointwise  a b  R (f a) (g b)) xs ys
map⁻ {xs = []}    {[]}    f g [] = []
map⁻ {xs = _  _} {_  _} f g (r  rs) = r  map⁻ f g rs

------------------------------------------------------------------------
-- foldr

foldr⁺ :  {_•_ : Op₂ A} {_◦_ : Op₂ B} 
         (∀ {w x y z}  R w x  R y z  R (w  y) (x  z)) 
          {e f}  R e f  Pointwise R xs ys 
         R (foldr _•_ e xs) (foldr _◦_ f ys)
foldr⁺ _    e~f []            = e~f
foldr⁺ pres e~f (x~y  xs~ys) = pres x~y (foldr⁺ pres e~f xs~ys)

------------------------------------------------------------------------
-- filter

module _ {P : Pred A p} {Q : Pred B q}
         (P? : U.Decidable P) (Q? : U.Decidable Q)
         (P⇒Q :  {a b}  R a b  P a  Q b)
         (Q⇒P :  {a b}  R a b  Q b  P a)
         where

  filter⁺ : Pointwise R xs ys 
            Pointwise R (filter P? xs) (filter Q? ys)
  filter⁺ []       = []
  filter⁺ {x  _} {y  _} (r  rs) with P? x | Q? y
  ... | true  because _ | true  because _ = r  filter⁺ rs
  ... | false because _ | false because _ = filter⁺ rs
  ... | yes p           | no ¬q = contradiction (P⇒Q r p) ¬q
  ... | no ¬p           | yes q = contradiction (Q⇒P r q) ¬p

------------------------------------------------------------------------
-- replicate

replicate⁺ : R x y   n  Pointwise R (replicate n x) (replicate n y)
replicate⁺ r 0       = []
replicate⁺ r (suc n) = r  replicate⁺ r n

------------------------------------------------------------------------
-- lookup

lookup⁻ : length xs  length ys 
          (∀ {i j}  toℕ i  toℕ j  R (lookup xs i) (lookup ys j)) 
          Pointwise R xs ys
lookup⁻ {xs = []}    {ys = []}    _             _  = []
lookup⁻ {xs = _  _} {ys = _  _} |xs|≡|ys| eq = eq {fzero} P.refl 
  lookup⁻ (suc-injective |xs|≡|ys|) (eq  P.cong ℕ.suc)

lookup⁺ :  (Rxys : Pointwise R xs ys) 
           i  (let j = cast (Pointwise-length Rxys) i) 
          R (lookup xs i) (lookup ys j)
lookup⁺ (Rxy  _)    fzero    = Rxy
lookup⁺ (_    Rxys) (fsuc i) = lookup⁺ Rxys i

------------------------------------------------------------------------
-- Properties of propositional pointwise
------------------------------------------------------------------------

Pointwise-≡⇒≡ : Pointwise {A = A} _≡_  _≡_
Pointwise-≡⇒≡ []               = P.refl
Pointwise-≡⇒≡ (P.refl  xs∼ys) with Pointwise-≡⇒≡ xs∼ys
... | P.refl = P.refl

≡⇒Pointwise-≡ :  _≡_  Pointwise {A = A} _≡_
≡⇒Pointwise-≡ P.refl = refl P.refl

Pointwise-≡↔≡ : Inverse (setoid (P.setoid A)) (P.setoid (List A))
Pointwise-≡↔≡ = record
  { to         = record { _⟨$⟩_ = id; cong = Pointwise-≡⇒≡ }
  ; from       = record { _⟨$⟩_ = id; cong = ≡⇒Pointwise-≡ }
  ; inverse-of = record
    { left-inverse-of  = λ _  refl P.refl
    ; right-inverse-of = λ _  P.refl
    }
  }