Deprecate Algebra.Operations.Semiring

CHANGELOG.md

@@ -86,6 +86,9 @@ Deprecated modules
   The properties of summation in `Algebra.Properties.CommutativeMonoid` have likewise
   been deprecated and moved to `Algebra.Properties.CommutativeMonoid.Summation`.
 
+* The module `Algebra.Operations.Semiring` has been deprecated. The contents has
+  been moved to `Algebra.Properties.Semiring.(Multiplication/Exponentiation)`.
+
 Deprecated names
 ----------------
 
@@ -166,7 +169,7 @@ New modules
   Algebra.Properties.CommutativeSemigroup.Divisibility
   ```
 
-* Generic summations over algebraic structures
+* Generic summation over algebraic structures
   ```
   Algebra.Properties.Monoid.Summation
   Algebra.Properties.CommutativeMonoid.Summation
@@ -175,6 +178,12 @@ New modules
 * Generic multiplication over algebraic structures
   ```
   Algebra.Properties.Monoid.Multiplication
+  Algebra.Properties.Semiring.Multiplication
+  ```
+
+* Generic exponentiation over algebraic structures
+  ```
+  Algebra.Properties.Semiring.Exponentiation
   ```
 
 * Setoid equality over vectors:

src/Algebra/Operations/Semiring.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 #-}
@@ -12,68 +11,21 @@
 {-# OPTIONS --warn=noUserWarning #-}
 
 open import Algebra
+import Algebra.Operations.CommutativeMonoid as MonoidOperations
 
 module Algebra.Operations.Semiring {s₁ s₂} (S : Semiring s₁ s₂) where
 
-import Algebra.Operations.CommutativeMonoid as MonoidOperations
-open import Data.Nat.Base
-  using (zero; suc; ℕ) renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
-open import Data.Product using (module Σ)
-open import Function.Base using (_$_)
-open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+{-# WARNING_ON_IMPORT
+"Algebra.Operations.Semiring was deprecated in v1.5.
+Use Algebra.Properties.Semiring.(Multiplication/Exponentiation) instead."
+#-}
 
-open Semiring S renaming (zero to *-zero)
-open import Relation.Binary.Reasoning.Setoid setoid
+open Semiring S
 
 ------------------------------------------------------------------------
--- Operations
+-- Re-exports
 
--- Re-export all monoid operations and proofs
 open MonoidOperations +-commutativeMonoid public
-
--- Exponentiation.
-infixr 9 _^_
-_^_ : Carrier → ℕ → Carrier
-x ^ zero  = 1#
-x ^ suc n = x * x ^ n
-
-------------------------------------------------------------------------
--- Properties of _×_
-
--- _× 1# is homomorphic with respect to _ℕ*_/_*_.
-
-×1-homo-* : ∀ m n → (m ℕ* n) × 1# ≈ (m × 1#) * (n × 1#)
-×1-homo-* 0 n = begin
-  0#             ≈⟨ sym (Σ.proj₁ *-zero (n × 1#)) ⟩
-  0# * (n × 1#)  ∎
-×1-homo-* (suc m) n = begin
-  (n ℕ+ m ℕ* n) × 1#                  ≈⟨ ×-homo-+ 1# n (m ℕ* n) ⟩
-  n × 1# + (m ℕ* n) × 1#              ≈⟨ +-cong refl (×1-homo-* m n) ⟩
-  n × 1# + (m × 1#) * (n × 1#)         ≈⟨ sym (+-cong (*-identityˡ _) refl) ⟩
-  1# * (n × 1#) + (m × 1#) * (n × 1#)  ≈⟨ sym (distribʳ (n × 1#) 1# (m × 1#)) ⟩
-  (1# + m × 1#) * (n × 1#)             ∎
-
-------------------------------------------------------------------------
--- Properties of _×′_
-
--- _×′ 1# is homomorphic with respect to _ℕ*_/_*_.
-
-×′1-homo-* : ∀ m n → (m ℕ* n) ×′ 1# ≈ (m ×′ 1#) * (n ×′ 1#)
-×′1-homo-* m n = begin
-  (m ℕ* n) ×′ 1#         ≈⟨ sym $ ×≈×′ (m ℕ* n) 1# ⟩
-  (m ℕ* n) ×  1#         ≈⟨ ×1-homo-* m n ⟩
-  (m ×  1#) * (n ×  1#)  ≈⟨ *-cong (×≈×′ m 1#) (×≈×′ n 1#) ⟩
-  (m ×′ 1#) * (n ×′ 1#)  ∎
-
-------------------------------------------------------------------------
--- Properties of _^_
-
--- _^_ preserves equality.
-
-^-congˡ : ∀ n → (_^ n) Preserves _≈_ ⟶ _≈_
-^-congˡ zero    x≈y = refl
-^-congˡ (suc n) x≈y = *-cong x≈y (^-congˡ n x≈y)
-
-^-cong : _^_ Preserves₂ _≈_ ⟶ _≡_ ⟶ _≈_
-^-cong {v = n} x≈y P.refl = ^-congˡ n x≈y
+open import Algebra.Properties.Semiring.Exponentiation S public
+open import Algebra.Properties.Semiring.Multiplication S public
+  using (×1-homo-*; ×′1-homo-*)

src/Algebra/Properties/Monoid/Multiplication.agda

@@ -18,7 +18,7 @@ open Monoid M
   renaming
   ( _∙_       to _+_
   ; ∙-cong    to +-cong
-  ; ∙-congˡ   to ∙-congˡ
+  ; ∙-congˡ   to +-congˡ
   ; identityˡ to +-identityˡ
   ; identityʳ to +-identityʳ
   ; assoc     to +-assoc
@@ -69,7 +69,7 @@ suc n ×′ x = x + n ×′ x
          ∀ n → .{{_ : NonZero n}} → n × c ≈ c
 ×-idem {c} idem (suc zero)    = +-identityʳ c
 ×-idem {c} idem (suc (suc n)) = begin
-  c + (suc n × c) ≈⟨ ∙-congˡ (×-idem idem (suc n) ) ⟩
+  c + (suc n × c) ≈⟨ +-congˡ (×-idem idem (suc n) ) ⟩
   c + c           ≈⟨ idem ⟩
   c               ∎
 
@@ -86,7 +86,7 @@ suc n ×′ x = x + n ×′ x
 ×≈×′ : ∀ n x → n × x ≈ n ×′ x
 ×≈×′ 0       x = refl
 ×≈×′ (suc n) x = begin
-  x + n × x   ≈⟨ +-cong refl (×≈×′ n x) ⟩
+  x + n × x   ≈⟨ +-congˡ (×≈×′ n x) ⟩
   x + n ×′ x  ≈⟨ sym (1+×′ n x) ⟩
   suc n ×′ x  ∎
 

src/Algebra/Properties/Semiring/Exponentiation.agda

@@ -0,0 +1,42 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Exponentiation defined over a semiring as repeated multiplication
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra
+
+module Algebra.Properties.Semiring.Exponentiation
+  {a ℓ} (S : Semiring a ℓ) where
+
+open import Data.Nat.Base using (zero; suc; ℕ)
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality as P using (_≡_)
+
+open Semiring S renaming (zero to *-zero)
+open import Relation.Binary.Reasoning.Setoid setoid
+
+------------------------------------------------------------------------
+-- Operations
+
+-- Standard exponentiation.
+
+infixr 9 _^_
+
+_^_ : Carrier → ℕ → Carrier
+x ^ zero  = 1#
+x ^ suc n = x * x ^ n
+
+------------------------------------------------------------------------
+-- Properties of _^_
+
+-- _^_ preserves equality.
+
+^-congˡ : ∀ n → (_^ n) Preserves _≈_ ⟶ _≈_
+^-congˡ zero    x≈y = refl
+^-congˡ (suc n) x≈y = *-cong x≈y (^-congˡ n x≈y)
+
+^-cong : _^_ Preserves₂ _≈_ ⟶ _≡_ ⟶ _≈_
+^-cong {v = n} x≈y P.refl = ^-congˡ n x≈y

src/Algebra/Properties/Semiring/Multiplication.agda

@@ -0,0 +1,48 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Multiplication by a natural number over a semiring
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra
+import Algebra.Properties.Monoid.Multiplication as MonoidMultiplication
+open import Data.Nat.Base as ℕ using (zero; suc)
+
+module Algebra.Properties.Semiring.Multiplication
+  {a ℓ} (S : Semiring a ℓ) where
+
+open Semiring S renaming (zero to *-zero)
+open import Relation.Binary.Reasoning.Setoid setoid
+
+------------------------------------------------------------------------
+-- Re-export definition from the monoid
+
+open MonoidMultiplication +-monoid public
+
+------------------------------------------------------------------------
+-- Properties of _×_
+
+-- (_× 1#) is homomorphic with respect to _ℕ.*_/_*_.
+
+×1-homo-* : ∀ m n → (m ℕ.* n) × 1# ≈ (m × 1#) * (n × 1#)
+×1-homo-* 0       n = sym (zeroˡ (n × 1#))
+×1-homo-* (suc m) n = begin
+  (n ℕ.+ m ℕ.* n) × 1#                ≈⟨  ×-homo-+ 1# n (m ℕ.* n) ⟩
+  n × 1# + (m ℕ.* n) × 1#             ≈⟨  +-congˡ (×1-homo-* m n) ⟩
+  n × 1# + (m × 1#) * (n × 1#)        ≈˘⟨ +-congʳ (*-identityˡ _) ⟩
+  1# * (n × 1#) + (m × 1#) * (n × 1#) ≈˘⟨ distribʳ (n × 1#) 1# (m × 1#) ⟩
+  (1# + m × 1#) * (n × 1#)            ∎
+
+------------------------------------------------------------------------
+-- Properties of _×′_
+
+-- (_×′ 1#) is homomorphic with respect to _ℕ.*_/_*_.
+
+×′1-homo-* : ∀ m n → (m ℕ.* n) ×′ 1# ≈ (m ×′ 1#) * (n ×′ 1#)
+×′1-homo-* m n = begin
+  (m ℕ.* n) ×′ 1#        ≈˘⟨ ×≈×′ (m ℕ.* n) 1# ⟩
+  (m ℕ.* n) ×  1#        ≈⟨  ×1-homo-* m n ⟩
+  (m ×  1#) * (n ×  1#)  ≈⟨  *-cong (×≈×′ m 1#) (×≈×′ n 1#) ⟩
+  (m ×′ 1#) * (n ×′ 1#)  ∎

src/Algebra/Solver/Ring.agda

@@ -37,7 +37,7 @@ open AlmostCommutativeRing R
 open import Algebra.Definitions _≈_
 open import Algebra.Morphism
 open _-Raw-AlmostCommutative⟶_ morphism renaming (⟦_⟧ to ⟦_⟧′)
-open import Algebra.Operations.Semiring semiring
+open import Algebra.Properties.Semiring.Exponentiation semiring
 
 open import Relation.Binary
 open import Relation.Nullary using (yes; no)

src/Algebra/Solver/Ring/NaturalCoefficients.agda

@@ -8,13 +8,13 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Algebra
-import Algebra.Operations.Semiring as SemiringOps
+import Algebra.Properties.Semiring.Multiplication as SemiringMultiplication
 open import Data.Maybe.Base using (Maybe; just; nothing; map)
 
 module Algebra.Solver.Ring.NaturalCoefficients
   {r₁ r₂} (R : CommutativeSemiring r₁ r₂)
   (open CommutativeSemiring R)
-  (open SemiringOps semiring)
+  (open SemiringMultiplication semiring)
   (dec : ∀ m n → Maybe (m × 1# ≈ n × 1#)) where
 
 import Algebra.Solver.Ring

src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda

@@ -16,14 +16,14 @@ open import Algebra
 module Algebra.Solver.Ring.NaturalCoefficients.Default
   {r₁ r₂} (R : CommutativeSemiring r₁ r₂) where
 
-import Algebra.Operations.Semiring as SemiringOps
+import Algebra.Properties.Semiring.Multiplication as SemiringMultiplication
 open import Data.Maybe.Base using (Maybe; map)
 open import Data.Nat using (_≟_)
 open import Relation.Binary.Consequences using (dec⟶weaklyDec)
 import Relation.Binary.PropositionalEquality as P
 
 open CommutativeSemiring R
-open SemiringOps semiring
+open SemiringMultiplication semiring
 
 private
   dec : ∀ m n → Maybe (m × 1# ≈ n × 1#)