Deprecate Algebra.Operations.Ring and refactor Tactics.RingSolver (#1396)

Author: MatthewDaggitt

CHANGELOG.md

@@ -87,16 +87,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`.
-
-* The module `Algebra.Operations.Semiring` has been deprecated. The contents has
-  been moved to `Algebra.Properties.Semiring.(Multiplication/Exponentiation)`.
+* All modules in the folder `Algebra.Operations` have been deprecated, as their design
+	a) was inconsistent, some are parameterised over the raw bundle and some over the normal bundle
+    b) prevented definitions from being neatly inherited by super-bundles.
+  
+  These problems have been fixed with a redesign: definitions of the operations can be found in 
+  `Algebra.Definitions.(RawMagma/RawMonoid/RawSemiring)` and their properties can be found in 
+  `Algebra.Properties.(Magma/Semigroup/Monoid/CommutativeMonoid/Semiring).(Sum/Mult/Exp)`. 
+  The latter also export the definition, and so most users will only need to import the latter.
 
 Deprecated names
 ----------------
@@ -200,29 +198,33 @@ New modules
   Algebra.Definitions.RawSemiring
   ```
 
+* Setoid equality over vectors:
+  ```
+  Data.Vec.Functional.Relation.Binary.Equality.Setoid
+  ```
+
 * Properties of generic definitions over algebraic structures (divisibility, multiplication etc.):
   ```
   Algebra.Properties.Magma.Divisibility
-  
   Algebra.Properties.Semigroup.Divisibility
-  
   Algebra.Properties.CommutativeSemigroup.Divisibility
   
-  Algebra.Properties.Monoid.Summation
-  Algebra.Properties.Monoid.Multiplication
+  Algebra.Properties.Monoid.Sum
+  Algebra.Properties.Monoid.Mult
   Algebra.Properties.Monoid.Divisibility
   
-  Algebra.Properties.CommutativeMonoid.Summation
+  Algebra.Properties.CommutativeMonoid.Sum
+  Algebra.Properties.CommutativeMonoid.Mult
   
-  Algebra.Properties.Semiring.Multiplication
-  Algebra.Properties.Semiring.Exponentiation
-  Algebra.Properties.Semiring.GCD
   Algebra.Properties.Semiring.Divisibility
-  ```
-
-* Setoid equality over vectors:
-  ```
-  Data.Vec.Functional.Relation.Binary.Equality.Setoid
+  Algebra.Properties.Semiring.Exp
+  Algebra.Properties.Semiring.Exp.TCOptimised
+  Algebra.Properties.Semiring.GCD
+  Algebra.Properties.Semiring.Mult
+  Algebra.Properties.Semiring.Mult.TCOptimised
+  
+  Algebra.Properties.CommutativeSemiring.Exp
+  Algebra.Properties.CommutativeSemiring.Exp.TCOptimised
   ```
 
 * Heterogeneous relation characterising a list as an infix segment of another:

src/Algebra/Bundles.agda

@@ -783,6 +783,22 @@ record RawRing c ℓ : Set (suc (c ⊔ ℓ)) where
     0#      : Carrier
     1#      : Carrier
 
+  rawSemiring : RawSemiring c ℓ
+  rawSemiring = record
+    { _≈_ = _≈_
+    ; _+_ = _+_
+    ; _*_ = _*_
+    ; 0#  = 0#
+    ; 1#  = 1#
+    }
+
+  open RawSemiring rawSemiring public
+    using
+    ( _≉_
+    ; +-rawMagma; +-rawMonoid
+    ; *-rawMagma; *-rawMonoid
+    )
+
   +-rawGroup : RawGroup c ℓ
   +-rawGroup = record
     { _≈_ = _≈_
@@ -791,13 +807,6 @@ record RawRing c ℓ : Set (suc (c ⊔ ℓ)) where
     ; _⁻¹ = -_
     }
 
-  *-rawMonoid : RawMonoid c ℓ
-  *-rawMonoid = record
-    { _≈_ = _≈_
-    ; _∙_ = _*_
-    ; ε   = 1#
-    }
-
 record Ring c ℓ : Set (suc (c ⊔ ℓ)) where
   infix  8 -_
   infixl 7 _*_

src/Algebra/Definitions/RawMonoid.agda

@@ -55,7 +55,9 @@ infixl 8 _×′_
 _×′_ : ℕ → Carrier → Carrier
 0     ×′ x = 0#
 1     ×′ x = x
-suc n ×′ x = x + n ×′ x
+suc n ×′ x = n ×′ x + x
+
+{-# INLINE _×′_ #-}
 
 ------------------------------------------------------------------------
 -- Summation

src/Algebra/Definitions/RawSemiring.agda

@@ -8,6 +8,7 @@
 
 open import Algebra.Bundles using (RawSemiring)
 open import Data.Sum.Base using (_⊎_)
+open import Data.Nat using (ℕ)
 open import Level using (_⊔_)
 open import Relation.Binary.Core using (Rel)
 
@@ -20,15 +21,15 @@ open RawSemiring M renaming (Carrier to A)
 
 open import Algebra.Definitions.RawMonoid +-rawMonoid public
   using
-  ( _×_
-  ; _×′_
-  ; sum
+  ( _×_   -- : ℕ → A → A
+  ; _×′_  -- : ℕ → A → A
+  ; sum   -- : Vector A n → A
   )
 
 ------------------------------------------------------------------------
 -- Definitions over _*_
 
-open import Algebra.Definitions.RawMonoid *-rawMonoid public
+open import Algebra.Definitions.RawMonoid *-rawMonoid as Mult public
   using
   ( _∣_
   ; _∤_
@@ -37,8 +38,24 @@ open import Algebra.Definitions.RawMonoid *-rawMonoid public
   ( sum to product
   )
 
+-- Unlike `sum` to `product`, can't simply rename multiplication to
+-- exponentation as the argument order is reversed.
+
+-- Standard exponentiation
+
+infixr 8 _^_
+_^_ : A → ℕ → A
+x ^ n  = n Mult.× x
+
+-- Exponentiation optimsed for type-checking
+
+infixr 8 _^′_
+_^′_ : A → ℕ → A
+x ^′ n  = n Mult.×′ x
+{-# INLINE _^′_ #-}
+
 ------------------------------------------------------------------------
--- Coprimality
+-- Primality
 
 Coprime : Rel A (a ⊔ ℓ)
 Coprime x y = ∀ {z} → z ∣ x → z ∣ y → z ∣ 1#

src/Algebra/Operations/CommutativeMonoid.agda

@@ -24,7 +24,7 @@ module Algebra.Operations.CommutativeMonoid
 
 {-# WARNING_ON_IMPORT
 "Algebra.Operations.CommutativeMonoid was deprecated in v1.5.
-Use Algebra.Properties.CommutativeMonoid.(Summation/Multiplication/Multiplication.TCOptimised) instead."
+Use Algebra.Properties.CommutativeMonoid.(Sum/Mult/Exp)(.TCOptimised) instead."
 #-}
 
 open CommutativeMonoid CM

src/Algebra/Operations/Ring.agda

@@ -1,40 +1,22 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Some defined operations over Rings
+-- This module is DEPRECATED.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
--- This module gives the definition of _^_ which is used throughout
--- the library. It's a little different from the normal definition:
---
---   x ^ zero  = 1#
---   x ^ suc i = x * x ^ i
---
--- This is for two reasons. First, we want to avoid unnecessarily
--- multiplying by 1# if possible:
---
---     Standard definition: x ^ 2 = x * x * 1#
---     Our definition:      x ^ 2 = x * x
---
--- This speeds up typechecking and makes for much more readable
--- proofs.
---
--- Secondly, we want to associate to the left:
---
---     Standard definition: x ^ 3 = x * (x * (x * 1#))
---     Our definition:      x ^ 2 = (x * x) * x
---
--- As counterintuitive as it may seem, this also speeds up
--- typechecking.
-
 open import Algebra
 
 module Algebra.Operations.Ring
   {ℓ₁ ℓ₂} (ring : RawRing ℓ₁ ℓ₂)
   where
 
+{-# WARNING_ON_IMPORT
+"Algebra.Operations.Ring was deprecated in v1.5.
+Use Algebra.Properties.Semiring.Exp(.TCOptimised) instead."
+#-}
+
 open import Data.Nat.Base as ℕ using (ℕ; suc; zero)
 
 open RawRing ring

src/Algebra/Operations/Semiring.agda

@@ -17,7 +17,7 @@ module Algebra.Operations.Semiring {s₁ s₂} (S : Semiring s₁ s₂) where
 
 {-# WARNING_ON_IMPORT
 "Algebra.Operations.Semiring was deprecated in v1.5.
-Use Algebra.Properties.Semiring.(Multiplication/Exponentiation) instead."
+Use Algebra.Properties.Semiring.(Mult/Exp) instead."
 #-}
 
 open Semiring S

src/Algebra/Properties/CommutativeMonoid/Mult.agda

@@ -0,0 +1,46 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Multiplication over a monoid (i.e. repeated addition)
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra.Bundles using (CommutativeMonoid)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
+
+module Algebra.Properties.CommutativeMonoid.Mult
+  {a ℓ} (M : CommutativeMonoid a ℓ) where
+
+-- View of the monoid operator as addition
+open CommutativeMonoid M
+  renaming
+  ( _∙_       to _+_
+  ; ∙-cong    to +-cong
+  ; ∙-congʳ   to +-congʳ
+  ; ∙-congˡ   to +-congˡ
+  ; identityˡ to +-identityˡ
+  ; identityʳ to +-identityʳ
+  ; assoc     to +-assoc
+  ; ε         to 0#
+  )
+
+open import Relation.Binary.Reasoning.Setoid setoid
+open import Algebra.Properties.CommutativeSemigroup commutativeSemigroup
+
+------------------------------------------------------------------------
+-- Re-export definition and properties for monoids
+
+open import Algebra.Properties.Monoid.Mult monoid public
+
+------------------------------------------------------------------------
+-- Properties of _×_
+
+×-distrib-+ : ∀ x y n → n × (x + y) ≈ n × x + n × y
+×-distrib-+ x y zero    = sym (+-identityˡ 0# )
+×-distrib-+ x y (suc n) = begin
+  x + y + n × (x + y)       ≈⟨ +-congˡ (×-distrib-+ x y n) ⟩
+  x + y + (n × x + n × y)   ≈⟨ +-assoc x y (n × x + n × y) ⟩
+  x + (y + (n × x + n × y)) ≈⟨ +-congˡ (x∙yz≈y∙xz y (n × x) (n × y)) ⟩
+  x + (n × x + suc n × y)   ≈⟨ x∙yz≈xy∙z x (n × x) (suc n × y) ⟩
+  suc n × x + suc n × y     ∎

src/Algebra/Properties/CommutativeMonoid/Mult/TCOptimised.agda

@@ -0,0 +1,47 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Multiplication over a monoid (i.e. repeated addition) optimised for
+-- type checking.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra.Bundles using (CommutativeMonoid)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
+open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
+open import Relation.Binary.PropositionalEquality as P using (_≡_)
+
+module Algebra.Properties.CommutativeMonoid.Mult.TCOptimised
+  {a ℓ} (M : CommutativeMonoid a ℓ) where
+
+open CommutativeMonoid M renaming
+  ( _∙_       to _+_
+  ; ∙-cong    to +-cong
+  ; ∙-congˡ   to +-congˡ
+  ; ∙-congʳ   to +-congʳ
+  ; identityˡ to +-identityˡ
+  ; identityʳ to +-identityʳ
+  ; assoc     to +-assoc
+  ; ε         to 0#
+  )
+
+open import Algebra.Properties.CommutativeMonoid.Mult M as U
+  using () renaming (_×_ to _×ᵤ_)
+
+open import Relation.Binary.Reasoning.Setoid setoid
+
+------------------------------------------------------------------------
+-- Re-export definition and properties for monoids
+
+open import Algebra.Properties.Monoid.Mult.TCOptimised monoid public
+
+------------------------------------------------------------------------
+-- Properties
+
+×-distrib-+ : ∀ x y n → n × (x + y) ≈ n × x + n × y
+×-distrib-+ x y n = begin
+  n ×  (x + y)    ≈˘⟨ ×ᵤ≈× n (x + y) ⟩
+  n ×ᵤ (x + y)    ≈⟨  U.×-distrib-+ x y n ⟩
+  n ×ᵤ x + n ×ᵤ y ≈⟨  +-cong (×ᵤ≈× n x) (×ᵤ≈× n y) ⟩
+  n ×  x + n ×  y ∎

src/Algebra/Properties/CommutativeMonoid/Summation.agda renamed to src/Algebra/Properties/CommutativeMonoid/Sum.agda

@@ -18,7 +18,7 @@ open import Function.Equality using (_⟨$⟩_)
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Nullary.Negation using (contradiction)
 
-module Algebra.Properties.CommutativeMonoid.Summation
+module Algebra.Properties.CommutativeMonoid.Sum
   {a ℓ} (M : CommutativeMonoid a ℓ) where
 
 open CommutativeMonoid M
@@ -40,7 +40,7 @@ open import Relation.Binary.Reasoning.Setoid setoid
 ------------------------------------------------------------------------
 -- Re-export summation over monoids
 
-open import Algebra.Properties.Monoid.Summation monoid public
+open import Algebra.Properties.Monoid.Sum monoid public
 
 ------------------------------------------------------------------------
 -- Properties