Added pointwise and catmaybe in Lists

CHANGELOG.md

@@ -3909,3 +3909,19 @@ This is a full list of proofs that have changed form to use irrelevant instance
   1/pos⇒pos : ∀ p .{{_ : NonZero p}} → (1/p : Positive (1/ p)) → Positive p
   1/neg⇒neg : ∀ p .{{_ : NonZero p}} → (1/p : Negative (1/ p)) → Negative p
   ```
+
+* In `Data.Maybe.Relation.Binary.Pointwise`:
+```agda
+  pointwise⊆any : Pointwise R (just x) ⊆ Any (R x)
+```
+
+* In `Data.List.Relation.Unary.All.Properties`:
+```
+  catMaybesAll⁺ : All (Maybe.All P) xs → All P (catMaybes xs)
+  catMaybesAny⁺ : All (Maybe.Any P) xs → All P (catMaybes xs)
+```
+
+* In `Data.List.Relation.Unary.AllPairs.Properties`:
+```
+  pointwise⁺ : AllPairs (Pointwise R) xs → AllPairs R (catMaybes xs)
+```

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

@@ -29,6 +29,7 @@ open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_
 open import Data.List.Relation.Binary.Subset.Propositional using (_⊆_)
 open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
 open import Data.Maybe.Relation.Unary.All as Maybe using (just; nothing)
+open import Data.Maybe.Relation.Unary.Any as Maybe using (just)
 open import Data.Nat.Base using (zero; suc; s≤s; _<_; z<s; s<s)
 open import Data.Nat.Properties using (≤-refl; m≤n⇒m≤1+n)
 open import Data.Product.Base as Prod using (_×_; _,_; uncurry; uncurry′)
@@ -388,6 +389,18 @@ mapMaybe⁺ {xs = x ∷ xs} {f = f} (px ∷ pxs) with f x
 ... | just v with px
 ...   | just pv = pv ∷ mapMaybe⁺ pxs
 
+------------------------------------------------------------------------
+-- catMaybes
+
+catMaybesAll⁺ : All (Maybe.All P) xs → All P (catMaybes xs)
+catMaybesAll⁺ [] = []
+catMaybesAll⁺ (just px ∷ pxs) = px ∷ catMaybesAll⁺ pxs
+catMaybesAll⁺ (nothing ∷ pxs) = catMaybesAll⁺ pxs
+
+catMaybesAny⁺ : All (Maybe.Any P) xs → All P (catMaybes xs)
+catMaybesAny⁺ [] = []
+catMaybesAny⁺ (just px ∷ pxs) = px ∷ catMaybesAny⁺ pxs
+
 ------------------------------------------------------------------------
 -- _++_
 

src/Data/List/Relation/Unary/AllPairs/Properties.agda

@@ -10,9 +10,11 @@ module Data.List.Relation.Unary.AllPairs.Properties where
 
 open import Data.List.Base hiding (any)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
-import Data.List.Relation.Unary.All.Properties as All
+open import Data.List.Relation.Unary.All.Properties as All using (catMaybesAny⁺)
 open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_)
 open import Data.Bool.Base using (true; false)
+open import Data.Maybe using (Maybe; nothing; just)
+open import Data.Maybe.Relation.Binary.Pointwise using (pointwise⊆any; Pointwise)
 open import Data.Fin.Base using (Fin)
 open import Data.Fin.Properties using (suc-injective)
 open import Data.Nat.Base using (zero; suc; _<_; z≤n; s≤s)
@@ -22,7 +24,7 @@ open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (DecSetoid)
 open import Relation.Binary.PropositionalEquality.Core using (_≢_)
-open import Relation.Unary using (Pred; Decidable)
+open import Relation.Unary using (Pred; Decidable; _⊆_)
 open import Relation.Nullary.Decidable using (does)
 
 private
@@ -132,3 +134,13 @@ module _ {R : Rel A ℓ} {P : Pred A p} (P? : Decidable P) where
   filter⁺ {x ∷ xs} (x∉xs ∷ xs!) with does (P? x)
   ... | false = filter⁺ xs!
   ... | true  = All.filter⁺ P? x∉xs ∷ filter⁺ xs!
+
+------------------------------------------------------------------------
+-- pointwise
+
+module _ {R : Rel A ℓ}  where
+
+  pointwise⁺ : {xs : List (Maybe A)} → AllPairs (Pointwise R) xs → AllPairs R (catMaybes xs)
+  pointwise⁺ {xs = []} [] = []
+  pointwise⁺ {xs = nothing ∷  _} (x∼xs ∷ pxs) = pointwise⁺ pxs
+  pointwise⁺ {xs = just x  ∷ xs} (x∼xs ∷ pxs) = catMaybesAny⁺ (All.map pointwise⊆any x∼xs) ∷ pointwise⁺ pxs

src/Data/Maybe/Relation/Binary/Pointwise.agda

@@ -11,13 +11,15 @@ module Data.Maybe.Relation.Binary.Pointwise where
 open import Level
 open import Data.Product.Base using (∃; _×_; -,_; _,_)
 open import Data.Maybe.Base using (Maybe; just; nothing)
+open import Data.Maybe.Relation.Unary.Any using (Any; just)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Relation.Binary.Core using (REL; Rel; _⇒_)
 open import Relation.Binary.Bundles using (Setoid; DecSetoid)
 open import Relation.Binary.Definitions using (Reflexive; Sym; Trans; Decidable)
 open import Relation.Binary.Structures using (IsEquivalence; IsDecEquivalence)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Nullary
+open import Relation.Unary using (_⊆_)
 import Relation.Nullary.Decidable as Dec
 
 ------------------------------------------------------------------------
@@ -93,6 +95,9 @@ module _ {a r} {A : Set a} {R : Rel A r} where
     ; _≟_           = dec R._≟_
     } where module R = IsDecEquivalence R-isDecEquivalence
 
+  pointwise⊆any : ∀ {x} → Pointwise R (just x) ⊆ Any (R x)
+  pointwise⊆any (just Rxy) = just Rxy
+
 module _ {c ℓ} where
 
   setoid : Setoid c ℓ → Setoid c (c ⊔ ℓ)