------------------------------------------------------------------------ -- The Agda standard library -- -- Lists where every pair of elements are related (symmetrically) ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} open import Relation.Binary.Core using (Rel; _⇒_) module Data.List.Relation.Unary.AllPairs {a ℓ} {A : Set a} {R : Rel A ℓ} where open import Data.List.Base using (List; []; _∷_) open import Data.List.Relation.Unary.All as All using (All; []; _∷_) open import Data.Product.Base as Prod using (_,_; _×_; uncurry; <_,_>) open import Function.Base using (id; _∘_) open import Level using (_⊔_) open import Relation.Binary.Definitions as B open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_) open import Relation.Binary.PropositionalEquality open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_) open import Relation.Nullary.Decidable as Dec using (_×-dec_; yes; no) ------------------------------------------------------------------------ -- Definition open import Data.List.Relation.Unary.AllPairs.Core public ------------------------------------------------------------------------ -- Operations head : ∀ {x xs} → AllPairs R (x ∷ xs) → All (R x) xs head (px ∷ pxs) = px tail : ∀ {x xs} → AllPairs R (x ∷ xs) → AllPairs R xs tail (px ∷ pxs) = pxs uncons : ∀ {x xs} → AllPairs R (x ∷ xs) → All (R x) xs × AllPairs R xs uncons = < head , tail > module _ {q} {S : Rel A q} where map : R ⇒ S → AllPairs R ⊆ AllPairs S map ~₁⇒~₂ [] = [] map ~₁⇒~₂ (x~xs ∷ pxs) = All.map ~₁⇒~₂ x~xs ∷ (map ~₁⇒~₂ pxs) module _ {s t} {S : Rel A s} {T : Rel A t} where zipWith : R ∩ᵇ S ⇒ T → AllPairs R ∩ᵘ AllPairs S ⊆ AllPairs T zipWith f ([] , []) = [] zipWith f (px ∷ pxs , qx ∷ qxs) = All.zipWith f (px , qx) ∷ zipWith f (pxs , qxs) unzipWith : T ⇒ R ∩ᵇ S → AllPairs T ⊆ AllPairs R ∩ᵘ AllPairs S unzipWith f [] = [] , [] unzipWith f (rx ∷ rxs) = Prod.zip _∷_ _∷_ (All.unzipWith f rx) (unzipWith f rxs) module _ {s} {S : Rel A s} where zip : AllPairs R ∩ᵘ AllPairs S ⊆ AllPairs (R ∩ᵇ S) zip = zipWith id unzip : AllPairs (R ∩ᵇ S) ⊆ AllPairs R ∩ᵘ AllPairs S unzip = unzipWith id ------------------------------------------------------------------------ -- Properties of predicates preserved by AllPairs allPairs? : B.Decidable R → U.Decidable (AllPairs R) allPairs? R? [] = yes [] allPairs? R? (x ∷ xs) = Dec.map′ (uncurry _∷_) uncons (All.all? (R? x) xs ×-dec allPairs? R? xs) irrelevant : B.Irrelevant R → U.Irrelevant (AllPairs R) irrelevant irr [] [] = refl irrelevant irr (px₁ ∷ pxs₁) (px₂ ∷ pxs₂) = cong₂ _∷_ (All.irrelevant irr px₁ px₂) (irrelevant irr pxs₁ pxs₂) satisfiable : U.Satisfiable (AllPairs R) satisfiable = [] , []