From 4b1993e38fda3807c2be3e81510ae78ab1522d0c Mon Sep 17 00:00:00 2001 From: Guilherme Date: Fri, 1 Dec 2023 14:35:28 +0100 Subject: [PATCH 1/8] added pointwise and catmaybe --- CHANGELOG.md | 10 ++++++++++ .../List/Relation/Unary/All/Properties.agda | 8 ++++++++ .../Relation/Unary/AllPairs/Properties.agda | 20 +++++++++++++++++-- 3 files changed, 36 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index f494eee972..822336a136 100644 --- a/CHANGELOG.md +++ b/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) +``` diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda index 1b55bcd2b8..0ac486ebfc 100644 --- a/src/Data/List/Relation/Unary/All/Properties.agda +++ b/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 Date: Mon, 4 Dec 2023 15:25:57 +0100 Subject: [PATCH 2/8] added pointwise to any --- CHANGELOG.md | 5 +++++ src/Data/List/Relation/Unary/AllPairs/Properties.agda | 8 ++------ src/Data/Maybe/Relation/Binary/Pointwise.agda | 5 +++++ 3 files changed, 12 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 822336a136..7c5173e57a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3910,6 +3910,11 @@ This is a full list of proofs that have changed form to use irrelevant instance 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`: ``` catMaybes⁺ : All (Maybe.Any P) xs → All P (catMaybes xs) diff --git a/src/Data/List/Relation/Unary/AllPairs/Properties.agda b/src/Data/List/Relation/Unary/AllPairs/Properties.agda index 8717cc256f..c1a23048dd 100644 --- a/src/Data/List/Relation/Unary/AllPairs/Properties.agda +++ b/src/Data/List/Relation/Unary/AllPairs/Properties.agda @@ -12,10 +12,9 @@ open import Data.List.Base hiding (any) open import Data.List.Relation.Unary.All as All using (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.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) @@ -144,7 +143,4 @@ 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 + pointwise⁺ {xs = just x ∷ xs} (x∼xs ∷ pxs) = catMaybes⁺ (All.map pointwise⊆any x∼xs) ∷ pointwise⁺ 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 ⊔ ℓ) From b0e723209da5bac2ff2cf913957cffd8078995f1 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Mon, 4 Dec 2023 15:33:52 +0100 Subject: [PATCH 3/8] added cat maybe all --- CHANGELOG.md | 3 ++- src/Data/List/Relation/Unary/All/Properties.agda | 11 ++++++++--- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7c5173e57a..f4959c700f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3917,7 +3917,8 @@ This is a full list of proofs that have changed form to use irrelevant instance * In `Data.List.Relation.Unary.All.Properties`: ``` - catMaybes⁺ : All (Maybe.Any P) xs → All P (catMaybes xs) + 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`: diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda index 0ac486ebfc..e6d929ffa8 100644 --- a/src/Data/List/Relation/Unary/All/Properties.agda +++ b/src/Data/List/Relation/Unary/All/Properties.agda @@ -392,9 +392,14 @@ mapMaybe⁺ {xs = x ∷ xs} {f = f} (px ∷ pxs) with f x ------------------------------------------------------------------------ -- catMaybes -catMaybes⁺ : ∀ {xs : List (Maybe A)} → All (Maybe.Any P) xs → All P (catMaybes xs) -catMaybes⁺ [] = [] -catMaybes⁺ (just px ∷ pxs) = px ∷ catMaybes⁺ pxs +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 ------------------------------------------------------------------------ -- _++_ From 873d28ff559f034244552115cbb6dc480bd6def6 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Mon, 4 Dec 2023 16:03:58 +0100 Subject: [PATCH 4/8] changed pointwise definition --- src/Data/List/Relation/Unary/AllPairs/Properties.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/List/Relation/Unary/AllPairs/Properties.agda b/src/Data/List/Relation/Unary/AllPairs/Properties.agda index c1a23048dd..e506526eec 100644 --- a/src/Data/List/Relation/Unary/AllPairs/Properties.agda +++ b/src/Data/List/Relation/Unary/AllPairs/Properties.agda @@ -10,7 +10,7 @@ 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; []; _∷_) -open import Data.List.Relation.Unary.All.Properties as All using (catMaybes⁺) +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) @@ -143,4 +143,4 @@ 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 pointwise⊆any x∼xs) ∷ pointwise⁺ pxs + pointwise⁺ {xs = just x ∷ xs} (x∼xs ∷ pxs) = catMaybesAny⁺ (All.map pointwise⊆any x∼xs) ∷ pointwise⁺ pxs From 076c18126c03701b460378dea606378aa5d98bbd Mon Sep 17 00:00:00 2001 From: Guilherme Date: Wed, 13 Dec 2023 15:10:09 +0100 Subject: [PATCH 5/8] changed files name --- CHANGELOG.md | 6 +++--- src/Data/List/Relation/Unary/All/Properties.agda | 16 ++++++++-------- .../List/Relation/Unary/AllPairs/Properties.agda | 10 +++++----- 3 files changed, 16 insertions(+), 16 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index f4959c700f..323b32d457 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3917,11 +3917,11 @@ This is a full list of proofs that have changed form to use irrelevant instance * 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) + +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`: ``` - pointwise⁺ : AllPairs (Pointwise R) xs → AllPairs R (catMaybes xs) + catMaybes⁺ : AllPairs (Pointwise R) xs → AllPairs R (catMaybes xs) ``` diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda index e6d929ffa8..a7f72aa3f5 100644 --- a/src/Data/List/Relation/Unary/All/Properties.agda +++ b/src/Data/List/Relation/Unary/All/Properties.agda @@ -392,14 +392,14 @@ mapMaybe⁺ {xs = x ∷ xs} {f = f} (px ∷ pxs) with f x ------------------------------------------------------------------------ -- 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 +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⁺ [] = [] +Any-catMaybes⁺ (just px ∷ pxs) = px ∷ Any-catMaybes⁺ pxs ------------------------------------------------------------------------ -- _++_ diff --git a/src/Data/List/Relation/Unary/AllPairs/Properties.agda b/src/Data/List/Relation/Unary/AllPairs/Properties.agda index e506526eec..91f0c4e21f 100644 --- a/src/Data/List/Relation/Unary/AllPairs/Properties.agda +++ b/src/Data/List/Relation/Unary/AllPairs/Properties.agda @@ -138,9 +138,9 @@ module _ {R : Rel A ℓ} {P : Pred A p} (P? : Decidable P) where ------------------------------------------------------------------------ -- pointwise -module _ {R : Rel A ℓ} where +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 + 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) = catMaybesAny⁺ (All.map catMaybes⊆any x∼xs) ∷ catMaybes⁺ pxs From e4bc04bc6e2e13296c494cfa5d490cf6f745e8ce Mon Sep 17 00:00:00 2001 From: Guilherme Date: Wed, 13 Dec 2023 15:15:12 +0100 Subject: [PATCH 6/8] fixed changelogs and properties --- CHANGELOG.md | 4 ++-- src/Data/List/Relation/Unary/AllPairs/Properties.agda | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 323b32d457..57e40b04b7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3917,8 +3917,8 @@ This is a full list of proofs that have changed form to use irrelevant instance * In `Data.List.Relation.Unary.All.Properties`: ``` - +All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs) - +Any-catMaybes⁺ : All (Maybe.Any P) xs → All P (catMaybes xs) + 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`: diff --git a/src/Data/List/Relation/Unary/AllPairs/Properties.agda b/src/Data/List/Relation/Unary/AllPairs/Properties.agda index 91f0c4e21f..7d99ac9071 100644 --- a/src/Data/List/Relation/Unary/AllPairs/Properties.agda +++ b/src/Data/List/Relation/Unary/AllPairs/Properties.agda @@ -10,7 +10,7 @@ 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; []; _∷_) -open import Data.List.Relation.Unary.All.Properties as All using (catMaybesAny⁺) +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) @@ -143,4 +143,4 @@ 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) = catMaybesAny⁺ (All.map catMaybes⊆any x∼xs) ∷ catMaybes⁺ pxs + catMaybes⁺ {xs = just x ∷ xs} (x∼xs ∷ pxs) = Any-catMaybes⁺ (All.map pointwise⊆any x∼xs) ∷ catMaybes⁺ pxs From 3ef73634e5981017e7bd54fb879fed9e23624930 Mon Sep 17 00:00:00 2001 From: Guilherme Date: Wed, 13 Dec 2023 15:34:07 +0100 Subject: [PATCH 7/8] changed Any solution --- src/Data/List/Relation/Unary/All/Properties.agda | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda index a7f72aa3f5..d2a57b7143 100644 --- a/src/Data/List/Relation/Unary/All/Properties.agda +++ b/src/Data/List/Relation/Unary/All/Properties.agda @@ -28,7 +28,7 @@ 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 Date: Wed, 13 Dec 2023 21:13:25 +0100 Subject: [PATCH 8/8] changed pointwise to catMaybe --- src/Data/List/Relation/Unary/AllPairs/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/List/Relation/Unary/AllPairs/Properties.agda b/src/Data/List/Relation/Unary/AllPairs/Properties.agda index 7d99ac9071..71a236cef6 100644 --- a/src/Data/List/Relation/Unary/AllPairs/Properties.agda +++ b/src/Data/List/Relation/Unary/AllPairs/Properties.agda @@ -136,7 +136,7 @@ module _ {R : Rel A ℓ} {P : Pred A p} (P? : Decidable P) where ... | true = All.filter⁺ P? x∉xs ∷ filter⁺ xs! ------------------------------------------------------------------------ --- pointwise +-- catMaybes module _ {R : Rel A ℓ} where