Added pointwise and catmaybe in Lists (agda#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 <[email protected]> Co-authored-by: MatthewDaggitt <[email protected]>
jamesmckinna · Dec 14, 2023 · 2e4061d · 2e4061d
1 parent cc7d32d
commit 2e4061d
Show file tree

Hide file tree

Showing 4 changed files with 44 additions and 3 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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 ⊔ ℓ)