Added pointwise and catmaybe in Lists

CHANGELOG.md

@@ -3909,3 +3909,13 @@ 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.List.Relation.Unary.All.Properties`:
+```
+  catMaybes⁺ : 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,13 @@ mapMaybe⁺ {xs = x ∷ xs} {f = f} (px ∷ pxs) with f x
 ... | just v with px
 ...   | just pv = pv ∷ mapMaybe⁺ pxs
 
+------------------------------------------------------------------------
+-- catMaybes
+
+catMaybes⁺ : ∀ {xs : List (Maybe A)} → All (Maybe.Any P) xs → All P (catMaybes xs)
+catMaybes⁺ [] = []
+catMaybes⁺ (just px ∷ pxs) = px ∷ catMaybes⁺ pxs
+
 ------------------------------------------------------------------------
 -- _++_
 

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

@@ -10,9 +10,12 @@ 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 (catMaybes⁺)
 open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_)
+open import Data.Maybe.Relation.Unary.Any using (Any; just)
 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; just)
 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 +25,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 +135,16 @@ 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) = catMaybes⁺ (All.map helper x∼xs) ∷ pointwise⁺ pxs
+    where
+    helper : Pointwise R (just x) ⊆ Any (R x)
+    helper (just Rxy) = just Rxy