[ refactor ] Add Data.Nat.SumAndProduct

doc/README/Data/List.agda

@@ -7,6 +7,7 @@
 module README.Data.List where
 
 open import Data.Nat.Base using (ℕ; _+_)
+open import Data.Nat.SumAndProduct using (sum)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 
 ------------------------------------------------------------------------
@@ -18,7 +19,7 @@ open import Data.List
   using
   (List
   ; []; _∷_
-  ; sum; map; take; reverse; _++_; drop
+  ; map; take; reverse; _++_; drop
   )
 
 -- Lists are built using the "[]" and "_∷_" constructors.

src/Data/List/Base.agda

@@ -16,7 +16,7 @@ open import Data.Bool.Base as Bool
   using (Bool; false; true; not; _∧_; _∨_; if_then_else_)
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe′)
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_; _*_ ; _≤_ ; s≤s)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 open import Data.Product.Base as Product using (_×_; _,_; map₁; map₂′)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Data.These.Base as These using (These; this; that; these)
@@ -162,12 +162,6 @@ any p = or ∘ map p
 all : (A → Bool) → List A → Bool
 all p = and ∘ map p
 
-sum : List ℕ → ℕ
-sum = foldr _+_ 0
-
-product : List ℕ → ℕ
-product = foldr _*_ 1
-
 length : List A → ℕ
 length = foldr (const suc) 0
 
@@ -580,3 +574,20 @@ scanl f e (x ∷ xs) = e ∷ scanl f (f e x) xs
 "Warning: scanl was deprecated in v2.1.
 Please use Data.List.Scans.Base.scanl instead."
 #-}
