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

{-# OPTIONS --without-K --safe #-}

module Data.List.Relation.Binary.Pointwise where

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) 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)
open import Relation.Nullary.Negation using (contradiction)
import Relation.Nullary.Decidable as Dec using (map′)
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Unary as U using (Pred)
open import Relation.Binary renaming (Rel to Rel₂)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

private
  variable
    a b c d p q r  ℓ₁ ℓ₂ ℓ₃ : Level
    A : Set a
    B : Set b
    C : Set c
    D : Set d

------------------------------------------------------------------------
-- Definition

infixr 5 _∷_

data Pointwise {A : Set a} {B : Set b} (_∼_ : REL A B )
               : List A  List B  Set (a  b  ) where
  []  : Pointwise _∼_ [] []
  _∷_ :  {x xs y ys} (x∼y : x  y) (xs∼ys : Pointwise _∼_ xs ys) 
        Pointwise _∼_ (x  xs) (y  ys)

------------------------------------------------------------------------
-- Operations

module _ {_∼_ : REL A B } where

  head :  {x y xs ys}  Pointwise _∼_ (x  xs) (y  ys)  x  y
  head (x∼y  xs∼ys) = x∼y

  tail :  {x y xs ys}  Pointwise _∼_ (x  xs) (y  ys) 
         Pointwise _∼_ xs ys
  tail (x∼y  xs∼ys) = xs∼ys

  uncons :  {x y xs ys}  Pointwise _∼_ (x  xs) (y  ys) 
           x  y × Pointwise _∼_ xs ys
  uncons = < head , tail >

  rec :  (P :  {xs ys}  Pointwise _∼_ xs ys  Set c) 
        (∀ {x y xs ys} {xs∼ys : Pointwise _∼_ xs ys} 
          (x∼y : x  y)  P xs∼ys  P (x∼y  xs∼ys)) 
        P [] 
         {xs ys} (xs∼ys : Pointwise _∼_ xs ys)  P xs∼ys
  rec P c n []            = n
  rec P c n (x∼y  xs∼ys) = c x∼y (rec P c n xs∼ys)

  map :  {_≈_ : REL A B ℓ₂}  _≈_  _∼_  Pointwise _≈_  Pointwise _∼_
  map ≈⇒∼ []            = []
  map ≈⇒∼ (x≈y  xs≈ys) = ≈⇒∼ x≈y  map ≈⇒∼ xs≈ys

------------------------------------------------------------------------
-- Relational properties

reflexive :  {_≈_ : REL A B ℓ₁} {_∼_ : REL A B ℓ₂} 
            _≈_  _∼_  Pointwise _≈_  Pointwise _∼_
reflexive ≈⇒∼ []            = []
reflexive ≈⇒∼ (x≈y  xs≈ys) = ≈⇒∼ x≈y  reflexive ≈⇒∼ xs≈ys

refl :  {_∼_ : Rel₂ A }  Reflexive _∼_  Reflexive (Pointwise _∼_)
refl rfl {[]}     = []
refl rfl {x  xs} = rfl  refl rfl

symmetric :  {_≈_ : REL A B ℓ₁} {_∼_ : REL B A ℓ₂} 
            Sym _≈_ _∼_  Sym (Pointwise _≈_) (Pointwise _∼_)
symmetric sym []            = []
symmetric sym (x∼y  xs∼ys) = sym x∼y  symmetric sym xs∼ys

transitive :  {_≋_ : REL A B ℓ₁} {_≈_ : REL B C ℓ₂} {_∼_ : REL A C ℓ₃} 
             Trans _≋_ _≈_ _∼_ 
             Trans (Pointwise _≋_) (Pointwise _≈_) (Pointwise _∼_)
transitive trans []            []            = []
transitive trans (x∼y  xs∼ys) (y∼z  ys∼zs) =
  trans x∼y y∼z  transitive trans xs∼ys ys∼zs

antisymmetric :  {_≤_ : REL A B ℓ₁} {_≤′_ : REL B A ℓ₂} {_≈_ : REL A B ℓ₃} 
                Antisym _≤_ _≤′_ _≈_ 
                Antisym (Pointwise _≤_) (Pointwise _≤′_) (Pointwise _≈_)
antisymmetric antisym []            []            = []
antisymmetric antisym (x∼y  xs∼ys) (y∼x  ys∼xs) =
  antisym x∼y y∼x  antisymmetric antisym xs∼ys ys∼xs

respects₂ :  {_≈_ : Rel₂ A ℓ₁} {_∼_ : Rel₂ A ℓ₂} 
            _∼_ Respects₂ _≈_  (Pointwise _∼_) Respects₂ (Pointwise _≈_)
respects₂ {_≈_ = _≈_} {_∼_} resp = respʳ , respˡ
  where
  respʳ : (Pointwise _∼_) Respectsʳ (Pointwise _≈_)
  respʳ []            []            = []
  respʳ (x≈y  xs≈ys) (z∼x  zs∼xs) =
    proj₁ resp x≈y z∼x  respʳ xs≈ys zs∼xs

  respˡ : (Pointwise _∼_) Respectsˡ (Pointwise _≈_)
  respˡ []            []            = []
  respˡ (x≈y  xs≈ys) (x∼z  xs∼zs) =
    proj₂ resp x≈y x∼z  respˡ xs≈ys xs∼zs

module _ {_∼_ : REL A B } (dec : Decidable _∼_) where

  decidable : Decidable (Pointwise _∼_)
  decidable []       []       = yes []
  decidable []       (y  ys) = no  ())
  decidable (x  xs) []       = no  ())
  decidable (x  xs) (y  ys) =
    Dec.map′ (uncurry _∷_) uncons (dec x y ×-dec decidable xs ys)

