[ add ] Data.List.Base.foldMap and refactor

CHANGELOG.md

@@ -136,6 +136,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
 ------------------
 
@@ -181,6 +188,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-congruent
+  ```
+
 * In `Data.Nat.GCD`:
   ```agda
   gcd[0,0]≡0 ↦ gcd[n,n]≡n
@@ -342,6 +354,20 @@ 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.List.Effectful.Foldable`:
+  for `CM : CommutativeMonoid`, `S : Setoid`, `F: Func S CM.setoid`,
+  ```agda
+  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`.
+
 * In `Data.List.Membership.Propositional.Properties`:
   ```agda
   foldl-selective : Selective _≡_ _•_ → ∀ e xs →
@@ -353,6 +379,10 @@ Additions to existing modules
   foldl-selective : Selective _≈_ _•_ → ∀ e xs →
                     (foldl _•_ e xs ≈ e) ⊎ (foldl _•_ e xs ∈ xs)
    ```
+* In `Data.List.Properties`:
+  ```agda
+  foldMap≗foldr∘map : foldMap _∙_ ε f ≗ foldr _∙_ ε (map f)
+  ```
 
 * In `Data.List.Relation.Ternary.Appending.Setoid.Properties`:
   ```agda

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-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 ↭
-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-congruent ∧-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-congruent ∨-commutativeMonoid (↭⇒↭ₛ p)
 
 or-locate : ∀ bs → or bs ≡ true → true ∈ bs
 or-locate (false ∷ bs) p = there (or-locate bs p)

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)

src/Data/List/Effectful/Foldable.agda

@@ -8,18 +8,27 @@
 
 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)
+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)
+import Function.Construct.Identity as Identity using (function)
+open import Function.Definitions using (Congruent)
 open import Level using (Level)
-import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; cong)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 private
   variable
-    a c ℓ : Level
+    a c r ℓ : Level
     A : Set a
 
 ------------------------------------------------------------------------
@@ -30,8 +39,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
@@ -51,7 +59,7 @@ foldable = record
   }
 
 ------------------------------------------------------------------------
--- Properties
+-- foldMap gives rise to a Monoid homomorphism
 
 module _ (M : Monoid c ℓ) (f : A → Monoid.Carrier M) where
 
@@ -76,3 +84,55 @@ module _ (M : Monoid c ℓ) (f : A → Monoid.Carrier M) where
       }
     ; ε-homo = []-homo
     }
+
+------------------------------------------------------------------------
+-- for Commutative Monoids, foldMap and foldr respect Permutation
+
+module _ (commutativeMonoid : CommutativeMonoid c ℓ) where
+
+  private
+    open module CM = CommutativeMonoid commutativeMonoid
+      using (_∙_; ε; setoid; ∙-cong; ∙-congˡ; ∙-congʳ; assoc; comm)
+  open ≈-Reasoning setoid
+
+-- 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-congruent : Congruent _↭ₛ_ CM._≈_ h
+
+    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-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-congruent (trans xs↭ys ys↭zs) =
+      CM.trans (foldMap-congruent xs↭ys) (foldMap-congruent ys↭zs)
+
+-- foldr
+
+  open Permutation CM.setoid renaming (_↭_ to _↭ₘ_)
+
+  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-congruent $ Identity.function CM.setoid

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 _∙_ ε ∘ List.map f
+  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

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-congruent
+  record { isCommutativeMonoid = isCommutativeMonoid }
+{-# WARNING_ON_USAGE foldr-commMonoid
+"Warning: foldr-commMonoid was deprecated in v3.0.
+Please use Data.List.Effectful.Foldable.foldr-congruent instead."
+#-}

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)
 

src/Data/Nat/ListAction/Properties.agda

@@ -13,13 +13,13 @@ module Data.Nat.ListAction.Properties where
 
 open import Algebra.Bundles using (CommutativeMonoid)
 open import Data.List.Base using (List; []; _∷_; _++_; map; foldl)
+open import Data.List.Effectful.Foldable
+  using (foldr-congruent)
 open import Data.List.Membership.Propositional using (_∈_)
 import Data.List.Properties as Listₚ
 import Data.List.Membership.Propositional.Properties as ∈ₚ
 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 as Any using (here; there)
 
@@ -68,8 +68,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-congruent +-0-commutativeMonoid (↭⇒↭ₛ p)
 
 
 -- product
@@ -104,9 +103,7 @@ 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-congruent *-1-commutativeMonoid (↭⇒↭ₛ p)
 
 -- minimum