Add various relations over non-empty lists (#2862)

* Add various relations over non-empty lists

* Address James' feedback

Author: MatthewDaggitt

CHANGELOG.md

@@ -93,6 +93,14 @@ New modules
 
 * `Effect.Monad.Random` and `Effect.Monad.Random.Instances` for an mtl-style randomness monad constraint.
 
+* Various additions over non-empty lists:
+  ```
+  Data.List.NonEmpty.Relation.Binary.Pointwise
+  Data.List.NonEmpty.Relation.Unary.Any
+  Data.List.NonEmpty.Membership.Propositional
+  Data.List.NonEmpty.Membership.Setoid
+  ```
+
 Additions to existing modules
 -----------------------------
 
@@ -159,6 +167,11 @@ Additions to existing modules
   search-least⟨¬_⟩ : Decidable P → Π[ P ] ⊎ Least⟨ ∁ P ⟩
   ```
 
+* In `Data.List.NonEmpty.Relation.Unary.All`:
+  ```
+  map : P ⊆ Q → All P xs → All Q xs
+  ```
+
 * In `Data.Nat.ListAction.Properties`
   ```agda
   *-distribˡ-sum : ∀ m ns → m * sum ns ≡ sum (map (m *_) ns)

src/Data/List/NonEmpty/Membership/Propositional.agda

@@ -0,0 +1,27 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Propositional membership over non-empty lists
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.NonEmpty.Membership.Propositional {a} {A : Set a} where
+
+open import Relation.Binary.PropositionalEquality using (setoid; refl)
+open import Data.List.NonEmpty
+open import Level
+open import Relation.Unary using (Pred)
+
+import Data.List.NonEmpty.Membership.Setoid as SetoidMembership
+
+private
+  variable
+    p : Level
+    P : Pred A p
+    xs : List⁺ A
+
+------------------------------------------------------------------------
+-- Re-export contents of setoid membership
+
+open SetoidMembership (setoid A) public

src/Data/List/NonEmpty/Membership/Setoid.agda

@@ -0,0 +1,28 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Setoid membership over non-empty lists
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Bundles using (Setoid)
+
+module Data.List.NonEmpty.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where
+
+open import Data.List.NonEmpty.Base using (List⁺)
+open import Data.List.NonEmpty.Relation.Unary.Any using (Any)
+open import Relation.Nullary.Negation using (¬_)
+
+open Setoid S renaming (Carrier to A)
+
+------------------------------------------------------------------------
+-- Definitions
+
+infix 4 _∈_ _∉_
+
+_∈_ : A → List⁺ A → Set _
+x ∈ xs = Any (x ≈_) xs
+
+_∉_ : A → List⁺ A → Set _
+x ∉ xs = ¬ x ∈ xs

src/Data/List/NonEmpty/Relation/Binary/Pointwise.agda

@@ -0,0 +1,33 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Pointwise lifting of relations to non-empty lists
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.NonEmpty.Relation.Binary.Pointwise where
+
+open import Data.List.Base using (List; []; _∷_)
+open import Data.List.NonEmpty.Base using (List⁺; _∷_)
+import Data.List.Relation.Binary.Pointwise.Base as List
+open import Level
+open import Relation.Binary.Core using (REL)
+
+private
+  variable
+    a b ℓ : Level
+    A B : Set a
+    x y : A
+    xs ys : List A
+
+------------------------------------------------------------------------
+-- Definition
+------------------------------------------------------------------------
+
+infixr 5 _∷_
+
+data Pointwise {A : Set a} {B : Set b} (R : REL A B ℓ)
+               : List⁺ A → List⁺ B → Set (a ⊔ b ⊔ ℓ) where
+  _∷_ : (x∼y : R x y) (xs∼ys : List.Pointwise R xs ys) →
+         Pointwise R (x ∷ xs) (y ∷ ys)

src/Data/List/NonEmpty/Relation/Unary/All.agda

@@ -12,14 +12,18 @@ import Data.List.Relation.Unary.All as List
 open import Data.List.Relation.Unary.All using ([]; _∷_)
 open import Data.List.Base using ([]; _∷_)
 open import Data.List.NonEmpty.Base using (List⁺; _∷_; toList)
+open import Data.List.NonEmpty.Membership.Propositional using (_∈_)
+open import Data.List.NonEmpty.Relation.Unary.Any using (here; there)
 open import Level using (Level; _⊔_)
-open import Relation.Unary using (Pred)
+open import Relation.Unary using (Pred; _⊆_)
+open import Relation.Binary.PropositionalEquality.Core using (refl)
 
 private
   variable
     a p : Level
     A : Set a
-    P : Pred A p
+    P Q : Pred A p
+    xs : List⁺ A
 
 ------------------------------------------------------------------------
 -- Definition
@@ -35,5 +39,12 @@ data All {A : Set a} (P : Pred A p) : Pred (List⁺ A) (a ⊔ p) where
 ------------------------------------------------------------------------
 -- Functions
 
+map : P ⊆ Q → All P ⊆ All Q
+map P⊆Q (px ∷ pxs) = P⊆Q px ∷ List.map P⊆Q pxs
+
+lookup : All P xs → ∀ {x} → x ∈ xs → P x
+lookup (px ∷ pxs) (here refl)   = px
+lookup (px ∷ pxs) (there x∈xs) = List.lookup pxs x∈xs
+
 toList⁺ : ∀ {xs : List⁺ A} → All P xs → List.All P (toList xs)
 toList⁺ (px ∷ pxs) = px ∷ pxs

src/Data/List/NonEmpty/Relation/Unary/Any.agda

@@ -0,0 +1,47 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Non-empty lists where at least one element satisfies a given property
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.NonEmpty.Relation.Unary.Any where
+
+open import Data.List.NonEmpty.Base using (List⁺; _∷_; toList)
+open import Data.List.Relation.Unary.Any as List using (here; there)
+open import Data.List.Base using ([]; _∷_)
+open import Data.Product.Base using (_,_)
+open import Level using (Level; _⊔_)
+open import Relation.Unary using (Pred; Satisfiable; _⊆_)
+
+private
+  variable
+    a p : Level
+    A : Set a
+    P Q : Pred A p
+    xs : List⁺ A
+
+------------------------------------------------------------------------
+-- Definition
+
+-- Given a predicate P, then Any P xs means that every element in xs
+-- satisfies P. See `Relation.Unary` for an explanation of predicates.
+
+data Any {A : Set a} (P : Pred A p) : Pred (List⁺ A) (a ⊔ p) where
+  here : ∀ {x xs} (px : P x) → Any P (x ∷ xs)
+  there : ∀ {x xs} (pxs : List.Any P xs) → Any P (x ∷ xs)
+
+------------------------------------------------------------------------
+-- Operations
+
+map : P ⊆ Q → Any P ⊆ Any Q
+map g (here px)   = here (g px)
+map g (there pxs) = there (List.map g pxs)
+
+------------------------------------------------------------------------
+-- Predicates
+
+satisfied : Any P xs → Satisfiable P
+satisfied (here px)  = _ , px
+satisfied (there pxs) = List.satisfied pxs

src/Data/List/Relation/Unary/Any.agda

@@ -71,7 +71,7 @@ xs ─ x∈xs = removeAt xs (index x∈xs)
 
 -- If any element satisfies P, then P is satisfied.
 
-satisfied : Any P xs → ∃ P
+satisfied : Any P xs → Satisfiable P
 satisfied (here px)   = _ , px
 satisfied (there pxs) = satisfied pxs