From 6909af004e587013162e5a35b64c6c53f7037560 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 20 Jun 2026 10:53:49 +0100 Subject: [PATCH 01/14] [ add ] `Data.List.Base.foldMap` --- CHANGELOG.md | 5 +++++ src/Data/List/Base.agda | 7 +++++++ 2 files changed, 12 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 586d4c71cd..9d59c82799 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -166,6 +166,11 @@ Additions to existing modules gcd[i,i]≡∣i∣ : ∀ i → gcd i i ≡ + ∣i∣ ``` +* In `Data.List.Base`: + ```agda + foldMap : (B → B → B) → B → (A → B) → List A → B + ``` + * In `Data.Nat.GCD`: ```agda gcd[n,n]≡n : ∀ n → gcd n n ≡ n diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index 548e0bd827..00c6db2c38 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -123,6 +123,13 @@ merge R? x∷xs@(x ∷ xs) y∷ys@(y ∷ ys) = if does (R? x y) ------------------------------------------------------------------------ -- Operations for reducing lists +foldMap : (B → B → B) → B → (A → B) → List A → B +foldMap _∙_ ε f = go + module FoldMap where + go : List _ → _ + go [] = ε + go (x ∷ xs) = (f x) ∙ (go xs) + foldr : (A → B → B) → B → List A → B foldr c n [] = n foldr c n (x ∷ xs) = c x (foldr c n xs) From 516790a558aa5bef6daafc8138f06fa791d2565e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 20 Jun 2026 11:04:20 +0100 Subject: [PATCH 02/14] refactor: `Data.List.Effectful.Foldable.foldMap` --- src/Data/List/Effectful/Foldable.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Data/List/Effectful/Foldable.agda b/src/Data/List/Effectful/Foldable.agda index 5d2f8656ec..1d8a0b20a9 100644 --- a/src/Data/List/Effectful/Foldable.agda +++ b/src/Data/List/Effectful/Foldable.agda @@ -30,8 +30,7 @@ module _ (M : RawMonoid c ℓ) where open RawMonoid M foldMap : (A → Carrier) → List A → Carrier - foldMap f [] = ε - foldMap f (x ∷ xs) = f x ∙ foldMap f xs + foldMap = List.foldMap _∙_ ε ------------------------------------------------------------------------ -- Basic implementation using supplied defaults From 4f89cd54642dde8b88adea49a30280c66450971b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 21 Jun 2026 09:36:03 +0100 Subject: [PATCH 03/14] add: property --- CHANGELOG.md | 5 +++++ src/Data/List/Properties.agda | 6 ++++++ 2 files changed, 11 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9d59c82799..fd17d85551 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -171,6 +171,11 @@ Additions to existing modules foldMap : (B → B → B) → B → (A → B) → List A → B ``` +* In `Data.List.Properties`: + ```agda + foldMap≗foldr∘map : foldMap _∙_ ε f ≗ foldr (λ x → f x ∙_) ε + ``` + * In `Data.Nat.GCD`: ```agda gcd[n,n]≡n : ∀ n → gcd n n ≡ n diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 2fc94a996b..0e4212559b 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -644,6 +644,12 @@ foldr-map : ∀ (f : A → B → B) (g : C → A) x xs → foldr f x (map g xs) foldr-map f g x [] = refl foldr-map f g x (y ∷ xs) = cong (f (g y)) (foldr-map f g x xs) +module _ (_∙_ : B → B → B) (ε : B) (f : A → B) where + + foldMap≗foldr∘map : foldMap _∙_ ε f ≗ foldr (λ x → f x ∙_) ε + foldMap≗foldr∘map [] = refl + foldMap≗foldr∘map (x ∷ xs) = cong (f x ∙_) (foldMap≗foldr∘map xs) + -- Interaction with predicates module _ {P : Pred A p} {f : A → A → A} where From 83f19d4d501675f7154da056327b880153e95461 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 22 Jun 2026 06:32:22 +0100 Subject: [PATCH 04/14] refactor: move `foldr-commMonoid` to `Data.List.Effectful.Foldable` --- CHANGELOG.md | 5 ++ src/Data/List/Effectful/Foldable.agda | 39 +++++++++++++-- .../Binary/Permutation/Setoid/Properties.agda | 48 ++++++++----------- src/Data/Nat/ListAction/Properties.agda | 10 ++-- 4 files changed, 64 insertions(+), 38 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index fd17d85551..0323a37de1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -86,6 +86,11 @@ Deprecated names gcd[0,0]≡0 ↦ gcd[i,i]≡∣i∣ ``` +* In `Data.List.Relation.Binary.Permutation.Setoid.Properties`: + ```agda + foldr-commMonoid ↦ Data.List.Effectful.Foldable.foldr-commMonoid + ``` + * In `Data.Nat.GCD`: ```agda gcd[0,0]≡0 ↦ gcd[n,n]≡n diff --git a/src/Data/List/Effectful/Foldable.agda b/src/Data/List/Effectful/Foldable.agda index 1d8a0b20a9..73a012f814 100644 --- a/src/Data/List/Effectful/Foldable.agda +++ b/src/Data/List/Effectful/Foldable.agda @@ -8,18 +8,26 @@ module Data.List.Effectful.Foldable where -open import Algebra.Bundles using (Monoid) +open import Algebra.Bundles using (Monoid; CommutativeMonoid) open import Algebra.Bundles.Raw using (RawMonoid) open import Algebra.Morphism.Structures using (IsMonoidHomomorphism) -open import Data.List.Base as List using (List; []; _∷_; _++_) +open import Data.List.Base as List using (List; []; _∷_; _++_; foldr) +import Data.List.Relation.Binary.Permutation.Setoid as Permutation +open import Data.List.Relation.Binary.Pointwise as Pointwise + using (Pointwise) open import Effect.Foldable using (RawFoldableWithDefaults; RawFoldable) open import Function.Base using (_∘_; id) +open import Function.Bundles using (Func) +open import Function.Construct.Identity using (function) open import Level using (Level) +open import Relation.Binary.Definitions using (Monotonic₁) +open import Relation.Binary.Bundles using (Setoid) import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; cong) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning private variable - a c ℓ : Level + a c r ℓ : Level A : Set a ------------------------------------------------------------------------ @@ -50,7 +58,7 @@ foldable = record } ------------------------------------------------------------------------ --- Properties +-- foldMap gives rise to a Monoid homomorphism module _ (M : Monoid c ℓ) (f : A → Monoid.Carrier M) where @@ -75,3 +83,26 @@ module _ (M : Monoid c ℓ) (f : A → Monoid.Carrier M) where } ; ε-homo = []-homo } + +------------------------------------------------------------------------ +-- for Commutative Monoids, foldr respects Permutation + +module _ (commutativeMonoid : CommutativeMonoid c ℓ) where + + private + open module CM = CommutativeMonoid commutativeMonoid + using (_∙_; ε; ∙-cong; ∙-congˡ; ∙-congʳ; assoc; comm) + open Permutation CM.setoid + + foldr-commMonoid : Monotonic₁ _↭_ CM._≈_ (foldr _∙_ ε) + foldr-commMonoid (refl xs≋ys) = Pointwise.foldr⁺ ∙-cong CM.refl xs≋ys + foldr-commMonoid (prep x≈y xs↭ys) = ∙-cong x≈y (foldr-commMonoid xs↭ys) + foldr-commMonoid (swap {xs} {ys} {x} {y} {x′} {y′} x≈x′ y≈y′ xs↭ys) = begin + x ∙ (y ∙ foldr _∙_ ε xs) ≈⟨ ∙-congˡ (∙-congˡ (foldr-commMonoid xs↭ys)) ⟩ + x ∙ (y ∙ foldr _∙_ ε ys) ≈⟨ assoc x y (foldr _∙_ ε ys) ⟨ + (x ∙ y) ∙ foldr _∙_ ε ys ≈⟨ ∙-congʳ (comm x y) ⟩ + (y ∙ x) ∙ foldr _∙_ ε ys ≈⟨ ∙-congʳ (∙-cong y≈y′ x≈x′) ⟩ + (y′ ∙ x′) ∙ foldr _∙_ ε ys ≈⟨ assoc y′ x′ (foldr _∙_ ε ys) ⟩ + y′ ∙ (x′ ∙ foldr _∙_ ε ys) ∎ + where open ≈-Reasoning CM.setoid + foldr-commMonoid (trans xs↭ys ys↭zs) = CM.trans (foldr-commMonoid xs↭ys) (foldr-commMonoid ys↭zs) diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda index 9463dec462..6f7ba10bde 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda @@ -6,10 +6,7 @@ {-# OPTIONS --without-K --safe #-} -open import Relation.Binary.Core - using (Rel; _⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_) open import Relation.Binary.Bundles using (Setoid) -open import Relation.Binary.Definitions as B hiding (Decidable) module Data.List.Relation.Binary.Permutation.Setoid.Properties {a ℓ} (S : Setoid a ℓ) @@ -19,6 +16,7 @@ open import Algebra open import Data.Bool.Base using (true; false) open import Data.Fin.Base using (zero; suc) open import Data.List.Base as List hiding (head; tail) +import Data.List.Effectful.Foldable as Foldable open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise; head; tail) import Data.List.Relation.Binary.Equality.Setoid as Equality @@ -37,13 +35,16 @@ open import Data.Product.Base using (_,_; _×_; ∃; ∃₂; proj₁; proj₂) open import Function.Base using (_∘_; _⟨_⟩_; flip) open import Function.Bundles using (Inverse) open import Level using (Level; _⊔_) -open import Relation.Unary using (Pred; Decidable) -import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +open import Relation.Binary.Core + using (Rel; _⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_) +open import Relation.Binary.Definitions as B hiding (Decidable) open import Relation.Binary.Properties.Setoid S using (≉-resp₂) open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_ ; refl; sym; cong; cong₂; subst; _≢_) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Relation.Nullary.Decidable using (yes; no; does) open import Relation.Nullary.Negation using (¬_; contradiction; contraposition) +open import Relation.Unary using (Pred; Decidable) open Setoid S using (_≈_) @@ -419,29 +420,7 @@ module _ (R? : B.Decidable R) where where open PermutationReasoning ------------------------------------------------------------------------ --- foldr over a Commutative Monoid - -module _{_∙_ : Op₂ A} {ε : A} - (isCommutativeMonoid : IsCommutativeMonoid _≈_ _∙_ ε) where - - private - commutativeMonoid : CommutativeMonoid _ _ - commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid } - open module CM = CommutativeMonoid commutativeMonoid - using (∙-cong; ∙-congˡ; ∙-congʳ; assoc; comm) - - foldr-commMonoid : (foldr _∙_ ε) Preserves _↭_ ⟶ _≈_ - foldr-commMonoid (refl xs≋ys) = Pointwise.foldr⁺ ∙-cong CM.refl xs≋ys - foldr-commMonoid (prep x≈y xs↭ys) = ∙-cong x≈y (foldr-commMonoid xs↭ys) - foldr-commMonoid (swap {xs} {ys} {x} {y} {x′} {y′} x≈x′ y≈y′ xs↭ys) = begin - x ∙ (y ∙ foldr _∙_ ε xs) ≈⟨ ∙-congˡ (∙-congˡ (foldr-commMonoid xs↭ys)) ⟩ - x ∙ (y ∙ foldr _∙_ ε ys) ≈⟨ assoc x y (foldr _∙_ ε ys) ⟨ - (x ∙ y) ∙ foldr _∙_ ε ys ≈⟨ ∙-congʳ (comm x y) ⟩ - (y ∙ x) ∙ foldr _∙_ ε ys ≈⟨ ∙-congʳ (∙-cong y≈y′ x≈x′) ⟩ - (y′ ∙ x′) ∙ foldr _∙_ ε ys ≈⟨ assoc y′ x′ (foldr _∙_ ε ys) ⟩ - y′ ∙ (x′ ∙ foldr _∙_ ε ys) ∎ - where open ≈-Reasoning CM.setoid - foldr-commMonoid (trans xs↭ys ys↭zs) = CM.trans (foldr-commMonoid xs↭ys) (foldr-commMonoid ys↭zs) +-- onIndices-lookup onIndices-lookup : ∀ (xs↭ys : xs ↭ ys) → ∀ i → lookup xs i ≈ lookup ys (Inverse.to (onIndices xs↭ys) i) @@ -453,6 +432,7 @@ onIndices-lookup (swap _ eq xs↭ys) (suc zero) = eq onIndices-lookup (swap _ _ xs↭ys) (suc (suc i)) = onIndices-lookup xs↭ys i onIndices-lookup (trans xs↭ys ys↭zs) i = ≈-trans (onIndices-lookup xs↭ys i) (onIndices-lookup ys↭zs _) + ------------------------------------------------------------------------ -- TOWARDS DEPRECATION ------------------------------------------------------------------------ @@ -514,3 +494,15 @@ split v as bs xs↭as++[v]++bs "Warning: split was deprecated in v2.1. Please use the sharper lemma ↭-split instead." #-} + +-- Version 3.0 + +foldr-commMonoid : ∀ {_∙_ : Op₂ A} {ε : A} → + (isCommutativeMonoid : IsCommutativeMonoid _≈_ _∙_ ε) → + (foldr _∙_ ε) Preserves _↭_ ⟶ _≈_ +foldr-commMonoid isCommutativeMonoid = Foldable.foldr-commMonoid + record { isCommutativeMonoid = isCommutativeMonoid } +{-# WARNING_ON_USAGE foldr-commMonoid +"Warning: foldr-commMonoid was deprecated in v3.0. +Please use Data.List.Effectful.Foldable.foldr-commMonoid instead." +#-} diff --git a/src/Data/Nat/ListAction/Properties.agda b/src/Data/Nat/ListAction/Properties.agda index 90c644c7fb..7a08ef6204 100644 --- a/src/Data/Nat/ListAction/Properties.agda +++ b/src/Data/Nat/ListAction/Properties.agda @@ -13,11 +13,11 @@ module Data.Nat.ListAction.Properties where open import Algebra.Bundles using (CommutativeMonoid) open import Data.List.Base using (List; []; _∷_; _++_; map) +open import Data.List.Effectful.Foldable + using (foldr-commMonoid) open import Data.List.Membership.Propositional using (_∈_) open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭⇒↭ₛ) -open import Data.List.Relation.Binary.Permutation.Setoid.Properties - using (foldr-commMonoid) open import Data.List.Relation.Unary.All using (All; []; _∷_) open import Data.List.Relation.Unary.Any using (here; there) open import Data.Nat.Base using (ℕ; _+_; _*_; _^_; NonZero; _≤_) @@ -62,8 +62,7 @@ sum-++ (m ∷ ms) ns = begin *-distribʳ-sum m (n ∷ ns) = trans (*-distribʳ-+ m n (sum ns)) (cong (n * m +_) (*-distribʳ-sum m ns)) sum-↭ : sum Preserves _↭_ ⟶ _≡_ -sum-↭ p = foldr-commMonoid ℕ-+-0.setoid ℕ-+-0.isCommutativeMonoid (↭⇒↭ₛ p) - where module ℕ-+-0 = CommutativeMonoid +-0-commutativeMonoid +sum-↭ p = foldr-commMonoid +-0-commutativeMonoid (↭⇒↭ₛ p) -- product @@ -93,5 +92,4 @@ product≢0 (n≢0 ∷ ns≢0) = m*n≢0 _ _ {{n≢0}} {{product≢0 ns≢0}} ^-distribʳ-product m (n ∷ ns) = trans (^-distribʳ-* m n (product ns)) (cong (n ^ m *_) (^-distribʳ-product m ns)) product-↭ : product Preserves _↭_ ⟶ _≡_ -product-↭ p = foldr-commMonoid ℕ-*-1.setoid ℕ-*-1.isCommutativeMonoid (↭⇒↭ₛ p) - where module ℕ-*-1 = CommutativeMonoid *-1-commutativeMonoid +product-↭ p = foldr-commMonoid *-1-commutativeMonoid (↭⇒↭ₛ p) From 301b58fb08c68cf2972102c6bb59e34ee5c7ea59 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 22 Jun 2026 07:03:04 +0100 Subject: [PATCH 05/14] refactor: streamline imports and names --- src/Data/List/Effectful/Foldable.agda | 21 +++++++++++-------- .../Binary/Permutation/Setoid/Properties.agda | 2 +- 2 files changed, 13 insertions(+), 10 deletions(-) diff --git a/src/Data/List/Effectful/Foldable.agda b/src/Data/List/Effectful/Foldable.agda index 73a012f814..01d6b0b419 100644 --- a/src/Data/List/Effectful/Foldable.agda +++ b/src/Data/List/Effectful/Foldable.agda @@ -19,8 +19,8 @@ open import Effect.Foldable using (RawFoldableWithDefaults; RawFoldable) open import Function.Base using (_∘_; id) open import Function.Bundles using (Func) open import Function.Construct.Identity using (function) +open import Function.Definitions using (Congruent) open import Level using (Level) -open import Relation.Binary.Definitions using (Monotonic₁) open import Relation.Binary.Bundles using (Setoid) import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; cong) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning @@ -94,15 +94,18 @@ module _ (commutativeMonoid : CommutativeMonoid c ℓ) where using (_∙_; ε; ∙-cong; ∙-congˡ; ∙-congʳ; assoc; comm) open Permutation CM.setoid - foldr-commMonoid : Monotonic₁ _↭_ CM._≈_ (foldr _∙_ ε) + h = foldr _∙_ ε + + foldr-commMonoid : Congruent _↭_ CM._≈_ h foldr-commMonoid (refl xs≋ys) = Pointwise.foldr⁺ ∙-cong CM.refl xs≋ys foldr-commMonoid (prep x≈y xs↭ys) = ∙-cong x≈y (foldr-commMonoid xs↭ys) foldr-commMonoid (swap {xs} {ys} {x} {y} {x′} {y′} x≈x′ y≈y′ xs↭ys) = begin - x ∙ (y ∙ foldr _∙_ ε xs) ≈⟨ ∙-congˡ (∙-congˡ (foldr-commMonoid xs↭ys)) ⟩ - x ∙ (y ∙ foldr _∙_ ε ys) ≈⟨ assoc x y (foldr _∙_ ε ys) ⟨ - (x ∙ y) ∙ foldr _∙_ ε ys ≈⟨ ∙-congʳ (comm x y) ⟩ - (y ∙ x) ∙ foldr _∙_ ε ys ≈⟨ ∙-congʳ (∙-cong y≈y′ x≈x′) ⟩ - (y′ ∙ x′) ∙ foldr _∙_ ε ys ≈⟨ assoc y′ x′ (foldr _∙_ ε ys) ⟩ - y′ ∙ (x′ ∙ foldr _∙_ ε ys) ∎ + x ∙ (y ∙ h xs) ≈⟨ ∙-congˡ (∙-congˡ (foldr-commMonoid xs↭ys)) ⟩ + x ∙ (y ∙ h ys) ≈⟨ assoc x y (h ys) ⟨ + (x ∙ y) ∙ h ys ≈⟨ ∙-congʳ (comm x y) ⟩ + (y ∙ x) ∙ h ys ≈⟨ ∙-congʳ (∙-cong y≈y′ x≈x′) ⟩ + (y′ ∙ x′) ∙ h ys ≈⟨ assoc y′ x′ (h ys) ⟩ + y′ ∙ (x′ ∙ h ys) ∎ where open ≈-Reasoning CM.setoid - foldr-commMonoid (trans xs↭ys ys↭zs) = CM.trans (foldr-commMonoid xs↭ys) (foldr-commMonoid ys↭zs) + foldr-commMonoid (trans xs↭ys ys↭zs) = + CM.trans (foldr-commMonoid xs↭ys) (foldr-commMonoid ys↭zs) diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda index 6f7ba10bde..d7a19e00bb 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda @@ -36,7 +36,7 @@ open import Function.Base using (_∘_; _⟨_⟩_; flip) open import Function.Bundles using (Inverse) open import Level using (Level; _⊔_) open import Relation.Binary.Core - using (Rel; _⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_) + using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_) open import Relation.Binary.Definitions as B hiding (Decidable) open import Relation.Binary.Properties.Setoid S using (≉-resp₂) open import Relation.Binary.PropositionalEquality.Core as ≡ From 9406198a48ff7e81220a3a94988dfda0702b392c Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 22 Jun 2026 07:03:42 +0100 Subject: [PATCH 06/14] fix: uncommitted changes --- src/Data/Bool/ListAction/Properties.agda | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Data/Bool/ListAction/Properties.agda b/src/Data/Bool/ListAction/Properties.agda index 7fd34e8260..aea585f16f 100644 --- a/src/Data/Bool/ListAction/Properties.agda +++ b/src/Data/Bool/ListAction/Properties.agda @@ -12,10 +12,11 @@ open import Data.Bool.Base open import Data.Bool.Properties open import Data.Bool.ListAction open import Data.List.Base hiding (and; or; all; any) +open import Data.List.Effectful.Foldable + using (foldr-commMonoid) open import Data.List.Membership.Propositional using (_∈_) open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭⇒↭ₛ) import Data.List.Relation.Binary.Permutation.Propositional.Properties as ↭ -open import Data.List.Relation.Binary.Permutation.Setoid.Properties open import Data.List.Relation.Unary.Any using (here; there) open import Function.Base using (_∘′_) open import Relation.Binary.Core using (_Preserves_⟶_) @@ -45,7 +46,7 @@ and-++ (b ∷ bs) cs = begin ∨-distribʳ-and b (c ∷ cs) = trans (∨-distribʳ-∧ b c (and cs)) (cong ((c ∨ b) ∧_) (∨-distribʳ-and b cs)) and-↭ : and Preserves _↭_ ⟶ _≡_ -and-↭ p = foldr-commMonoid ≡-setoid ∧-isCommutativeMonoid (↭⇒↭ₛ p) +and-↭ p = foldr-commMonoid ∧-commutativeMonoid (↭⇒↭ₛ p) and-locate : ∀ bs → and bs ≡ false → false ∈ bs and-locate (false ∷ bs) p = here refl @@ -70,7 +71,7 @@ or-++ (b ∷ bs) cs = begin ∧-distribʳ-or b (c ∷ cs) = trans (∧-distribʳ-∨ b c (or cs)) (cong ((c ∧ b) ∨_) (∧-distribʳ-or b cs)) or-↭ : or Preserves _↭_ ⟶ _≡_ -or-↭ p = foldr-commMonoid ≡-setoid ∨-isCommutativeMonoid (↭⇒↭ₛ p) +or-↭ p = foldr-commMonoid ∨-commutativeMonoid (↭⇒↭ₛ p) or-locate : ∀ bs → or bs ≡ true → true ∈ bs or-locate (false ∷ bs) p = there (or-locate bs p) From 85de5125769fd37d27234612d3f20d600085511e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 22 Jun 2026 07:04:04 +0100 Subject: [PATCH 07/14] fix: `CHANGELOG` entry --- CHANGELOG.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 0323a37de1..226b7631e0 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -61,6 +61,13 @@ Minor improvements it now has the implicit parameters of its internal modules lifted out as global `variable`s. +* [Issue #3016](https://github.com/agda/agda-stdlib/issues/3016) + `Data.List.Relation.Binary.Permutation.Setoid.Properties.foldr-commMonoid` + now moves to `Data.List.Effectful.Foldable`, where it better belongs, for + the sake both of the dependency graph, and of incorporating the refactoring + of that module to make use of the addition of `Data.List.Base.foldMap` and + its properties. + Deprecated modules ------------------ From d9f57493037cbbb07d7085e424f1a7f2aaa3c2a7 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 22 Jun 2026 08:12:42 +0100 Subject: [PATCH 08/14] interim: still need to fix up unsolved metavars --- src/Data/List/Effectful/Foldable.agda | 69 +++++++++++++++++++-------- 1 file changed, 50 insertions(+), 19 deletions(-) diff --git a/src/Data/List/Effectful/Foldable.agda b/src/Data/List/Effectful/Foldable.agda index 01d6b0b419..a2b8451b7f 100644 --- a/src/Data/List/Effectful/Foldable.agda +++ b/src/Data/List/Effectful/Foldable.agda @@ -12,6 +12,7 @@ open import Algebra.Bundles using (Monoid; CommutativeMonoid) open import Algebra.Bundles.Raw using (RawMonoid) open import Algebra.Morphism.Structures using (IsMonoidHomomorphism) open import Data.List.Base as List using (List; []; _∷_; _++_; foldr) +open import Data.List.Properties using (foldMap≗foldr∘map) import Data.List.Relation.Binary.Permutation.Setoid as Permutation open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise) @@ -85,27 +86,57 @@ module _ (M : Monoid c ℓ) (f : A → Monoid.Carrier M) where } ------------------------------------------------------------------------ --- for Commutative Monoids, foldr respects Permutation +-- for Commutative Monoids, foldMap and foldr respect Permutation module _ (commutativeMonoid : CommutativeMonoid c ℓ) where private open module CM = CommutativeMonoid commutativeMonoid - using (_∙_; ε; ∙-cong; ∙-congˡ; ∙-congʳ; assoc; comm) - open Permutation CM.setoid - - h = foldr _∙_ ε - - foldr-commMonoid : Congruent _↭_ CM._≈_ h - foldr-commMonoid (refl xs≋ys) = Pointwise.foldr⁺ ∙-cong CM.refl xs≋ys - foldr-commMonoid (prep x≈y xs↭ys) = ∙-cong x≈y (foldr-commMonoid xs↭ys) - foldr-commMonoid (swap {xs} {ys} {x} {y} {x′} {y′} x≈x′ y≈y′ xs↭ys) = begin - x ∙ (y ∙ h xs) ≈⟨ ∙-congˡ (∙-congˡ (foldr-commMonoid xs↭ys)) ⟩ - x ∙ (y ∙ h ys) ≈⟨ assoc x y (h ys) ⟨ - (x ∙ y) ∙ h ys ≈⟨ ∙-congʳ (comm x y) ⟩ - (y ∙ x) ∙ h ys ≈⟨ ∙-congʳ (∙-cong y≈y′ x≈x′) ⟩ - (y′ ∙ x′) ∙ h ys ≈⟨ assoc y′ x′ (h ys) ⟩ - y′ ∙ (x′ ∙ h ys) ∎ - where open ≈-Reasoning CM.setoid - foldr-commMonoid (trans xs↭ys ys↭zs) = - CM.trans (foldr-commMonoid xs↭ys) (foldr-commMonoid ys↭zs) + using (_∙_; ε; setoid; ∙-cong; ∙-congˡ; ∙-congʳ; assoc; comm) + open ≈-Reasoning setoid + + module _ {S : Setoid a r} (F : Func S setoid) where + + open Permutation S renaming (_↭_ to _↭ₛ_) + private + open module F = Func F + f = F.to + h = foldMap CM.rawMonoid f + + + foldMap-commMonoid : Congruent _↭ₛ_ CM._≈_ h + foldMap-commMonoid (refl {xs} {ys} xs≋ys) + rewrite foldMap≗foldr∘map _∙_ ε f xs | foldMap≗foldr∘map _∙_ ε f ys + = Pointwise.foldr⁺ ∙-cong (CM.refl {x = ε})(Pointwise.map⁺ f f (Pointwise.map F.cong xs≋ys)) + foldMap-commMonoid (prep x≈y xs↭ys) = ∙-cong (F.cong x≈y) (foldMap-commMonoid xs↭ys) + foldMap-commMonoid (swap {xs} {ys} {x} {y} {x′} {y′} x≈x′ y≈y′ xs↭ys) = begin + f x ∙ (f y ∙ h xs) ≈⟨ ∙-congˡ (∙-congˡ (foldMap-commMonoid xs↭ys)) ⟩ + f x ∙ (f y ∙ h ys) ≈⟨ assoc (f x) (f y) (h ys) ⟨ + (f x ∙ f y) ∙ h ys ≈⟨ ∙-congʳ (comm (f x) (f y)) ⟩ + (f y ∙ f x) ∙ h ys ≈⟨ ∙-congʳ (∙-cong (F.cong y≈y′) (F.cong x≈x′)) ⟩ + (f y′ ∙ f x′) ∙ h ys ≈⟨ assoc (f y′) (f x′) (h ys) ⟩ + f y′ ∙ (f x′ ∙ h ys) ∎ + foldMap-commMonoid (trans xs↭ys ys↭zs) = + CM.trans (foldMap-commMonoid xs↭ys) (foldMap-commMonoid ys↭zs) + + module _ where + + open Permutation CM.setoid renaming (_↭_ to _↭ₘ_) + + private g = foldr _∙_ ε + + foldr-commMonoid : Congruent _↭ₘ_ CM._≈_ g +{- + foldr-commMonoid = {!foldMap-commMonoid (function CM.setoid)!} +-} + foldr-commMonoid (refl xs≋ys) = Pointwise.foldr⁺ ∙-cong CM.refl xs≋ys + foldr-commMonoid (prep x≈y xs↭ys) = ∙-cong x≈y (foldr-commMonoid xs↭ys) + foldr-commMonoid (swap {xs} {ys} {x} {y} {x′} {y′} x≈x′ y≈y′ xs↭ys) = begin + x ∙ (y ∙ g xs) ≈⟨ ∙-congˡ (∙-congˡ (foldr-commMonoid xs↭ys)) ⟩ + x ∙ (y ∙ g ys) ≈⟨ assoc x y (g ys) ⟨ + (x ∙ y) ∙ g ys ≈⟨ ∙-congʳ (comm x y) ⟩ + (y ∙ x) ∙ g ys ≈⟨ ∙-congʳ (∙-cong y≈y′ x≈x′) ⟩ + (y′ ∙ x′) ∙ g ys ≈⟨ assoc y′ x′ (g ys) ⟩ + y′ ∙ (x′ ∙ g ys) ∎ + foldr-commMonoid (trans xs↭ys ys↭zs) = + CM.trans (foldr-commMonoid xs↭ys) (foldr-commMonoid ys↭zs) From ef43d29fb7281e3cb873bb3ea47ec6f1ba94f7c6 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 22 Jun 2026 17:20:05 +0100 Subject: [PATCH 09/14] fix: corrected notation --- src/Data/List/Relation/Binary/Pointwise.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/List/Relation/Binary/Pointwise.agda b/src/Data/List/Relation/Binary/Pointwise.agda index f43f6ff24b..b30f8b98b9 100644 --- a/src/Data/List/Relation/Binary/Pointwise.agda +++ b/src/Data/List/Relation/Binary/Pointwise.agda @@ -214,10 +214,10 @@ map⁻ {xs = _ ∷ _} {_ ∷ _} f g (r ∷ rs) = r ∷ map⁻ f g rs ------------------------------------------------------------------------ -- foldr -foldr⁺ : ∀ {_•_ : Op₂ A} {_◦_ : Op₂ B} → - (∀ {w x y z} → R w x → R y z → R (w • y) (x ◦ z)) → +foldr⁺ : ∀ {_∙_ : Op₂ A} {_◦_ : Op₂ B} → + (∀ {w x y z} → R w x → R y z → R (w ∙ y) (x ◦ z)) → ∀ {e f} → R e f → Pointwise R xs ys → - R (foldr _•_ e xs) (foldr _◦_ f ys) + R (foldr _∙_ e xs) (foldr _◦_ f ys) foldr⁺ _ e~f [] = e~f foldr⁺ pres e~f (x~y ∷ xs~ys) = pres x~y (foldr⁺ pres e~f xs~ys) From 626578f0ef13394fca99fa52fa1eb12e2ad0fbf0 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 22 Jun 2026 17:20:36 +0100 Subject: [PATCH 10/14] refactor: new property --- src/Data/List/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 0e4212559b..4031845bc7 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -646,7 +646,7 @@ foldr-map f g x (y ∷ xs) = cong (f (g y)) (foldr-map f g x xs) module _ (_∙_ : B → B → B) (ε : B) (f : A → B) where - foldMap≗foldr∘map : foldMap _∙_ ε f ≗ foldr (λ x → f x ∙_) ε + foldMap≗foldr∘map : foldMap _∙_ ε f ≗ foldr _∙_ ε ∘ List.map f foldMap≗foldr∘map [] = refl foldMap≗foldr∘map (x ∷ xs) = cong (f x ∙_) (foldMap≗foldr∘map xs) From bb5a2351cc06ce4fafca8ff10a8fc867a623afec Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 22 Jun 2026 17:21:11 +0100 Subject: [PATCH 11/14] refactor: express old `foldr-commMonoid` in terms of new `foldMap-commMonoid` --- CHANGELOG.md | 11 +++++- src/Data/List/Effectful/Foldable.agda | 50 ++++++++++++--------------- 2 files changed, 33 insertions(+), 28 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 226b7631e0..1b770ab4c2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -183,9 +183,18 @@ Additions to existing modules foldMap : (B → B → B) → B → (A → B) → List A → B ``` +* In `Data.List.Effectful.Foldable`: + for `CM : CommutativeMonoid`, `S : Setoid`, `F: Func S CM.setoid`, + ```agda + foldMap-commMonoid : Congruent _↭ₛ_ CM._≈_ (foldMap CM.rawMonoid F.to) + foldr-commMonoid : Congruent _↭ₘ_ CM._≈_ (foldr _∙_ ε) + ``` + where `_↭ₛ_` is the `Permutation` relation on `S`, and `_↭ₘ_` the `Permutation` + relation on `CM.setoid`. + * In `Data.List.Properties`: ```agda - foldMap≗foldr∘map : foldMap _∙_ ε f ≗ foldr (λ x → f x ∙_) ε + foldMap≗foldr∘map : foldMap _∙_ ε f ≗ foldr _∙_ ε (map f) ``` * In `Data.Nat.GCD`: diff --git a/src/Data/List/Effectful/Foldable.agda b/src/Data/List/Effectful/Foldable.agda index a2b8451b7f..db1ccb969e 100644 --- a/src/Data/List/Effectful/Foldable.agda +++ b/src/Data/List/Effectful/Foldable.agda @@ -12,18 +12,18 @@ open import Algebra.Bundles using (Monoid; CommutativeMonoid) open import Algebra.Bundles.Raw using (RawMonoid) open import Algebra.Morphism.Structures using (IsMonoidHomomorphism) open import Data.List.Base as List using (List; []; _∷_; _++_; foldr) -open import Data.List.Properties using (foldMap≗foldr∘map) +open import Data.List.Properties using (map-id; foldMap≗foldr∘map) import Data.List.Relation.Binary.Permutation.Setoid as Permutation open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise) open import Effect.Foldable using (RawFoldableWithDefaults; RawFoldable) -open import Function.Base using (_∘_; id) +open import Function.Base using (_∘_; id; _$_) open import Function.Bundles using (Func) -open import Function.Construct.Identity using (function) +import Function.Construct.Identity as Identity using (function) open import Function.Definitions using (Congruent) open import Level using (Level) open import Relation.Binary.Bundles using (Setoid) -import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; cong) +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning private @@ -95,19 +95,25 @@ module _ (commutativeMonoid : CommutativeMonoid c ℓ) where using (_∙_; ε; setoid; ∙-cong; ∙-congˡ; ∙-congʳ; assoc; comm) open ≈-Reasoning setoid - module _ {S : Setoid a r} (F : Func S setoid) where +-- foldMap + + module _ {S : Setoid c r} (F : Func S setoid) where open Permutation S renaming (_↭_ to _↭ₛ_) private + open module S = Setoid S open module F = Func F f = F.to h = foldMap CM.rawMonoid f foldMap-commMonoid : Congruent _↭ₛ_ CM._≈_ h + foldMap-commMonoid (refl {xs} {ys} xs≋ys) rewrite foldMap≗foldr∘map _∙_ ε f xs | foldMap≗foldr∘map _∙_ ε f ys - = Pointwise.foldr⁺ ∙-cong (CM.refl {x = ε})(Pointwise.map⁺ f f (Pointwise.map F.cong xs≋ys)) + = Pointwise.foldr⁺ {R = CM._≈_} ∙-cong (CM.refl {x = ε}) $ + (Pointwise.map⁺ f f (Pointwise.map F.cong xs≋ys)) + foldMap-commMonoid (prep x≈y xs↭ys) = ∙-cong (F.cong x≈y) (foldMap-commMonoid xs↭ys) foldMap-commMonoid (swap {xs} {ys} {x} {y} {x′} {y′} x≈x′ y≈y′ xs↭ys) = begin f x ∙ (f y ∙ h xs) ≈⟨ ∙-congˡ (∙-congˡ (foldMap-commMonoid xs↭ys)) ⟩ @@ -116,27 +122,17 @@ module _ (commutativeMonoid : CommutativeMonoid c ℓ) where (f y ∙ f x) ∙ h ys ≈⟨ ∙-congʳ (∙-cong (F.cong y≈y′) (F.cong x≈x′)) ⟩ (f y′ ∙ f x′) ∙ h ys ≈⟨ assoc (f y′) (f x′) (h ys) ⟩ f y′ ∙ (f x′ ∙ h ys) ∎ + foldMap-commMonoid (trans xs↭ys ys↭zs) = CM.trans (foldMap-commMonoid xs↭ys) (foldMap-commMonoid ys↭zs) - module _ where - - open Permutation CM.setoid renaming (_↭_ to _↭ₘ_) - - private g = foldr _∙_ ε - - foldr-commMonoid : Congruent _↭ₘ_ CM._≈_ g -{- - foldr-commMonoid = {!foldMap-commMonoid (function CM.setoid)!} --} - foldr-commMonoid (refl xs≋ys) = Pointwise.foldr⁺ ∙-cong CM.refl xs≋ys - foldr-commMonoid (prep x≈y xs↭ys) = ∙-cong x≈y (foldr-commMonoid xs↭ys) - foldr-commMonoid (swap {xs} {ys} {x} {y} {x′} {y′} x≈x′ y≈y′ xs↭ys) = begin - x ∙ (y ∙ g xs) ≈⟨ ∙-congˡ (∙-congˡ (foldr-commMonoid xs↭ys)) ⟩ - x ∙ (y ∙ g ys) ≈⟨ assoc x y (g ys) ⟨ - (x ∙ y) ∙ g ys ≈⟨ ∙-congʳ (comm x y) ⟩ - (y ∙ x) ∙ g ys ≈⟨ ∙-congʳ (∙-cong y≈y′ x≈x′) ⟩ - (y′ ∙ x′) ∙ g ys ≈⟨ assoc y′ x′ (g ys) ⟩ - y′ ∙ (x′ ∙ g ys) ∎ - foldr-commMonoid (trans xs↭ys ys↭zs) = - CM.trans (foldr-commMonoid xs↭ys) (foldr-commMonoid ys↭zs) +-- foldr + + open Permutation CM.setoid renaming (_↭_ to _↭ₘ_) + + foldr-commMonoid : Congruent _↭ₘ_ CM._≈_ (foldr _∙_ ε) + foldr-commMonoid {x = xs} {y = ys} + rewrite ≡.sym (map-id xs) | ≡.sym (map-id ys) + rewrite ≡.sym (foldMap≗foldr∘map _∙_ ε id xs) | ≡.sym (foldMap≗foldr∘map _∙_ ε id ys) + rewrite map-id xs | map-id ys + = foldMap-commMonoid $ Identity.function CM.setoid From c2cf9e2fbca1e267777d417dfa9b97f77c790e5c Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 22 Jun 2026 17:22:18 +0100 Subject: [PATCH 12/14] fix: whitespace --- src/Data/List/Effectful/Foldable.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/List/Effectful/Foldable.agda b/src/Data/List/Effectful/Foldable.agda index db1ccb969e..ae5a584aac 100644 --- a/src/Data/List/Effectful/Foldable.agda +++ b/src/Data/List/Effectful/Foldable.agda @@ -98,20 +98,20 @@ module _ (commutativeMonoid : CommutativeMonoid c ℓ) where -- foldMap module _ {S : Setoid c r} (F : Func S setoid) where - + open Permutation S renaming (_↭_ to _↭ₛ_) private open module S = Setoid S open module F = Func F f = F.to h = foldMap CM.rawMonoid f - + foldMap-commMonoid : Congruent _↭ₛ_ CM._≈_ h foldMap-commMonoid (refl {xs} {ys} xs≋ys) rewrite foldMap≗foldr∘map _∙_ ε f xs | foldMap≗foldr∘map _∙_ ε f ys - = Pointwise.foldr⁺ {R = CM._≈_} ∙-cong (CM.refl {x = ε}) $ + = Pointwise.foldr⁺ {R = CM._≈_} ∙-cong (CM.refl {x = ε}) $ (Pointwise.map⁺ f f (Pointwise.map F.cong xs≋ys)) foldMap-commMonoid (prep x≈y xs↭ys) = ∙-cong (F.cong x≈y) (foldMap-commMonoid xs↭ys) From 674b3b2a753e149e28fca8d99efb638da2c1027a Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 22 Jun 2026 17:26:50 +0100 Subject: [PATCH 13/14] refactor: rename accoridng to Jacques' suggestions --- CHANGELOG.md | 6 ++--- src/Data/List/Effectful/Foldable.agda | 22 +++++++++---------- .../Binary/Permutation/Setoid/Properties.agda | 4 ++-- 3 files changed, 16 insertions(+), 16 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 1b770ab4c2..282a60ff79 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -95,7 +95,7 @@ Deprecated names * In `Data.List.Relation.Binary.Permutation.Setoid.Properties`: ```agda - foldr-commMonoid ↦ Data.List.Effectful.Foldable.foldr-commMonoid + foldr-commMonoid ↦ Data.List.Effectful.Foldable.foldr-congruent ``` * In `Data.Nat.GCD`: @@ -186,8 +186,8 @@ Additions to existing modules * In `Data.List.Effectful.Foldable`: for `CM : CommutativeMonoid`, `S : Setoid`, `F: Func S CM.setoid`, ```agda - foldMap-commMonoid : Congruent _↭ₛ_ CM._≈_ (foldMap CM.rawMonoid F.to) - foldr-commMonoid : Congruent _↭ₘ_ CM._≈_ (foldr _∙_ ε) + foldMap-congruent : Congruent _↭ₛ_ CM._≈_ (foldMap CM.rawMonoid F.to) + foldr-congruent : Congruent _↭ₘ_ CM._≈_ (foldr _∙_ ε) ``` where `_↭ₛ_` is the `Permutation` relation on `S`, and `_↭ₘ_` the `Permutation` relation on `CM.setoid`. diff --git a/src/Data/List/Effectful/Foldable.agda b/src/Data/List/Effectful/Foldable.agda index ae5a584aac..1419621c6b 100644 --- a/src/Data/List/Effectful/Foldable.agda +++ b/src/Data/List/Effectful/Foldable.agda @@ -106,33 +106,33 @@ module _ (commutativeMonoid : CommutativeMonoid c ℓ) where f = F.to h = foldMap CM.rawMonoid f + foldMap-congruent : Congruent _↭ₛ_ CM._≈_ h - foldMap-commMonoid : Congruent _↭ₛ_ CM._≈_ h - - foldMap-commMonoid (refl {xs} {ys} xs≋ys) + foldMap-congruent (refl {xs} {ys} xs≋ys) rewrite foldMap≗foldr∘map _∙_ ε f xs | foldMap≗foldr∘map _∙_ ε f ys = Pointwise.foldr⁺ {R = CM._≈_} ∙-cong (CM.refl {x = ε}) $ (Pointwise.map⁺ f f (Pointwise.map F.cong xs≋ys)) - foldMap-commMonoid (prep x≈y xs↭ys) = ∙-cong (F.cong x≈y) (foldMap-commMonoid xs↭ys) - foldMap-commMonoid (swap {xs} {ys} {x} {y} {x′} {y′} x≈x′ y≈y′ xs↭ys) = begin - f x ∙ (f y ∙ h xs) ≈⟨ ∙-congˡ (∙-congˡ (foldMap-commMonoid xs↭ys)) ⟩ + foldMap-congruent (prep x≈y xs↭ys) = ∙-cong (F.cong x≈y) (foldMap-congruent xs↭ys) + + foldMap-congruent (swap {xs} {ys} {x} {y} {x′} {y′} x≈x′ y≈y′ xs↭ys) = begin + f x ∙ (f y ∙ h xs) ≈⟨ ∙-congˡ (∙-congˡ (foldMap-congruent xs↭ys)) ⟩ f x ∙ (f y ∙ h ys) ≈⟨ assoc (f x) (f y) (h ys) ⟨ (f x ∙ f y) ∙ h ys ≈⟨ ∙-congʳ (comm (f x) (f y)) ⟩ (f y ∙ f x) ∙ h ys ≈⟨ ∙-congʳ (∙-cong (F.cong y≈y′) (F.cong x≈x′)) ⟩ (f y′ ∙ f x′) ∙ h ys ≈⟨ assoc (f y′) (f x′) (h ys) ⟩ f y′ ∙ (f x′ ∙ h ys) ∎ - foldMap-commMonoid (trans xs↭ys ys↭zs) = - CM.trans (foldMap-commMonoid xs↭ys) (foldMap-commMonoid ys↭zs) + foldMap-congruent (trans xs↭ys ys↭zs) = + CM.trans (foldMap-congruent xs↭ys) (foldMap-congruent ys↭zs) -- foldr open Permutation CM.setoid renaming (_↭_ to _↭ₘ_) - foldr-commMonoid : Congruent _↭ₘ_ CM._≈_ (foldr _∙_ ε) - foldr-commMonoid {x = xs} {y = ys} + foldr-congruent : Congruent _↭ₘ_ CM._≈_ (foldr _∙_ ε) + foldr-congruent {x = xs} {y = ys} rewrite ≡.sym (map-id xs) | ≡.sym (map-id ys) rewrite ≡.sym (foldMap≗foldr∘map _∙_ ε id xs) | ≡.sym (foldMap≗foldr∘map _∙_ ε id ys) rewrite map-id xs | map-id ys - = foldMap-commMonoid $ Identity.function CM.setoid + = foldMap-congruent $ Identity.function CM.setoid diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda index d7a19e00bb..be730a144d 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda @@ -500,9 +500,9 @@ Please use the sharper lemma ↭-split instead." foldr-commMonoid : ∀ {_∙_ : Op₂ A} {ε : A} → (isCommutativeMonoid : IsCommutativeMonoid _≈_ _∙_ ε) → (foldr _∙_ ε) Preserves _↭_ ⟶ _≈_ -foldr-commMonoid isCommutativeMonoid = Foldable.foldr-commMonoid +foldr-commMonoid isCommutativeMonoid = Foldable.foldr-congruent record { isCommutativeMonoid = isCommutativeMonoid } {-# WARNING_ON_USAGE foldr-commMonoid "Warning: foldr-commMonoid was deprecated in v3.0. -Please use Data.List.Effectful.Foldable.foldr-commMonoid instead." +Please use Data.List.Effectful.Foldable.foldr-congruent instead." #-} From 0f446e92f3fa743024deb924d79d00112f3b1449 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 22 Jun 2026 17:34:53 +0100 Subject: [PATCH 14/14] fix: knock-on name changes --- src/Data/Bool/ListAction/Properties.agda | 6 +++--- src/Data/Nat/ListAction/Properties.agda | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Data/Bool/ListAction/Properties.agda b/src/Data/Bool/ListAction/Properties.agda index aea585f16f..82d44a2672 100644 --- a/src/Data/Bool/ListAction/Properties.agda +++ b/src/Data/Bool/ListAction/Properties.agda @@ -13,7 +13,7 @@ open import Data.Bool.Properties open import Data.Bool.ListAction open import Data.List.Base hiding (and; or; all; any) open import Data.List.Effectful.Foldable - using (foldr-commMonoid) + using (foldr-congruent) open import Data.List.Membership.Propositional using (_∈_) open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭⇒↭ₛ) import Data.List.Relation.Binary.Permutation.Propositional.Properties as ↭ @@ -46,7 +46,7 @@ and-++ (b ∷ bs) cs = begin ∨-distribʳ-and b (c ∷ cs) = trans (∨-distribʳ-∧ b c (and cs)) (cong ((c ∨ b) ∧_) (∨-distribʳ-and b cs)) and-↭ : and Preserves _↭_ ⟶ _≡_ -and-↭ p = foldr-commMonoid ∧-commutativeMonoid (↭⇒↭ₛ p) +and-↭ p = foldr-congruent ∧-commutativeMonoid (↭⇒↭ₛ p) and-locate : ∀ bs → and bs ≡ false → false ∈ bs and-locate (false ∷ bs) p = here refl @@ -71,7 +71,7 @@ or-++ (b ∷ bs) cs = begin ∧-distribʳ-or b (c ∷ cs) = trans (∧-distribʳ-∨ b c (or cs)) (cong ((c ∧ b) ∨_) (∧-distribʳ-or b cs)) or-↭ : or Preserves _↭_ ⟶ _≡_ -or-↭ p = foldr-commMonoid ∨-commutativeMonoid (↭⇒↭ₛ p) +or-↭ p = foldr-congruent ∨-commutativeMonoid (↭⇒↭ₛ p) or-locate : ∀ bs → or bs ≡ true → true ∈ bs or-locate (false ∷ bs) p = there (or-locate bs p) diff --git a/src/Data/Nat/ListAction/Properties.agda b/src/Data/Nat/ListAction/Properties.agda index 7a08ef6204..4e148c12aa 100644 --- a/src/Data/Nat/ListAction/Properties.agda +++ b/src/Data/Nat/ListAction/Properties.agda @@ -14,7 +14,7 @@ module Data.Nat.ListAction.Properties where open import Algebra.Bundles using (CommutativeMonoid) open import Data.List.Base using (List; []; _∷_; _++_; map) open import Data.List.Effectful.Foldable - using (foldr-commMonoid) + using (foldr-congruent) open import Data.List.Membership.Propositional using (_∈_) open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭⇒↭ₛ) @@ -62,7 +62,7 @@ sum-++ (m ∷ ms) ns = begin *-distribʳ-sum m (n ∷ ns) = trans (*-distribʳ-+ m n (sum ns)) (cong (n * m +_) (*-distribʳ-sum m ns)) sum-↭ : sum Preserves _↭_ ⟶ _≡_ -sum-↭ p = foldr-commMonoid +-0-commutativeMonoid (↭⇒↭ₛ p) +sum-↭ p = foldr-congruent +-0-commutativeMonoid (↭⇒↭ₛ p) -- product @@ -92,4 +92,4 @@ product≢0 (n≢0 ∷ ns≢0) = m*n≢0 _ _ {{n≢0}} {{product≢0 ns≢0}} ^-distribʳ-product m (n ∷ ns) = trans (^-distribʳ-* m n (product ns)) (cong (n ^ m *_) (^-distribʳ-product m ns)) product-↭ : product Preserves _↭_ ⟶ _≡_ -product-↭ p = foldr-commMonoid *-1-commutativeMonoid (↭⇒↭ₛ p) +product-↭ p = foldr-congruent *-1-commutativeMonoid (↭⇒↭ₛ p)