+
+-- Version 2.3
+
+sum : List ℕ → ℕ
+sum = foldr ℕ._+_ 0
+{-# WARNING_ON_USAGE sum
+"Warning: sum was deprecated in v2.3.
+Please use Data.Nat.SumAndProduct.sum instead."
+#-}
+
+product : List ℕ → ℕ
+product = foldr ℕ._*_ 1
+{-# WARNING_ON_USAGE product
+"Warning: product was deprecated in v2.3.
+Please use Data.Nat.SumAndProduct.product instead."
+#-}
+

src/Data/List/Properties.agda

@@ -21,13 +21,11 @@ import Algebra.Structures as AlgebraicStructures
 open import Data.Bool.Base using (Bool; false; true; not; if_then_else_)
 open import Data.Fin.Base using (Fin; zero; suc; cast; toℕ)
 open import Data.List.Base as List
-open import Data.List.Membership.Propositional using (_∈_)
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
 open import Data.Maybe.Relation.Unary.Any using (just) renaming (Any to MAny)
 open import Data.Nat.Base
-open import Data.Nat.Divisibility using (_∣_; divides; ∣n⇒∣m*n)
 open import Data.Nat.Properties
 open import Data.Product.Base as Product
   using (_×_; _,_; uncurry; uncurry′; proj₁; proj₂; <_,_>)
@@ -829,34 +827,6 @@ mapMaybeIsInj₂∘mapInj₂ = mapMaybe-map-retract λ _ → refl
 mapMaybeIsInj₂∘mapInj₁ : (xs : List A) → mapMaybe (isInj₂ {B = B}) (map inj₁ xs) ≡ []
 mapMaybeIsInj₂∘mapInj₁ = mapMaybe-map-none λ _ → refl
 
-------------------------------------------------------------------------
--- sum
-
-sum-++ : ∀ xs ys → sum (xs ++ ys) ≡ sum xs + sum ys
-sum-++ []       ys = refl
-sum-++ (x ∷ xs) ys = begin
-  x + sum (xs ++ ys)     ≡⟨ cong (x +_) (sum-++ xs ys) ⟩
-  x + (sum xs + sum ys)  ≡⟨ sym (+-assoc x _ _) ⟩
-  (x + sum xs) + sum ys  ∎
-
-------------------------------------------------------------------------
--- product
-
-∈⇒∣product : ∀ {n ns} → n ∈ ns → n ∣ product ns
-∈⇒∣product {n} {n ∷ ns} (here  refl) = divides (product ns) (*-comm n (product ns))
-∈⇒∣product {n} {m ∷ ns} (there n∈ns) = ∣n⇒∣m*n m (∈⇒∣product n∈ns)
-
-product≢0 : ∀ {ns} → All NonZero ns → NonZero (product ns)
-product≢0 [] = _
-product≢0 {n ∷ ns} (n≢0 ∷ ns≢0) = m*n≢0 n (product ns) {{n≢0}} {{product≢0 ns≢0}}
-
-∈⇒≤product : ∀ {n ns} → All NonZero ns → n ∈ ns → n ≤ product ns
-∈⇒≤product {ns = n ∷ ns} (_ ∷ ns≢0) (here refl) =
-  m≤m*n n (product ns) {{product≢0 ns≢0}}
-∈⇒≤product {ns = n ∷ _} (n≢0 ∷ ns≢0) (there n∈ns) =
-  m≤n⇒m≤o*n n {{n≢0}} (∈⇒≤product ns≢0 n∈ns)
-
-
 ------------------------------------------------------------------------
 -- applyUpTo
 
@@ -1534,7 +1504,7 @@ module _ (f : A → B) where
 
 
 ------------------------------------------------------------------------
--- DEPRECATED
+-- DEPRECATED NAMES
 ------------------------------------------------------------------------
 -- Please use the new names as continuing support for the old names is
 -- not guaranteed.
@@ -1565,12 +1535,6 @@ map-++-commute = map-++
 Please use map-++ instead."
 #-}
 
-sum-++-commute = sum-++
-{-# WARNING_ON_USAGE sum-++-commute
-"Warning: map-++-commute was deprecated in v2.0.
-Please use map-++ instead."
-#-}
-
 reverse-map-commute = reverse-map
 {-# WARNING_ON_USAGE reverse-map-commute
 "Warning: reverse-map-commute was deprecated in v2.0.
@@ -1658,3 +1622,50 @@ concat-[-] = concat-map-[_]
 "Warning: concat-[-] was deprecated in v2.2.
 Please use concat-map-[_] instead."
 #-}
+
+-- Version 2.3
+
+sum-++ : ∀ xs ys → sum (xs ++ ys) ≡ sum xs + sum ys
+sum-++ []       ys = refl
+sum-++ (x ∷ xs) ys = begin
+  x + sum (xs ++ ys)     ≡⟨ cong (x +_) (sum-++ xs ys) ⟩
+  x + (sum xs + sum ys)  ≡⟨ +-assoc x _ _ ⟨
+  (x + sum xs) + sum ys  ∎
+{-# WARNING_ON_USAGE sum-++
+"Warning: sum-++ was deprecated in v2.3.
+Please use Data.Nat.SumAndProperties.sum-++ instead."
+#-}
+sum-++-commute = sum-++
+{-# WARNING_ON_USAGE sum-++-commute
+"Warning: sum-++-commute was deprecated in v2.0.
+Please use Data.Nat.SumAndProperties.sum-++ instead."
+#-}
+
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.Nat.Divisibility using (_∣_; m∣m*n; ∣n⇒∣m*n)
+
+∈⇒∣product : ∀ {n ns} → n ∈ ns → n ∣ product ns
+∈⇒∣product {ns = n ∷ ns} (here  refl) = m∣m*n (product ns)
+∈⇒∣product {ns = m ∷ ns} (there n∈ns) = ∣n⇒∣m*n m (∈⇒∣product n∈ns)
+{-# WARNING_ON_USAGE ∈⇒∣product
+"Warning: ∈⇒∣product was deprecated in v2.3.
+Please use Data.Nat.SumAndProperties.∈⇒∣product instead."
+#-}
+
+product≢0 : ∀ {ns} → All NonZero ns → NonZero (product ns)
+product≢0 [] = _
+product≢0 {n ∷ ns} (n≢0 ∷ ns≢0) = m*n≢0 n (product ns) {{n≢0}} {{product≢0 ns≢0}}
+{-# WARNING_ON_USAGE product≢0
+"Warning: product≢0 was deprecated in v2.3.
+Please use Data.Nat.SumAndProperties.product≢0 instead."
+#-}
+
+∈⇒≤product : ∀ {n ns} → All NonZero ns → n ∈ ns → n ≤ product ns
+∈⇒≤product {ns = n ∷ ns} (_ ∷ ns≢0) (here refl) =
+  m≤m*n n (product ns) {{product≢0 ns≢0}}
+∈⇒≤product {ns = n ∷ _} (n≢0 ∷ ns≢0) (there n∈ns) =
+  m≤n⇒m≤o*n n {{n≢0}} (∈⇒≤product ns≢0 n∈ns)
+{-# WARNING_ON_USAGE ∈⇒≤product
+"Warning: ∈⇒≤product was deprecated in v2.3.
+Please use Data.Nat.SumAndProperties.∈⇒≤product instead."
+#-}

src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda

@@ -15,7 +15,7 @@ open import Data.Bool.Base using (Bool; true; false)
 open import Data.Nat.Base using (ℕ; suc)
 import Data.Nat.Properties as ℕ
 open import Data.Product.Base using (-,_)
-open import Data.List.Base as List
+open import Data.List.Base as List hiding (sum; product)
 open import Data.List.Relation.Binary.Permutation.Propositional
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
@@ -372,24 +372,6 @@ module _ {ℓ} {R : Rel A ℓ} (R? : Decidable R) where
     x ∷ xs ++ y ∷ ys         ∎
     where open PermutationReasoning
 
-------------------------------------------------------------------------
--- sum
-
-sum-↭ : sum Preserves _↭_ ⟶ _≡_
-sum-↭ p = foldr-commMonoid ℕ-+-0.isCommutativeMonoid (↭⇒↭ₛ p)
-  where
-  module ℕ-+-0 = CommutativeMonoid ℕ.+-0-commutativeMonoid
-  open Permutation ℕ-+-0.setoid
-
-------------------------------------------------------------------------
--- product
-
-product-↭ : product Preserves _↭_ ⟶ _≡_
-product-↭ p = foldr-commMonoid ℕ-*-1.isCommutativeMonoid (↭⇒↭ₛ p)
-  where
-  module ℕ-*-1 = CommutativeMonoid ℕ.*-1-commutativeMonoid
-  open Permutation ℕ-*-1.setoid
-
 ------------------------------------------------------------------------
 -- catMaybes
 
@@ -408,3 +390,25 @@ catMaybes-↭ (swap (just x) (just y) xs↭) = swap x y $ catMaybes-↭ xs↭
 
 mapMaybe-↭ : (f : A → Maybe B) → xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys
 mapMaybe-↭ f = catMaybes-↭ ∘ map⁺ f
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.3
+
+import Data.Nat.SumAndProduct as ℕ
+
+sum-↭ = ℕ.sum-↭
+{-# WARNING_ON_USAGE sum-↭
+"Warning: sum-↭ was deprecated in v2.3.
+Please use Data.Nat.SumAndProduct.sum-↭ instead."
+#-}
+product-↭ = ℕ.product-↭
+{-# WARNING_ON_USAGE product-↭
+"Warning: product-↭ was deprecated in v2.3.
+Please use Data.Nat.SumAndProduct.product-↭ instead."
+#-}

src/Data/Nat/Primality.agda

@@ -8,13 +8,13 @@
 
 module Data.Nat.Primality where
 
-open import Data.List.Base using ([]; _∷_; product)
-open import Data.List.Properties using (product≢0)
+open import Data.List.Base using ([]; _∷_)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.Nat.Base
 open import Data.Nat.Divisibility
 open import Data.Nat.GCD using (module GCD; module Bézout)
 open import Data.Nat.Properties
+open import Data.Nat.SumAndProduct using (product; product≢0)
 open import Data.Product.Base using (∃-syntax; _×_; map₂; _,_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (flip; _∘_; _∘′_)

src/Data/Nat/Primality/Factorisation.agda

@@ -17,16 +17,17 @@ open import Data.Nat.Induction using (<-Rec; <-rec; <-recBuilder)
 open import Data.Nat.Primality
   using (Prime; _Rough_; rough∧square>⇒prime; ∤⇒rough-suc; rough∧∣⇒rough; rough∧∣⇒prime;
          2-rough; euclidsLemma; prime⇒irreducible; ¬prime[1]; productOfPrimes≥1; prime⇒nonZero)
+open import Data.Nat.SumAndProduct using (product; product-↭)
 open import Data.Product.Base using (∃-syntax; _×_; _,_; proj₁; proj₂)
-open import Data.List.Base using (List; []; _∷_; _++_; product)
+open import Data.List.Base using (List; []; _∷_; _++_)
 open import Data.List.Membership.Propositional using (_∈_)
 open import Data.List.Membership.Propositional.Properties using (∈-∃++)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any using (here; there)
 open import Data.List.Relation.Binary.Permutation.Propositional
-  using (_↭_; prep; swap; ↭-reflexive; ↭-refl; ↭-trans; refl; module PermutationReasoning)
+  using (_↭_; ↭-reflexive; ↭-refl; ↭-trans; module PermutationReasoning)
 open import Data.List.Relation.Binary.Permutation.Propositional.Properties
-  using (product-↭; All-resp-↭; shift)
+  using (All-resp-↭; shift)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (_$_; _∘_; _|>_; flip)
 open import Induction using (build)
@@ -146,7 +147,7 @@ factorisationHasAllPrimeFactors {a ∷ as} {p} pPrime p∣aΠas (aPrime ∷ asPr
 
 private
   factorisationUnique′ : (as bs : List ℕ) → product as ≡ product bs → All Prime as → All Prime bs → as ↭ bs
-  factorisationUnique′ [] [] Πas≡Πbs asPrime bsPrime = refl
+  factorisationUnique′ [] [] Πas≡Πbs asPrime bsPrime = ↭-refl
   factorisationUnique′ [] (b@(2+ _) ∷ bs) Πas≡Πbs prime[as] (_ ∷ prime[bs]) =
     contradiction Πas≡Πbs (<⇒≢ Πas<Πbs)
     where

src/Data/Nat/SumAndProduct.agda

@@ -0,0 +1,90 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Natural numbers: sum and product of lists
+--
+-- Issue #2553: this is a compatibility stub module,
+-- ahead of a more thorough breaking set of changes.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Nat.SumAndProduct where
+
+open import Algebra.Bundles using (CommutativeMonoid)
+open import Data.List.Base using (List; []; _∷_; _++_; foldr)
+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; _≤_)
+open import Data.Nat.Divisibility using (_∣_; m∣m*n; ∣n⇒∣m*n)
+open import Data.Nat.Properties
+  using (+-assoc; *-assoc; *-identityˡ; m*n≢0; m≤m*n; m≤n⇒m≤o*n;
+         +-0-commutativeMonoid; *-1-commutativeMonoid)
+open import Relation.Binary.Core using (_Preserves_⟶_)
+open import Relation.Binary.PropositionalEquality.Core
+  using (_≡_; refl; sym; cong)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
+
+private
+  variable
+    m n : ℕ
+    ms ns : List ℕ
+
+
+------------------------------------------------------------------------
+-- Definitions
+
+sum : List ℕ → ℕ
+sum = foldr _+_ 0
+
+product : List ℕ → ℕ
+product = foldr _*_ 1
+
+------------------------------------------------------------------------
+-- Properties
+
+-- sum
+
+sum-++ : ∀ ms ns → sum (ms ++ ns) ≡ sum ms + sum ns
+sum-++ []       ns = refl
+sum-++ (m ∷ ms) ns = begin
+  m + sum (ms ++ ns)     ≡⟨ cong (m +_) (sum-++ ms ns) ⟩
+  m + (sum ms + sum ns)  ≡⟨ +-assoc m _ _ ⟨
+  (m + sum ms) + sum ns  ∎
+  where open ≡-Reasoning
+
+sum-↭ : sum Preserves _↭_ ⟶ _≡_
+sum-↭ p = foldr-commMonoid ℕ-+-0.setoid ℕ-+-0.isCommutativeMonoid (↭⇒↭ₛ p)
+  where module ℕ-+-0 = CommutativeMonoid +-0-commutativeMonoid
+
+
+-- product
+
+product-++ : ∀ ms ns → product (ms ++ ns) ≡ product ms * product ns
+product-++ []       ns = sym (*-identityˡ _)
+product-++ (m ∷ ms) ns = begin
+  m * product (ms ++ ns)         ≡⟨ cong (m *_) (product-++ ms ns) ⟩
+  m * (product ms * product ns)  ≡⟨ *-assoc m _ _ ⟨
+  (m * product ms) * product ns  ∎
+  where open ≡-Reasoning
+
+∈⇒∣product : n ∈ ns → n ∣ product ns
+∈⇒∣product {ns = n ∷ ns} (here  refl) = m∣m*n (product ns)
+∈⇒∣product {ns = m ∷ ns} (there n∈ns) = ∣n⇒∣m*n m (∈⇒∣product n∈ns)
+
+product≢0 : All NonZero ns → NonZero (product ns)
+product≢0 []           = _
+product≢0 (n≢0 ∷ ns≢0) = m*n≢0 _ _ {{n≢0}} {{product≢0 ns≢0}}
+
+∈⇒≤product : All NonZero ns → n ∈ ns → n ≤ product ns
+∈⇒≤product (n≢0 ∷ ns≢0) (here refl)  = m≤m*n _ _ {{product≢0 ns≢0}}
+∈⇒≤product (n≢0 ∷ ns≢0) (there n∈ns) = m≤n⇒m≤o*n _ {{n≢0}} (∈⇒≤product ns≢0 n∈ns)
+
+product-↭ : product Preserves _↭_ ⟶ _≡_
+product-↭ p = foldr-commMonoid ℕ-*-1.setoid ℕ-*-1.isCommutativeMonoid (↭⇒↭ₛ p)
+  where module ℕ-*-1 = CommutativeMonoid *-1-commutativeMonoid

src/Data/Tree/Binary/Zipper.agda

@@ -10,9 +10,10 @@ module Data.Tree.Binary.Zipper where
 
 open import Level using (Level; _⊔_)
 open import Data.Tree.Binary as BT using (Tree; node; leaf)
-open import Data.List.Base as List using (List; []; _∷_; sum; _++_; [_])
+open import Data.List.Base as List using (List; []; _∷_; _++_; [_])
 open import Data.Maybe.Base using (Maybe; nothing; just)
 open import Data.Nat.Base using (ℕ; suc; _+_)
+open import Data.Nat.SumAndProduct using (sum)
 open import Function.Base using (_$_; _∘_)
 
 private