module _ {_≈_ : Rel₂ A } where

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

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

module _ {_≈_ : Rel₂ A ℓ₁} {_∼_ : Rel₂ A ℓ₂} where

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

  isPartialOrder : IsPartialOrder _≈_ _∼_ 
                   IsPartialOrder (Pointwise _≈_) (Pointwise _∼_)
  isPartialOrder po = record
    { isPreorder = isPreorder    PO.isPreorder
    ; antisym    = antisymmetric PO.antisym
    } where module PO = IsPartialOrder po

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 predicates

module _ {_∼_ : Rel₂ A } {P : Pred A p} where

  All-resp-Pointwise : P Respects _∼_  (All P) Respects (Pointwise _∼_)
  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 Respects _∼_  (Any P) Respects (Pointwise _∼_)
  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)

module _ {_∼_ : Rel₂ A } {R : Rel₂ A r} where

  AllPairs-resp-Pointwise : R Respects₂ _∼_  (AllPairs R) Respects (Pointwise _∼_)
  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)

------------------------------------------------------------------------
-- length

module _ {_∼_ : REL A B } where

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

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

module _ {_∼_ : REL A B } where

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

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

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

module _ {_∼_ : REL A B } where

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

module _ {_∼_ : Rel₂ A } where

  ++-cancelˡ :  xs {ys zs : List A}  Pointwise _∼_ (xs ++ ys) (xs ++ zs)  Pointwise _∼_ ys zs
  ++-cancelˡ []       ys∼zs               = ys∼zs
  ++-cancelˡ (x  xs) (_  xs++ys∼xs++zs) = ++-cancelˡ xs xs++ys∼xs++zs

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

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

module _ {_∼_ : REL A B } where

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

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

module _ {R : REL A B } where

  reverseAcc⁺ :  {as bs as′ bs′}  Pointwise R as′ bs′  Pointwise R as bs 
                Pointwise R (reverseAcc as′ as) (reverseAcc bs′ bs)
  reverseAcc⁺ rs′ []       = rs′
  reverseAcc⁺ rs′ (r  rs) = reverseAcc⁺ (r  rs′) rs

  ʳ++⁺ :  {as bs as′ bs′} 
           Pointwise R as bs 
           Pointwise R as′ bs′ 
           Pointwise R (as ʳ++ as′) (bs ʳ++ bs′)
  ʳ++⁺ rs rs′ = reverseAcc⁺ rs′ rs

  reverse⁺ :  {as bs}  Pointwise R as bs  Pointwise R (reverse as) (reverse bs)
  reverse⁺ = reverseAcc⁺ []

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

module _ {R : REL C D } where

  map⁺ :  {as bs} (f : A  C) (g : B  D) 
         Pointwise  a b  R (f a) (g b)) as bs 
         Pointwise R (List.map f as) (List.map g bs)
  map⁺ f g []       = []
  map⁺ f g (r  rs) = r  map⁺ f g rs

  map⁻ :  {as bs} (f : A  C) (g : B  D) 
         Pointwise R (List.map f as) (List.map g bs) 
         Pointwise  a b  R (f a) (g b)) as bs
  map⁻ {as = []}     {[]}     f g [] = []
  map⁻ {as = []}     {b  bs} f g rs = contradiction (Pointwise-length rs) λ()
  map⁻ {as = a  as} {[]}     f g rs = contradiction (Pointwise-length rs) λ()
  map⁻ {as = a  as} {b  bs} f g (r  rs) = r  map⁻ f g rs

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

module _ {R : REL A B } {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⁺ :  {as bs}  Pointwise R as bs  Pointwise R (filter P? as) (filter Q? bs)
  filter⁺ []       = []
  filter⁺ {a  _} {b  _} (r  rs) with P? a | Q? b
  ... | 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

module _ {R : REL A B } where

  replicate⁺ :  {a b}  R a b   n  Pointwise R (replicate n a) (replicate n b)
  replicate⁺ r 0       = []
  replicate⁺ r (suc n) = r  replicate⁺ r n

------------------------------------------------------------------------
-- Irrelevance

module _ {R : REL A B } where

  irrelevant : Irrelevant R  Irrelevant (Pointwise R)
  irrelevant R-irr [] [] = P.refl
  irrelevant R-irr (r  rs) (r₁  rs₁) =
    P.cong₂ _∷_ (R-irr r r₁) (irrelevant R-irr rs rs₁)

------------------------------------------------------------------------
-- 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
    }
  }

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.15

Rel    = Pointwise
{-# WARNING_ON_USAGE Rel
"Warning: Rel was deprecated in v0.15.
Please use Pointwise instead."
#-}
Rel≡⇒≡ = Pointwise-≡⇒≡
{-# WARNING_ON_USAGE Rel≡⇒≡
"Warning: Rel≡⇒≡ was deprecated in v0.15.
Please use Pointwise-≡⇒≡ instead."
#-}
≡⇒Rel≡ = ≡⇒Pointwise-≡
{-# WARNING_ON_USAGE ≡⇒Rel≡
"Warning: ≡⇒Rel≡ was deprecated in v0.15.
Please use ≡⇒Pointwise-≡ instead."
#-}
Rel↔≡  = Pointwise-≡↔≡
{-# WARNING_ON_USAGE Rel↔≡
"Warning: Rel↔≡ was deprecated in v0.15.
Please use Pointwise-≡↔≡ instead."
#-}

-- Version 1.0

decidable-≡ = ≡-dec
{-# WARNING_ON_USAGE decidable-≡
"Warning: decidable-≡ was deprecated in v1.0.
Please use ≡-dec from `Data.List.Properties` instead."
#-}