Fix #2195 by removing redundant zero from IsRing

CHANGELOG.md

@@ -33,6 +33,12 @@ Highlights
 Bug-fixes
 ---------
 
+* In `Algebra.Structures` the record `IsRing` contained an unnecessary field
+  `zero : RightZero 0# *`, which could be derived from the other ring axioms.
+  Consequently this field has been removed from the record, and the record
+  `IsRingWithoutAnnihilatingZero` in `Algebra.Structures.Biased` has been
+  deprecated as it is now identical to is `IsRing`.
+
 * In `Algebra.Definitions.RawSemiring` the record `Prime` did not
   enforce that the number was not divisible by `1#`. To fix this
   `p∤1 : p ∤ 1#` has been added as a field.

src/Algebra/Construct/DirectProduct.agda

@@ -389,7 +389,6 @@ ring R S = record
       ; *-assoc          = Semiring.*-assoc Semi
       ; *-identity       = Semiring.*-identity Semi
       ; distrib          = Semiring.distrib Semi
-      ; zero             = Semiring.zero Semi
       }
   }
   where

src/Algebra/Lattice/Properties/BooleanAlgebra.agda

@@ -516,7 +516,6 @@ module XorRing
     ; *-assoc = ∧-assoc
     ; *-identity = ∧-identity
     ; distrib = ∧-distrib-⊕
-    ; zero = ∧-zero
     }
 
   ⊕-∧-isCommutativeRing : IsCommutativeRing _⊕_ _∧_ id ⊥ ⊤

src/Algebra/Morphism/RingMonomorphism.agda

@@ -150,7 +150,6 @@ isRing isRing = record
   ; *-assoc          = *-assoc R.*-isMagma R.*-assoc
   ; *-identity       = *-identity R.*-isMagma R.*-identity
   ; distrib          = distrib R.+-isGroup R.*-isMagma R.distrib
-  ; zero             = zero R.+-isGroup R.*-isMagma R.zero
   } where module R = IsRing isRing
 
 isCommutativeRing : IsCommutativeRing _≈₂_ _⊕_ _⊛_ ⊝_ 0#₂ 1#₂ →

src/Algebra/Structures.agda

@@ -806,7 +806,6 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
     *-assoc          : Associative *
     *-identity       : Identity 1# *
     distrib          : * DistributesOver +
-    zero             : Zero 0# *
 
   open IsAbelianGroup +-isAbelianGroup public
     renaming
@@ -862,10 +861,15 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
     )
 
   zeroˡ : LeftZero 0# *
-  zeroˡ = proj₁ zero
+  zeroˡ = Consequences.assoc+distribʳ+idʳ+invʳ⇒zeˡ setoid
+    +-cong *-cong +-assoc (proj₂ distrib) +-identityʳ -‿inverseʳ
 
   zeroʳ : RightZero 0# *
-  zeroʳ = proj₂ zero
+  zeroʳ = Consequences.assoc+distribˡ+idʳ+invʳ⇒zeʳ setoid
+    +-cong *-cong +-assoc (proj₁ distrib) +-identityʳ -‿inverseʳ
+
+  zero : Zero 0# *
+  zero = zeroˡ , zeroʳ
 
   isSemiringWithoutAnnihilatingZero
     : IsSemiringWithoutAnnihilatingZero + * 0# 1#

src/Algebra/Structures/Biased.agda

@@ -192,6 +192,33 @@ open IsCommutativeSemiringʳ public
 ------------------------------------------------------------------------
 -- IsRing
 
+record IsRing* (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
+  field
+    +-isAbelianGroup : IsAbelianGroup + 0# -_
+    *-isMonoid       : IsMonoid * 1#
+    distrib          : * DistributesOver +
+    zero             : Zero 0# *
+
+  isRing : IsRing + * -_ 0# 1#
+  isRing = record
+    { +-isAbelianGroup = +-isAbelianGroup
+    ; *-cong = ∙-cong
+    ; *-assoc = assoc
+    ; *-identity = identity
+    ; distrib = distrib
+    } where open IsMonoid *-isMonoid
+
+open IsRing* public
+  using () renaming (isRing to isRing*)
+
+
+
+------------------------------------------------------------------------
+-- Deprecated
+------------------------------------------------------------------------
+
+-- Version 2.0
+
 -- We can recover a ring without proving that 0# annihilates *.
 record IsRingWithoutAnnihilatingZero (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A)
                                      : Set (a ⊔ ℓ) where
@@ -224,28 +251,16 @@ record IsRingWithoutAnnihilatingZero (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A)
     ; *-assoc          = *.assoc
     ; *-identity       = *.identity
     ; distrib          = distrib
-    ; zero             = zero
     }
 
 open IsRingWithoutAnnihilatingZero public
   using () renaming (isRing to isRingWithoutAnnihilatingZero)
 
-record IsRing* (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
-  field
-    +-isAbelianGroup : IsAbelianGroup + 0# -_
-    *-isMonoid       : IsMonoid * 1#
-    distrib          : * DistributesOver +
-    zero             : Zero 0# *
-
-  isRing : IsRing + * -_ 0# 1#
-  isRing = record
-    { +-isAbelianGroup = +-isAbelianGroup
-    ; *-cong = ∙-cong
-    ; *-assoc = assoc
-    ; *-identity = identity
-    ; distrib = distrib
-    ; zero = zero
-    } where open IsMonoid *-isMonoid
-
-open IsRing* public
-  using () renaming (isRing to isRing*)
+{-# WARNING_ON_USAGE IsRingWithoutAnnihilatingZero
+"Warning: IsRingWithoutAnnihilatingZero was deprecated in v2.0.
+Please use the standard `IsRing` instead."
+#-}
+{-# WARNING_ON_USAGE isRingWithoutAnnihilatingZero
+"Warning: isRingWithoutAnnihilatingZero was deprecated in v2.0.
+Please use the standard `IsRing` instead."
+#-}

src/Data/Integer/Properties.agda

@@ -1532,7 +1532,6 @@ private
   ; *-assoc          = *-assoc
   ; *-identity       = *-identity
   ; distrib          = *-distrib-+
-  ; zero             = *-zero
   }
 
 +-*-isCommutativeRing : IsCommutativeRing _+_ _*_ -_ 0ℤ 1ℤ

src/Data/Parity/Properties.agda

@@ -371,7 +371,6 @@ p+p≡0ℙ 1ℙ = refl
   ; *-assoc          = *-assoc
   ; *-identity       = *-identity
   ; distrib          = *-distrib-+
-  ; zero             = *-zero
   }
 
 +-*-ring : Ring 0ℓ 0ℓ

src/Data/Rational/Unnormalised/Properties.agda

@@ -1387,7 +1387,6 @@ nonNeg*nonNeg⇒nonNeg p q = nonNegative
   ; *-assoc          = *-assoc
   ; *-identity       = *-identity
   ; distrib          = *-distrib-+
-  ; zero             = *-zero
   }
 
 +-*-isCommutativeRing : IsCommutativeRing _≃_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ

src/Relation/Binary/PropositionalEquality.agda

@@ -135,4 +135,3 @@ isPropositional = Irrelevant
 Please use Relation.Nullary.Irrelevant instead. "
 #-}
 
-