------------------------------------------------------------------------ -- 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₂ (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 [] [] = P.refl irrelevant irr (r ∷ rs) (r₁ ∷ rs₁) = P.cong₂ _∷_ (irr r r₁) (irrelevant irr rs rs₁)