From a75092763e959b74b333f55b87c966d647656309 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Mon, 25 Mar 2024 21:31:11 -0400 Subject: [PATCH 1/9] add some 'very dependent' maps to Data.Product. More documentation to come later. --- src/Data/Product.agda | 25 +++++++++++++++++++++++-- 1 file changed, 23 insertions(+), 2 deletions(-) diff --git a/src/Data/Product.agda b/src/Data/Product.agda index 02bf53a97b..cc800e8079 100644 --- a/src/Data/Product.agda +++ b/src/Data/Product.agda @@ -14,14 +14,35 @@ open import Relation.Nullary.Negation.Core private variable - a b c ℓ : Level - A B : Set a + a b c ℓ p q r s : Level + A B C : Set a ------------------------------------------------------------------------ -- Definition of dependent products open import Data.Product.Base public +-- These are here as they are not 'basic' but instead "very dependent", +-- i.e. the result type depends on the full input 'point' v. +dep-map : {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Set q} → + (f : (x : A) → B x) → (∀ {x} → (y : P x) → Q y (f x)) → + (v : Σ A P) → Σ (B (proj₁ v)) (Q (proj₂ v)) +dep-map f g (x , y) = (f x , g y) + +-- This is a "non-dependent" version of dep-map whereby the input is actually +-- a pair (i.e. _×_ ) but the output type still depends on the input 'point' v. +dep-map′ : {B : A → Set b} {P : Set p} {Q : P → Set q} → + (f : (x : A) → B x) → ((x : P) → Q x) → (v : A × P) → B (proj₁ v) × Q (proj₂ v) +dep-map′ f g (x , y) = (f x , g y) + +-- This is a generic zipWith for Σ where different functions are applied to each +-- component pair, and recombined. +zipWith : {P : A → Set p} {Q : B → Set q} {R : C → Set r} {S : (x : C) → R x → Set s} + (_∙_ : A → B → C) → (_∘_ : ∀ {x y} → P x → Q y → R (x ∙ y)) → + (_*_ : (x : C) → (y : R x) → S x y) → + (x : Σ A P) → (y : Σ B Q) → S (proj₁ x ∙ proj₁ y) (proj₂ x ∘ proj₂ y) +zipWith _∙_ _∘_ _*_ (a , p) (b , q) = (a ∙ b) * (p ∘ q) + ------------------------------------------------------------------------ -- Negation of existential quantifier From 3287bee20249124216c0c116173fd1a67799a53e Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Tue, 23 Apr 2024 20:50:51 -0400 Subject: [PATCH 2/9] and document --- CHANGELOG.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index ac44c5e869..97802145c2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -458,6 +458,21 @@ Additions to existing modules product-↭ : product Preserves _↭_ ⟶ _≡_ ``` +* Added some very-dependent map and zipWith to `Data.Product`. + ```agda + dep-map : {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Set q} → + (f : (x : A) → B x) → (∀ {x} → (y : P x) → Q y (f x)) → + (v : Σ A P) → Σ (B (proj₁ v)) (Q (proj₂ v)) + + dep-map′ : {B : A → Set b} {P : Set p} {Q : P → Set q} → + (f : (x : A) → B x) → ((x : P) → Q x) → (v : A × P) → B (proj₁ v) × Q (proj₂ v) + + zipWith : {P : A → Set p} {Q : B → Set q} {R : C → Set r} {S : (x : C) → R x → Set s} + (_∙_ : A → B → C) → (_∘_ : ∀ {x y} → P x → Q y → R (x ∙ y)) → + (_*_ : (x : C) → (y : R x) → S x y) → + (x : Σ A P) → (y : Σ B Q) → S (proj₁ x ∙ proj₁ y) (proj₂ x ∘ proj₂ y) + + ``` * Added new functions in `Data.String.Base`: ```agda map : (Char → Char) → String → String From 829e819a99675b95ea4f8fc198ef62174bccf3fa Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Tue, 23 Apr 2024 21:37:42 -0400 Subject: [PATCH 3/9] make imports more precise --- src/Data/Product.agda | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Data/Product.agda b/src/Data/Product.agda index cc800e8079..fe295025e1 100644 --- a/src/Data/Product.agda +++ b/src/Data/Product.agda @@ -8,9 +8,8 @@ module Data.Product where -open import Function.Base -open import Level -open import Relation.Nullary.Negation.Core +open import Level using (Level; _⊔_) +open import Relation.Nullary.Negation.Core using (¬_) private variable From 7e3da8bad34003a2fc4aad9de025a0397f84b6f1 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Tue, 23 Apr 2024 21:38:13 -0400 Subject: [PATCH 4/9] minimal properties of very-dependen map and zipWith. Structured to make it easy to add more. --- src/Data/Product/Properties/Dependent.agda | 53 ++++++++++++++++++++++ 1 file changed, 53 insertions(+) create mode 100644 src/Data/Product/Properties/Dependent.agda diff --git a/src/Data/Product/Properties/Dependent.agda b/src/Data/Product/Properties/Dependent.agda new file mode 100644 index 0000000000..890941f82f --- /dev/null +++ b/src/Data/Product/Properties/Dependent.agda @@ -0,0 +1,53 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of 'very dependent' map / zipWith over products +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Data.Product.Properties.Dependent where + +open import Data.Product using (Σ; _×_; _,_; dep-map; dep-map′; zipWith) +open import Function.Base using (id; flip) +open import Level using (Level) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; _≗_; cong₂; refl) + +private + variable + a b p q r s : Level + A B C : Set a + +------------------------------------------------------------------------ +-- dep-map + +module _ {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Set q} where + + dep-map-cong : {f g : (x : A) → B x} → {h i : ∀ {x} → (y : P x) → Q y (f x)} → + (∀ x → f x ≡ g x) → + (∀ {x} → (y : P x) → h y ≡ i y) → + (v : Σ A P) → dep-map f h v ≡ dep-map g i v + dep-map-cong f≗g h≗i (x , y) = cong₂ _,_ (f≗g x) (h≗i y) + +------------------------------------------------------------------------ +-- dep-map′ + +module _ {B : A → Set b} {P : Set p} {Q : P → Set q} where + + dep-map′-cong : {f g : (x : A) → B x} → {h i : (x : P) → Q x} → + (∀ x → f x ≡ g x) → + ((y : P) → h y ≡ i y) → + (v : A × P) → dep-map′ f h v ≡ dep-map′ g i v + dep-map′-cong f≗g h≗i (x , y) = cong₂ _,_ (f≗g x) (h≗i y) + +------------------------------------------------------------------------ +-- zipWith + +module _ {P : A → Set p} {Q : B → Set q} {R : C → Set r} {S : (x : C) → R x → Set s} where + + zipWith-flip : (_∙_ : A → B → C) → (_∘_ : ∀ {x y} → P x → Q y → R (x ∙ y)) → + (_*_ : (x : C) → (y : R x) → S x y) → + {x : Σ A P} → {y : Σ B Q} → + zipWith _∙_ _∘_ _*_ x y ≡ zipWith (flip _∙_) (flip _∘_) _*_ y x + zipWith-flip _∙_ _∘_ _*_ = refl From e3dffb847b42256cfe7a31faa4d28ad727dad57d Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Tue, 23 Apr 2024 21:51:57 -0400 Subject: [PATCH 5/9] whitespace --- src/Data/Product/Properties/Dependent.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Product/Properties/Dependent.agda b/src/Data/Product/Properties/Dependent.agda index 890941f82f..42ca3f060d 100644 --- a/src/Data/Product/Properties/Dependent.agda +++ b/src/Data/Product/Properties/Dependent.agda @@ -29,7 +29,7 @@ module _ {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Se (∀ {x} → (y : P x) → h y ≡ i y) → (v : Σ A P) → dep-map f h v ≡ dep-map g i v dep-map-cong f≗g h≗i (x , y) = cong₂ _,_ (f≗g x) (h≗i y) - + ------------------------------------------------------------------------ -- dep-map′ From a3fce90a16b6da83a6530966de7851da2a57d8a0 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Thu, 2 May 2024 21:59:59 -0400 Subject: [PATCH 6/9] implement new names and suggestions about using pattern-matching in the type --- CHANGELOG.md | 11 ++++++----- src/Data/Product.agda | 18 +++++++++--------- src/Data/Product/Properties/Dependent.agda | 6 +++--- 3 files changed, 18 insertions(+), 17 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 94825c7db9..9ffd86797d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -467,17 +467,18 @@ Additions to existing modules * Added some very-dependent map and zipWith to `Data.Product`. ```agda - dep-map : {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Set q} → + map-Σ : {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Set q} → (f : (x : A) → B x) → (∀ {x} → (y : P x) → Q y (f x)) → - (v : Σ A P) → Σ (B (proj₁ v)) (Q (proj₂ v)) + ((x , y) : Σ A P) → Σ (B x) (Q y) - dep-map′ : {B : A → Set b} {P : Set p} {Q : P → Set q} → - (f : (x : A) → B x) → ((x : P) → Q x) → (v : A × P) → B (proj₁ v) × Q (proj₂ v) + map-Σ′ : {B : A → Set b} {P : Set p} {Q : P → Set q} → + (f : (x : A) → B x) → ((x : P) → Q x) → ((x , y) : A × P) → B x × Q y zipWith : {P : A → Set p} {Q : B → Set q} {R : C → Set r} {S : (x : C) → R x → Set s} (_∙_ : A → B → C) → (_∘_ : ∀ {x y} → P x → Q y → R (x ∙ y)) → (_*_ : (x : C) → (y : R x) → S x y) → - (x : Σ A P) → (y : Σ B Q) → S (proj₁ x ∙ proj₁ y) (proj₂ x ∘ proj₂ y) + ((a , p) : Σ A P) → ((b , q) : Σ B Q) → + S (a ∙ b) (p ∘ q) ``` * Added new functions in `Data.String.Base`: diff --git a/src/Data/Product.agda b/src/Data/Product.agda index fe295025e1..693c5a8f5a 100644 --- a/src/Data/Product.agda +++ b/src/Data/Product.agda @@ -22,24 +22,24 @@ private open import Data.Product.Base public -- These are here as they are not 'basic' but instead "very dependent", --- i.e. the result type depends on the full input 'point' v. -dep-map : {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Set q} → +-- i.e. the result type depends on the full input 'point' (x , y). +map-Σ : {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Set q} → (f : (x : A) → B x) → (∀ {x} → (y : P x) → Q y (f x)) → - (v : Σ A P) → Σ (B (proj₁ v)) (Q (proj₂ v)) -dep-map f g (x , y) = (f x , g y) + ((x , y) : Σ A P) → Σ (B x) (Q y) +map-Σ f g (x , y) = (f x , g y) -- This is a "non-dependent" version of dep-map whereby the input is actually --- a pair (i.e. _×_ ) but the output type still depends on the input 'point' v. -dep-map′ : {B : A → Set b} {P : Set p} {Q : P → Set q} → - (f : (x : A) → B x) → ((x : P) → Q x) → (v : A × P) → B (proj₁ v) × Q (proj₂ v) -dep-map′ f g (x , y) = (f x , g y) +-- a pair (i.e. _×_ ) but the output type still depends on the input 'point' (x , y). +map-Σ′ : {B : A → Set b} {P : Set p} {Q : P → Set q} → + (f : (x : A) → B x) → ((x : P) → Q x) → ((x , y) : A × P) → B x × Q y +map-Σ′ f g (x , y) = (f x , g y) -- This is a generic zipWith for Σ where different functions are applied to each -- component pair, and recombined. zipWith : {P : A → Set p} {Q : B → Set q} {R : C → Set r} {S : (x : C) → R x → Set s} (_∙_ : A → B → C) → (_∘_ : ∀ {x y} → P x → Q y → R (x ∙ y)) → (_*_ : (x : C) → (y : R x) → S x y) → - (x : Σ A P) → (y : Σ B Q) → S (proj₁ x ∙ proj₁ y) (proj₂ x ∘ proj₂ y) + ((a , p) : Σ A P) → ((b , q) : Σ B Q) → S (a ∙ b) (p ∘ q) zipWith _∙_ _∘_ _*_ (a , p) (b , q) = (a ∙ b) * (p ∘ q) ------------------------------------------------------------------------ diff --git a/src/Data/Product/Properties/Dependent.agda b/src/Data/Product/Properties/Dependent.agda index 42ca3f060d..560af96217 100644 --- a/src/Data/Product/Properties/Dependent.agda +++ b/src/Data/Product/Properties/Dependent.agda @@ -8,7 +8,7 @@ module Data.Product.Properties.Dependent where -open import Data.Product using (Σ; _×_; _,_; dep-map; dep-map′; zipWith) +open import Data.Product using (Σ; _×_; _,_; map-Σ; map-Σ′; zipWith) open import Function.Base using (id; flip) open import Level using (Level) open import Relation.Binary.PropositionalEquality.Core @@ -27,7 +27,7 @@ module _ {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Se dep-map-cong : {f g : (x : A) → B x} → {h i : ∀ {x} → (y : P x) → Q y (f x)} → (∀ x → f x ≡ g x) → (∀ {x} → (y : P x) → h y ≡ i y) → - (v : Σ A P) → dep-map f h v ≡ dep-map g i v + (v : Σ A P) → map-Σ f h v ≡ map-Σ g i v dep-map-cong f≗g h≗i (x , y) = cong₂ _,_ (f≗g x) (h≗i y) ------------------------------------------------------------------------ @@ -38,7 +38,7 @@ module _ {B : A → Set b} {P : Set p} {Q : P → Set q} where dep-map′-cong : {f g : (x : A) → B x} → {h i : (x : P) → Q x} → (∀ x → f x ≡ g x) → ((y : P) → h y ≡ i y) → - (v : A × P) → dep-map′ f h v ≡ dep-map′ g i v + (v : A × P) → map-Σ′ f h v ≡ map-Σ′ g i v dep-map′-cong f≗g h≗i (x , y) = cong₂ _,_ (f≗g x) (h≗i y) ------------------------------------------------------------------------ From baa18617aa6225c1cb533d94325c69646e11cab7 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Thu, 2 May 2024 22:01:39 -0400 Subject: [PATCH 7/9] whitespace in CHANGELOG --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9ffd86797d..461bc2c0a8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -478,7 +478,7 @@ Additions to existing modules (_∙_ : A → B → C) → (_∘_ : ∀ {x y} → P x → Q y → R (x ∙ y)) → (_*_ : (x : C) → (y : R x) → S x y) → ((a , p) : Σ A P) → ((b , q) : Σ B Q) → - S (a ∙ b) (p ∘ q) + S (a ∙ b) (p ∘ q) ``` * Added new functions in `Data.String.Base`: From 84a4bf73e14089b6a602b343c36c11144b7b2b32 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Sun, 5 May 2024 13:35:30 -0400 Subject: [PATCH 8/9] small cleanup based on latest round of comments --- src/Data/Product.agda | 2 +- src/Data/Product/Properties/Dependent.agda | 16 ++++++++-------- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/Data/Product.agda b/src/Data/Product.agda index 693c5a8f5a..d0f6db0cde 100644 --- a/src/Data/Product.agda +++ b/src/Data/Product.agda @@ -28,7 +28,7 @@ map-Σ : {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Se ((x , y) : Σ A P) → Σ (B x) (Q y) map-Σ f g (x , y) = (f x , g y) --- This is a "non-dependent" version of dep-map whereby the input is actually +-- This is a "non-dependent" version of map-Σ whereby the input is actually -- a pair (i.e. _×_ ) but the output type still depends on the input 'point' (x , y). map-Σ′ : {B : A → Set b} {P : Set p} {Q : P → Set q} → (f : (x : A) → B x) → ((x : P) → Q x) → ((x , y) : A × P) → B x × Q y diff --git a/src/Data/Product/Properties/Dependent.agda b/src/Data/Product/Properties/Dependent.agda index 560af96217..5d01bbfbb6 100644 --- a/src/Data/Product/Properties/Dependent.agda +++ b/src/Data/Product/Properties/Dependent.agda @@ -24,22 +24,22 @@ private module _ {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Set q} where - dep-map-cong : {f g : (x : A) → B x} → {h i : ∀ {x} → (y : P x) → Q y (f x)} → + map-Σ-cong : {f g : (x : A) → B x} → {h k : ∀ {x} → (y : P x) → Q y (f x)} → (∀ x → f x ≡ g x) → - (∀ {x} → (y : P x) → h y ≡ i y) → - (v : Σ A P) → map-Σ f h v ≡ map-Σ g i v - dep-map-cong f≗g h≗i (x , y) = cong₂ _,_ (f≗g x) (h≗i y) + (∀ {x} → (y : P x) → h y ≡ k y) → + (v : Σ A P) → map-Σ f h v ≡ map-Σ g k v + map-Σ-cong f≗g h≗k (x , y) = cong₂ _,_ (f≗g x) (h≗k y) ------------------------------------------------------------------------ -- dep-map′ module _ {B : A → Set b} {P : Set p} {Q : P → Set q} where - dep-map′-cong : {f g : (x : A) → B x} → {h i : (x : P) → Q x} → + map-Σ′-cong : {f g : (x : A) → B x} → {h k : (x : P) → Q x} → (∀ x → f x ≡ g x) → - ((y : P) → h y ≡ i y) → - (v : A × P) → map-Σ′ f h v ≡ map-Σ′ g i v - dep-map′-cong f≗g h≗i (x , y) = cong₂ _,_ (f≗g x) (h≗i y) + ((y : P) → h y ≡ k y) → + (v : A × P) → map-Σ′ f h v ≡ map-Σ′ g k v + map-Σ′-cong f≗g h≗k (x , y) = cong₂ _,_ (f≗g x) (h≗k y) ------------------------------------------------------------------------ -- zipWith From dda6607dac19d05d37cf46b62a5316c282d0302f Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Wed, 15 May 2024 22:57:09 -0400 Subject: [PATCH 9/9] and fix the names in the comments too. --- src/Data/Product/Properties/Dependent.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Product/Properties/Dependent.agda b/src/Data/Product/Properties/Dependent.agda index 5d01bbfbb6..122b4e3f12 100644 --- a/src/Data/Product/Properties/Dependent.agda +++ b/src/Data/Product/Properties/Dependent.agda @@ -20,7 +20,7 @@ private A B C : Set a ------------------------------------------------------------------------ --- dep-map +-- map-Σ module _ {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Set q} where @@ -31,7 +31,7 @@ module _ {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Se map-Σ-cong f≗g h≗k (x , y) = cong₂ _,_ (f≗g x) (h≗k y) ------------------------------------------------------------------------ --- dep-map′ +-- map-Σ′ module _ {B : A → Set b} {P : Set p} {Q : P → Set q} where