------------------------------------------------------------------------
-- 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.Nat.Base using (ℕ)
open import Data.Fin.Base using (zero; suc; cast)
open import Data.Product.Base using (_,_; uncurry)
open import Data.List.Base using (List; []; _∷_; length; lookup)
open import Level
open import Relation.Binary.Core using (REL; _⇒_)
open import Relation.Binary.Definitions
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
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₂ (rʳ , rˡ) = respʳ rʳ , respˡ rˡ
 
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 []       []         = ≡.refl
irrelevant irr (r ∷ rs) (r₁ ∷ rs₁) =
  ≡.cong₂ _∷_ (irr r r₁) (irrelevant irr rs rs₁)
 
Pointwise-length : ∀ {xs ys} → Pointwise R xs ys → length xs ≡ length ys
Pointwise-length []            = ≡.refl
Pointwise-length (x∼y ∷ xs∼ys) = ≡.cong ℕ.suc (Pointwise-length xs∼ys)
 
lookup-cast : ∀ {xs ys} →
              Pointwise R xs ys →
              .(∣xs∣≡∣ys∣ : length xs ≡ length ys) →
              ∀ i →
              R (lookup xs i) (lookup ys (cast ∣xs∣≡∣ys∣ i))
lookup-cast (Rxy ∷ Rxsys) _ zero = Rxy
lookup-cast (Rxy ∷ Rxsys) _ (suc i) = lookup-cast Rxsys _ i