Deprecate Algebra.Operations.CommutativeMonoid (#1351)

Author: MatthewDaggitt

CHANGELOG.md

@@ -63,6 +63,14 @@ Deprecated modules
   complete. The new definitions are parameterised by raw bundles instead of bundles
   meaning they are much more flexible to work with.
 
+* The module `Algebra.Operations.CommutativeMonoid` has been deprecated. The definition
+  of multiplication and the associated properties have been moved to
+  `Algebra.Properties.CommutativeMonoid.Multiplication`. The definition of summation
+  which was defined over the deprecated `Data.Table` has been redefined in terms of
+  `Data.Vec.Functional` and been moved to `Algbra.Properties.CommutativeMonoid.Summation`.
+  The properties of summation in `Algebra.Properties.CommutativeMonoid` have likewise
+  been deprecated and moved to `Algebra.Properties.CommutativeMonoid.Summation`.
+
 Deprecated names
 ----------------
 
@@ -125,6 +133,22 @@ New modules
   Algebra.Properties.CommutativeSemigroup.Divisibility
   ```
 
+* Generic summations over algebraic structures
+  ```
+  Algebra.Properties.Monoid.Summation
+  Algebra.Properties.CommutativeMonoid.Summation
+  ```
+
+* Generic multiplication over algebraic structures
+  ```
+  Algebra.Properties.Monoid.Multiplication
+  ```
+
+* Setoid equality over vectors:
+  ```
+  Data.Vec.Functional.Relation.Binary.Equality.Setoid
+  ```
+
 * Heterogeneous relation characterising a list as an infix segment of another:
   ```
   Data.List.Relation.Binary.Infix.Heterogeneous

src/Algebra/Operations/CommutativeMonoid.agda

@@ -1,8 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Some defined operations (multiplication by natural number and
--- exponentiation)
+-- This module is DEPRECATED.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
@@ -11,51 +10,26 @@
 {-# OPTIONS --warn=noUserWarning #-}
 
 open import Algebra
+open import Data.List.Base as List using (List; []; _∷_; _++_)
+open import Data.Fin.Base using (Fin; zero)
+open import Data.Table.Base as Table using (Table)
+open import Function using (_∘_)
+open import Relation.Binary.PropositionalEquality as P using (_≡_)
 
 module Algebra.Operations.CommutativeMonoid
   {s₁ s₂} (CM : CommutativeMonoid s₁ s₂)
   where
 
-open import Data.Nat.Base using (ℕ; zero; suc)
-  renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
-open import Data.List.Base as List using (List; []; _∷_; _++_)
-open import Data.Fin.Base using (Fin; zero)
-open import Data.Product using (proj₁; proj₂)
-open import Data.Table.Base as Table using (Table)
-open import Function using (_∘_; _⟨_⟩_)
-open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+{-# WARNING_ON_IMPORT
+"Algebra.Operations.CommutativeMonoid was deprecated in v1.5.
+Use Algebra.Properties.CommutativeMonoid.(Summation/Multiplication) instead."
+#-}
 
 open CommutativeMonoid CM
   renaming
   ( _∙_       to _+_
-  ; ∙-cong    to +-cong
-  ; identityˡ to +-identityˡ
-  ; identityʳ to +-identityʳ
-  ; assoc     to +-assoc
-  ; comm      to +-comm
   ; ε         to 0#
   )
-open import Relation.Binary.Reasoning.Setoid setoid
-
-------------------------------------------------------------------------
--- Operations
-
--- Multiplication by natural number.
-
-infixr 8 _×_ _×′_
-
-_×_ : ℕ → Carrier → Carrier
-0     × x = 0#
-suc n × x = x + n × x
-
--- A variant that includes a "redundant" case which ensures that `1 × x`
--- is definitionally equal to `x`.
-
-_×′_ : ℕ → Carrier → Carrier
-0     ×′ x = 0#
-1     ×′ x = x
-suc n ×′ x = x + n ×′ x
 
 -- Summation over lists/tables
 
@@ -75,55 +49,6 @@ sumₜ-syntax _ = sumₜ ∘ Table.tabulate
 syntax sumₜ-syntax n (λ i → x) = ∑[ i < n ] x
 
 ------------------------------------------------------------------------
--- Properties of _×_
-
-×-congʳ : ∀ n → (n ×_) Preserves _≈_ ⟶ _≈_
-×-congʳ 0       x≈x′ = refl
-×-congʳ (suc n) x≈x′ = x≈x′ ⟨ +-cong ⟩ ×-congʳ n x≈x′
-
-×-cong : _×_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_
-×-cong {u} P.refl x≈x′ = ×-congʳ u x≈x′
-
--- _×_ is homomorphic with respect to _ℕ+_/_+_.
-
-×-homo-+ : ∀ c m n → (m ℕ+ n) × c ≈ m × c + n × c
-×-homo-+ c 0       n = sym (+-identityˡ (n × c))
-×-homo-+ c (suc m) n = begin
-  c + (m ℕ+ n) × c     ≈⟨ +-cong refl (×-homo-+ c m n) ⟩
-  c + (m × c + n × c)  ≈⟨ sym (+-assoc c (m × c) (n × c)) ⟩
-  c + m × c + n × c    ∎
-
-------------------------------------------------------------------------
--- Properties of _×′_
-
-1+×′ : ∀ n x → suc n ×′ x ≈ x + n ×′ x
-1+×′ 0       x = sym (+-identityʳ x)
-1+×′ (suc n) x = refl
-
--- _×_ and _×′_ are extensionally equal (up to the setoid
--- equivalence).
-
-×≈×′ : ∀ n x → n × x ≈ n ×′ x
-×≈×′ 0       x = begin 0# ∎
-×≈×′ (suc n) x = begin
-  x + n × x   ≈⟨ +-cong refl (×≈×′ n x) ⟩
-  x + n ×′ x  ≈⟨ sym (1+×′ n x) ⟩
-  suc n ×′ x  ∎
-
--- _×′_ is homomorphic with respect to _ℕ+_/_+_.
-
-×′-homo-+ : ∀ c m n → (m ℕ+ n) ×′ c ≈ m ×′ c + n ×′ c
-×′-homo-+ c m n = begin
-  (m ℕ+ n) ×′ c    ≈⟨ sym (×≈×′ (m ℕ+ n) c) ⟩
-  (m ℕ+ n) ×  c    ≈⟨ ×-homo-+ c m n ⟩
-  m ×  c + n ×  c  ≈⟨ +-cong (×≈×′ m c) (×≈×′ n c) ⟩
-  m ×′ c + n ×′ c  ∎
-
--- _×′_ preserves equality.
+-- Operations
 
-×′-cong : _×′_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_
-×′-cong {n} {_} {x} {y} P.refl x≈y = begin
-  n  ×′ x ≈⟨ sym (×≈×′ n x) ⟩
-  n  ×  x ≈⟨ ×-congʳ n x≈y ⟩
-  n  ×  y ≈⟨ ×≈×′ n y ⟩
-  n  ×′ y ∎
+open import Algebra.Properties.Monoid.Multiplication monoid public

src/Algebra/Operations/Semiring.agda

@@ -7,6 +7,10 @@
 
 {-# OPTIONS --without-K --safe #-}
 
+-- Disabled to prevent warnings from deprecated
+-- Algebra.Operations.CommutativeMonoid
+{-# OPTIONS --warn=noUserWarning #-}
+
 open import Algebra
 
 module Algebra.Operations.Semiring {s₁ s₂} (S : Semiring s₁ s₂) where

src/Algebra/Properties/CommutativeMonoid.agda

@@ -52,41 +52,35 @@ open CommutativeMonoid M
 open import Algebra.Definitions _≈_
 open import Relation.Binary.Reasoning.Setoid setoid
 
-module _ {n} where
-  open B.Setoid (TE.setoid setoid n) public
-    using ()
-    renaming (_≈_ to _≋_)
 
--- When summing over a function from a finite set, we can pull out any value and move it to the front.
 
-sumₜ-remove : ∀ {n} {i : Fin (suc n)} t → sumₜ t ≈ lookup t i + sumₜ (remove i t)
-sumₜ-remove {_}     {zero}   t = refl
-sumₜ-remove {suc n} {suc i}  t′ =
-  begin
-    t₀ + ∑t           ≈⟨ +-congˡ (sumₜ-remove t) ⟩
-    t₀ + (tᵢ + ∑t′)   ≈⟨ solve 3 (λ x y z → x ⊕ (y ⊕ z) ⊜ y ⊕ (x ⊕ z)) refl t₀ tᵢ ∑t′ ⟩
-    tᵢ + (t₀ + ∑t′)   ∎
-  where
-  t = tail t′
-  t₀ = head t′
-  tᵢ = lookup t i
-  ∑t = sumₜ t
-  ∑t′ = sumₜ (remove i t)
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+module _ {n} where
+  open B.Setoid (TE.setoid setoid n) public
+    using () renaming (_≈_ to _≋_)
 
--- '_≈_' is a congruence over 'sumTable n'.
+-- Version 1.5
 
 sumₜ-cong-≈ : ∀ {n} → sumₜ {n} Preserves _≋_ ⟶ _≈_
 sumₜ-cong-≈ {zero}  p = refl
 sumₜ-cong-≈ {suc n} p = +-cong (p _) (sumₜ-cong-≈ (p ∘ suc))
-
--- '_≡_' is a congruence over 'sum n'.
+{-# WARNING_ON_USAGE sumₜ-cong-≈
+"Warning: sumₜ-cong-≈ was deprecated in v1.5.
+Please use sum-cong-≋ from `Algebra.Properties.CommutativeMonoid.Summation` instead."
+#-}
 
 sumₜ-cong-≡ : ∀ {n} → sumₜ {n} Preserves _≗_ ⟶ _≡_
 sumₜ-cong-≡ {zero}  p = P.refl
 sumₜ-cong-≡ {suc n} p = P.cong₂ _+_ (p _) (sumₜ-cong-≡ (p ∘ suc))
-
--- If addition is idempotent on a particular value 'x', then summing over a
--- nonzero number of copies of 'x' gives back 'x'.
+{-# WARNING_ON_USAGE sumₜ-cong-≡
+"Warning: sumₜ-cong-≡ was deprecated in v1.5.
+Please use sum-cong-≗ from `Algebra.Properties.CommutativeMonoid.Summation` instead."
+#-}
 
 sumₜ-idem-replicate : ∀ n {x} → _+_ IdempotentOn x → sumₜ (replicate {n = suc n} x) ≈ x
 sumₜ-idem-replicate zero        idem = +-identityʳ _
@@ -95,16 +89,38 @@ sumₜ-idem-replicate (suc n) {x} idem = begin
   (x + x) + sumₜ (replicate {n = n} x)  ≈⟨ +-congʳ idem ⟩
   x + sumₜ (replicate {n = n} x)        ≈⟨ sumₜ-idem-replicate n idem ⟩
   x                                 ∎
-
--- The sum over the constantly zero function is zero.
+{-# WARNING_ON_USAGE sumₜ-idem-replicate
+"Warning: sumₜ-idem-replicate was deprecated in v1.5.
+Please use sum-replicate-idem from `Algebra.Properties.CommutativeMonoid.Summation` instead."
+#-}
 
 sumₜ-zero : ∀ n → sumₜ (replicate {n = n} 0#) ≈ 0#
 sumₜ-zero n = begin
   sumₜ (replicate {n = n} 0#)      ≈⟨ sym (+-identityˡ _) ⟩
   0# + sumₜ (replicate {n = n} 0#) ≈⟨ sumₜ-idem-replicate n (+-identityˡ 0#) ⟩
   0#                               ∎
+{-# WARNING_ON_USAGE sumₜ-zero
+"Warning: sumₜ-zero was deprecated in v1.5.
+Please use sum-replicate-zero from `Algebra.Properties.CommutativeMonoid.Summation` instead."
+#-}
 
--- The '∑' operator distributes over addition.
+sumₜ-remove : ∀ {n} {i : Fin (suc n)} t → sumₜ t ≈ lookup t i + sumₜ (remove i t)
+sumₜ-remove {_}     {zero}   t = refl
+sumₜ-remove {suc n} {suc i}  t′ =
+  begin
+    t₀ + ∑t           ≈⟨ +-congˡ (sumₜ-remove t) ⟩
+    t₀ + (tᵢ + ∑t′)   ≈⟨ solve 3 (λ x y z → x ⊕ (y ⊕ z) ⊜ y ⊕ (x ⊕ z)) refl t₀ tᵢ ∑t′ ⟩
+    tᵢ + (t₀ + ∑t′)   ∎
+  where
+  t = tail t′
+  t₀ = head t′
+  tᵢ = lookup t i
+  ∑t = sumₜ t
+  ∑t′ = sumₜ (remove i t)
+{-# WARNING_ON_USAGE sumₜ-remove
+"Warning: sumₜ-remove was deprecated in v1.5.
+Please use sum-remove from `Algebra.Properties.CommutativeMonoid.Summation` instead."
+#-}
 
 ∑-distrib-+ : ∀ n (f g : Fin n → Carrier) → ∑[ i < n ] (f i + g i) ≈ ∑[ i < n ] f i + ∑[ i < n ] g i
 ∑-distrib-+ zero    f g = sym (+-identityˡ _)
@@ -119,17 +135,21 @@ sumₜ-zero n = begin
   ∑f  = ∑[ i < n ] f (suc i)
   ∑g  = ∑[ i < n ] g (suc i)
   ∑fg = ∑[ i < n ] (f (suc i) + g (suc i))
-
--- The '∑' operator commutes with itself.
+{-# WARNING_ON_USAGE ∑-distrib-+
+"Warning: ∑-distrib-+ was deprecated in v1.5.
+Please use ∑-distrib-+ from `Algebra.Properties.CommutativeMonoid.Summation` instead."
+#-}
 
 ∑-comm : ∀ n m (f : Fin n → Fin m → Carrier) → ∑[ i < n ] ∑[ j < m ] f i j ≈ ∑[ j < m ] ∑[ i < n ] f i j
 ∑-comm zero    m f = sym (sumₜ-zero m)
 ∑-comm (suc n) m f = begin
   ∑[ j < m ] f zero j + ∑[ i < n ] ∑[ j < m ] f (suc i) j  ≈⟨ +-congˡ (∑-comm n m _) ⟩
   ∑[ j < m ] f zero j + ∑[ j < m ] ∑[ i < n ] f (suc i) j  ≈⟨ sym (∑-distrib-+ m _ _) ⟩
   ∑[ j < m ] (f zero j + ∑[ i < n ] f (suc i) j)           ∎
-
--- Any permutation of a table has the same sum as the original.
+{-# WARNING_ON_USAGE ∑-distrib-+
+"Warning: ∑-comm was deprecated in v1.5.
+Please use ∑-comm from `Algebra.Properties.CommutativeMonoid.Summation` instead."
+#-}
 
 sumₜ-permute : ∀ {m n} t (π : Permutation m n) → sumₜ t ≈ sumₜ (permute π t)
 sumₜ-permute {zero}  {zero}  t π = refl
@@ -145,9 +165,17 @@ sumₜ-permute {suc m} {suc n} t π = begin
   where
   0i = zero
   πt = permute π t
+{-# WARNING_ON_USAGE sumₜ-permute
+"Warning: sumₜ-permute was deprecated in v1.5.
+Please use sum-permute from `Algebra.Properties.CommutativeMonoid.Summation` instead."
+#-}
 
 ∑-permute : ∀ {m n} f (π : Permutation m n) → ∑[ i < n ] f i ≈ ∑[ i < m ] f (π ⟨$⟩ʳ i)
 ∑-permute = sumₜ-permute ∘ tabulate
+{-# WARNING_ON_USAGE ∑-permute
+"Warning: ∑-permute was deprecated in v1.5.
+Please use ∑-permute from `Algebra.Properties.CommutativeMonoid.Summation` instead."
+#-}
 
 -- If the function takes the same value at 'i' and 'j', then transposing 'i' and
 -- 'j' then selecting 'j' is the same as selecting 'i'.