From f5f9727050a2683b6ee63c4ad619c67d983426aa Mon Sep 17 00:00:00 2001
From: Guilherme Silva <guilhermehas@hotmail.com>
Date: Thu, 14 Dec 2023 05:06:36 +0100
Subject: [PATCH] Added pointwise and catmaybe in Lists (#2222)

* added pointwise and catmaybe

* added pointwise to any

* added cat maybe all

* changed pointwise definition

* changed files name

* fixed changelogs and properties

* changed Any solution

* changed pointwise to catMaybe

---------

Co-authored-by: Guilherme <alvares@chalmers.se>
Co-authored-by: MatthewDaggitt <matthewdaggitt@gmail.com>
---
 CHANGELOG.md                                     | 12 ++++++++++++
 src/Data/List/Relation/Unary/All/Properties.agda | 14 +++++++++++++-
 .../List/Relation/Unary/AllPairs/Properties.agda | 16 ++++++++++++++--
 src/Data/Maybe/Relation/Binary/Pointwise.agda    |  5 +++++
 4 files changed, 44 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e10ca58108..2701cdde9b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -27,7 +27,19 @@ New modules
 Additions to existing modules
 -----------------------------
 
+* In `Data.Maybe.Relation.Binary.Pointwise`:
+  ```agda
+  pointwise⊆any : Pointwise R (just x) ⊆ Any (R x)
+  ```
+
+* In `Data.List.Relation.Unary.All.Properties`:
+  ```agda
+  All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs)
+  Any-catMaybes⁺ : All (Maybe.Any P) xs → All P (catMaybes xs)
+  ```
+
 * In `Data.List.Relation.Unary.AllPairs.Properties`:
   ```
+  catMaybes⁺ : AllPairs (Pointwise R) xs → AllPairs R (catMaybes xs)
   tabulate⁺-< : (i < j → R (f i) (f j)) → AllPairs R (tabulate f)
   ```
diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda
index 1b55bcd2b8..d2a57b7143 100644
--- a/src/Data/List/Relation/Unary/All/Properties.agda
+++ b/src/Data/List/Relation/Unary/All/Properties.agda
@@ -28,7 +28,8 @@ import Data.List.Relation.Binary.Equality.Setoid as ListEq using (_≋_; []; _
 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.All as Maybe using (just; nothing; fromAny)
+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,17 @@ mapMaybe⁺ {xs = x ∷ xs} {f = f} (px ∷ pxs) with f x
 ... | just v with px
 ...   | just pv = pv ∷ mapMaybe⁺ pxs
 
+------------------------------------------------------------------------
+-- catMaybes
+
+All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs)
+All-catMaybes⁺ [] = []
+All-catMaybes⁺ (just px ∷ pxs) = px ∷ All-catMaybes⁺ pxs
+All-catMaybes⁺ (nothing ∷ pxs) = All-catMaybes⁺ pxs
+
+Any-catMaybes⁺ : All (Maybe.Any P) xs → All P (catMaybes xs)
+Any-catMaybes⁺ = All-catMaybes⁺ ∘ All.map fromAny
+
 ------------------------------------------------------------------------
 -- _++_
 
diff --git a/src/Data/List/Relation/Unary/AllPairs/Properties.agda b/src/Data/List/Relation/Unary/AllPairs/Properties.agda
index 027d9bb4cc..9b145c3834 100644
--- a/src/Data/List/Relation/Unary/AllPairs/Properties.agda
+++ b/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 (Any-catMaybes⁺)
 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 as F using (Fin)
 open import Data.Fin.Properties using (suc-injective; <⇒≢)
 open import Data.Nat.Base using (zero; suc; _<_; z≤n; s≤s; z<s; 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
@@ -136,3 +138,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!
+
+------------------------------------------------------------------------
+-- catMaybes
+
+module _ {R : Rel A ℓ} where
+
+  catMaybes⁺ : {xs : List (Maybe A)} → AllPairs (Pointwise R) xs → AllPairs R (catMaybes xs)
+  catMaybes⁺ {xs = []} [] = []
+  catMaybes⁺ {xs = nothing ∷  _} (x∼xs ∷ pxs) = catMaybes⁺ pxs
+  catMaybes⁺ {xs = just x  ∷ xs} (x∼xs ∷ pxs) = Any-catMaybes⁺ (All.map pointwise⊆any x∼xs) ∷ catMaybes⁺ pxs
diff --git a/src/Data/Maybe/Relation/Binary/Pointwise.agda b/src/Data/Maybe/Relation/Binary/Pointwise.agda
index 48fa144a2e..3da2abd9f1 100644
--- a/src/Data/Maybe/Relation/Binary/Pointwise.agda
+++ b/src/Data/Maybe/Relation/Binary/Pointwise.agda
@@ -11,6 +11,7 @@ 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)
@@ -18,6 +19,7 @@ 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 ⊔ ℓ)