------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of pointwise lifting of relations to lists
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Pointwise.Properties where

open import Data.Product.Base using (_,_; uncurry)
open import Data.List.Base using (List; []; _∷_)
open import Level
open import Relation.Binary.Core using (REL; _⇒_)
open import Relation.Binary.Definitions
import Relation.Binary.PropositionalEquality.Core as P
open import Relation.Nullary using (yes; no; _×-dec_)
import Relation.Nullary.Decidable as Dec

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

private
  variable
    a b  : Level
    A : Set a
    B : Set b
    R S T : REL A B 

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

reflexive : R  S  Pointwise R  Pointwise S
reflexive = map

refl : Reflexive R  Reflexive (Pointwise R)
refl rfl {[]}     = []
refl rfl {x  xs} = rfl  refl rfl

symmetric : Sym R S  Sym (Pointwise R) (Pointwise S)
symmetric sym []            = []
symmetric sym (x∼y  xs∼ys) = sym x∼y  symmetric sym xs∼ys

transitive : Trans R S T 
             Trans (Pointwise R) (Pointwise S) (Pointwise T)
transitive trans []            []            = []
transitive trans (x∼y  xs∼ys) (y∼z  ys∼zs) =
  trans x∼y y∼z  transitive trans xs∼ys ys∼zs

antisymmetric : Antisym R S T 
                Antisym (Pointwise R) (Pointwise S) (Pointwise T)
antisymmetric antisym []            []            = []
antisymmetric antisym (x∼y  xs∼ys) (y∼x  ys∼xs) =
  antisym x∼y y∼x  antisymmetric antisym xs∼ys ys∼xs

respʳ : R Respectsʳ S  (Pointwise R) Respectsʳ (Pointwise S)
respʳ resp []            []            = []
respʳ resp (x≈y  xs≈ys) (z∼x  zs∼xs) = resp x≈y z∼x  respʳ resp xs≈ys zs∼xs

respˡ : R Respectsˡ S  (Pointwise R) Respectsˡ (Pointwise S)
respˡ resp []            []            = []
respˡ resp (x≈y  xs≈ys) (x∼z  xs∼zs) = resp x≈y x∼z  respˡ resp xs≈ys xs∼zs

respects₂ : R Respects₂ S  (Pointwise R) Respects₂ (Pointwise S)
respects₂ ( , ) = respʳ  , respˡ 

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

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