Fix #2195 by removing redundant zero from IsRing (#2209)

* Fix #2195 by removing redundant zero from IsRing

* Moved proofs eariler to IsSemiringWithoutOne

* Updated CHANGELOG

* Fix bug

* Refactored Properties.Ring

CHANGELOG.md

@@ -33,6 +33,12 @@ Highlights
 Bug-fixes
 ---------
 
+* In `Algebra.Structures` the records `IsRing` and `IsRingWithoutOne` 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/Bundles.agda

@@ -944,6 +944,9 @@ record Ring c ℓ : Set (suc (c ⊔ ℓ)) where
   +-abelianGroup : AbelianGroup _ _
   +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup }
 
+  ringWithoutOne : RingWithoutOne _ _
+  ringWithoutOne = record { isRingWithoutOne = isRingWithoutOne }
+
   semiring : Semiring _ _
   semiring = record { isSemiring = isSemiring }
 

src/Algebra/Construct/DirectProduct.agda

@@ -335,8 +335,6 @@ ringWithoutOne R S = record
       ; *-assoc          = Semigroup.assoc (semigroup R.*-semigroup S.*-semigroup)
       ; distrib          = (λ x y z → (R.distribˡ , S.distribˡ) <*> x <*> y <*> z)
                             , (λ x y z → (R.distribʳ , S.distribʳ) <*> x <*> y <*> z)
-      ; zero             = uncurry (λ x y → R.zeroˡ x , S.zeroˡ y)
-                            , uncurry (λ x y → R.zeroʳ x , S.zeroʳ y)
       }
 
   } where module R = RingWithoutOne R; module S = RingWithoutOne S
@@ -389,7 +387,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/Properties/Ring.agda

@@ -12,73 +12,21 @@ module Algebra.Properties.Ring {r₁ r₂} (R : Ring r₁ r₂) where
 
 open Ring R
 
-import Algebra.Properties.AbelianGroup as AbelianGroupProperties
+import Algebra.Properties.RingWithoutOne as RingWithoutOneProperties
 open import Function.Base using (_$_)
 open import Relation.Binary.Reasoning.Setoid setoid
 open import Algebra.Definitions _≈_
 
 ------------------------------------------------------------------------
--- Export properties of abelian groups
+-- Export properties of rings without a 1#.
 
-open AbelianGroupProperties +-abelianGroup public
-  renaming
-  ( ε⁻¹≈ε            to -0#≈0#
-  ; ∙-cancelˡ        to +-cancelˡ
-  ; ∙-cancelʳ        to +-cancelʳ
-  ; ∙-cancel         to +-cancel
-  ; ⁻¹-involutive    to -‿involutive
-  ; ⁻¹-injective     to -‿injective
-  ; ⁻¹-anti-homo-∙   to -‿anti-homo-+
-  ; identityˡ-unique to +-identityˡ-unique
-  ; identityʳ-unique to +-identityʳ-unique
-  ; identity-unique  to +-identity-unique
-  ; inverseˡ-unique  to +-inverseˡ-unique
-  ; inverseʳ-unique  to +-inverseʳ-unique
-  ; ⁻¹-∙-comm        to -‿+-comm
-  )
+open RingWithoutOneProperties ringWithoutOne public
 
 ------------------------------------------------------------------------
--- Properties of -_
-
--‿distribˡ-* : ∀ x y → - (x * y) ≈ - x * y
--‿distribˡ-* x y = sym $ begin
-  - x * y                        ≈⟨ sym $ +-identityʳ _ ⟩
-  - x * y + 0#                   ≈⟨ +-congˡ $ sym (-‿inverseʳ _) ⟩
-  - x * y + (x * y + - (x * y))  ≈⟨ sym $ +-assoc _ _ _  ⟩
-  - x * y + x * y + - (x * y)    ≈⟨ +-congʳ $ sym (distribʳ _ _ _) ⟩
-  (- x + x) * y + - (x * y)      ≈⟨ +-congʳ $ *-congʳ $ -‿inverseˡ _ ⟩
-  0# * y + - (x * y)             ≈⟨ +-congʳ $ zeroˡ _ ⟩
-  0# + - (x * y)                 ≈⟨ +-identityˡ _ ⟩
-  - (x * y)                      ∎
-
--‿distribʳ-* : ∀ x y → - (x * y) ≈ x * - y
--‿distribʳ-* x y = sym $ begin
-  x * - y                        ≈⟨ sym $ +-identityˡ _ ⟩
-  0# + x * - y                   ≈⟨ +-congʳ $ sym (-‿inverseˡ _) ⟩
-  - (x * y) + x * y + x * - y    ≈⟨ +-assoc _ _ _  ⟩
-  - (x * y) + (x * y + x * - y)  ≈⟨ +-congˡ $ sym (distribˡ _ _ _)  ⟩
-  - (x * y) + x * (y + - y)      ≈⟨ +-congˡ $ *-congˡ $ -‿inverseʳ _ ⟩
-  - (x * y) + x * 0#             ≈⟨ +-congˡ $ zeroʳ _ ⟩
-  - (x * y) + 0#                 ≈⟨ +-identityʳ _ ⟩
-  - (x * y)                      ∎
+-- Extra properties of 1#
 
 -1*x≈-x : ∀ x → - 1# * x ≈ - x
 -1*x≈-x x = begin
-  - 1# * x    ≈⟨ sym (-‿distribˡ-* 1# x ) ⟩
+  - 1# * x    ≈⟨ -‿distribˡ-* 1# x ⟨
   - (1# * x)  ≈⟨ -‿cong ( *-identityˡ x ) ⟩
   - x         ∎
-
-x+x≈x⇒x≈0 : ∀ x → x + x ≈ x → x ≈ 0#
-x+x≈x⇒x≈0 x eq = +-identityˡ-unique x x eq
-
-x[y-z]≈xy-xz : ∀ x y z → x * (y - z) ≈ x * y - x * z
-x[y-z]≈xy-xz x y z = begin
-  x * (y - z)      ≈⟨ distribˡ x y (- z) ⟩
-  x * y + x * - z  ≈⟨ +-congˡ (sym (-‿distribʳ-* x z)) ⟩
-  x * y - x * z    ∎
-
-[y-z]x≈yx-zx : ∀ x y z → (y - z) * x ≈ (y * x) - (z * x)
-[y-z]x≈yx-zx x y z = begin
-  (y - z) * x      ≈⟨ distribʳ x y (- z) ⟩
-  y * x + - z * x  ≈⟨ +-congˡ (sym (-‿distribˡ-* z x)) ⟩
-  y * x - z * x    ∎

src/Algebra/Properties/RingWithoutOne.agda

@@ -38,22 +38,37 @@ open AbelianGroupProperties +-abelianGroup public
 
 -‿distribˡ-* : ∀ x y → - (x * y) ≈ - x * y
 -‿distribˡ-* x y = sym $ begin
-  - x * y                        ≈⟨ sym $ +-identityʳ (- x * y) ⟩
-  - x * y + 0#                   ≈⟨ +-congˡ $ sym ( -‿inverseʳ (x * y) ) ⟩
-  - x * y + (x * y + - (x * y))  ≈⟨ sym $ +-assoc (- x * y) (x * y) (- (x * y))  ⟩
-  - x * y + x * y + - (x * y)    ≈⟨ +-congʳ $ sym ( distribʳ y (- x) x ) ⟩
+  - x * y                        ≈⟨ +-identityʳ (- x * y) ⟨
+  - x * y + 0#                   ≈⟨ +-congˡ $ -‿inverseʳ (x * y) ⟨
+  - x * y + (x * y + - (x * y))  ≈⟨ +-assoc (- x * y) (x * y) (- (x * y)) ⟨
+  - x * y + x * y + - (x * y)    ≈⟨ +-congʳ $ distribʳ y (- x) x ⟨
   (- x + x) * y + - (x * y)      ≈⟨ +-congʳ $ *-congʳ $ -‿inverseˡ x ⟩
   0# * y + - (x * y)             ≈⟨ +-congʳ $ zeroˡ y ⟩
   0# + - (x * y)                 ≈⟨ +-identityˡ (- (x * y)) ⟩
   - (x * y)                      ∎
 
 -‿distribʳ-* : ∀ x y → - (x * y) ≈ x * - y
 -‿distribʳ-* x y = sym $ begin
-  x * - y                        ≈⟨ sym $ +-identityˡ (x * (- y)) ⟩
-  0# + x * - y                   ≈⟨ +-congʳ $ sym ( -‿inverseˡ (x * y) ) ⟩
-  - (x * y) + x * y + x * - y    ≈⟨ +-assoc (- (x * y)) (x * y) (x * (- y)) ⟩
-  - (x * y) + (x * y + x * - y)  ≈⟨ +-congˡ $ sym ( distribˡ x y ( - y) )  ⟩
+  x * - y                        ≈⟨ +-identityˡ (x * - y) ⟨
+  0# + x * - y                   ≈⟨ +-congʳ $ -‿inverseˡ (x * y) ⟨
+  - (x * y) + x * y + x * - y    ≈⟨ +-assoc (- (x * y)) (x * y) (x * - y) ⟩
+  - (x * y) + (x * y + x * - y)  ≈⟨ +-congˡ $ distribˡ x y (- y) ⟨
   - (x * y) + x * (y + - y)      ≈⟨ +-congˡ $ *-congˡ $ -‿inverseʳ y ⟩
   - (x * y) + x * 0#             ≈⟨ +-congˡ $ zeroʳ x ⟩
   - (x * y) + 0#                 ≈⟨ +-identityʳ (- (x * y)) ⟩
   - (x * y)                      ∎
+
+x+x≈x⇒x≈0 : ∀ x → x + x ≈ x → x ≈ 0#
+x+x≈x⇒x≈0 x eq = +-identityˡ-unique x x eq
+
+x[y-z]≈xy-xz : ∀ x y z → x * (y - z) ≈ x * y - x * z
+x[y-z]≈xy-xz x y z = begin
+  x * (y - z)      ≈⟨ distribˡ x y (- z) ⟩
+  x * y + x * - z  ≈⟨ +-congˡ (sym (-‿distribʳ-* x z)) ⟩
+  x * y - x * z    ∎
+
+[y-z]x≈yx-zx : ∀ x y z → (y - z) * x ≈ (y * x) - (z * x)
+[y-z]x≈yx-zx x y z = begin
+  (y - z) * x      ≈⟨ distribʳ x y (- z) ⟩
+  y * x + - z * x  ≈⟨ +-congˡ (sym (-‿distribˡ-* z x)) ⟩
+  y * x - z * x    ∎

src/Algebra/Structures.agda

@@ -651,7 +651,6 @@ record IsRingWithoutOne (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ
     *-cong           : Congruent₂ *
     *-assoc          : Associative *
     distrib          : * DistributesOver +
-    zero             : Zero 0# *
 
   open IsAbelianGroup +-isAbelianGroup public
     renaming
@@ -679,23 +678,28 @@ record IsRingWithoutOne (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ
     ; isGroup                 to +-isGroup
     )
 
-  *-isMagma : IsMagma *
-  *-isMagma = record
-    { isEquivalence = isEquivalence
-    ; ∙-cong        = *-cong
-    }
+  distribˡ : * DistributesOverˡ +
+  distribˡ = proj₁ distrib
+
+  distribʳ : * DistributesOverʳ +
+  distribʳ = proj₂ distrib
 
   zeroˡ : LeftZero 0# *
-  zeroˡ = proj₁ zero
+  zeroˡ = Consequences.assoc+distribʳ+idʳ+invʳ⇒zeˡ setoid
+    +-cong *-cong +-assoc distribʳ +-identityʳ -‿inverseʳ
 
   zeroʳ : RightZero 0# *
-  zeroʳ = proj₂ zero
+  zeroʳ = Consequences.assoc+distribˡ+idʳ+invʳ⇒zeʳ setoid
+    +-cong *-cong +-assoc distribˡ +-identityʳ -‿inverseʳ
 
-  distribˡ : * DistributesOverˡ +
-  distribˡ = proj₁ distrib
+  zero : Zero 0# *
+  zero = zeroˡ , zeroʳ
 
-  distribʳ : * DistributesOverʳ +
-  distribʳ = proj₂ distrib
+  *-isMagma : IsMagma *
+  *-isMagma = record
+    { isEquivalence = isEquivalence
+    ; ∙-cong        = *-cong
+    }
 
   *-isSemigroup : IsSemigroup *
   *-isSemigroup = record
@@ -806,45 +810,17 @@ 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
-    ( assoc                   to +-assoc
-    ; ∙-cong                  to +-cong
-    ; ∙-congˡ                 to +-congˡ
-    ; ∙-congʳ                 to +-congʳ
-    ; identity                to +-identity
-    ; identityˡ               to +-identityˡ
-    ; identityʳ               to +-identityʳ
-    ; inverse                 to -‿inverse
-    ; inverseˡ                to -‿inverseˡ
-    ; inverseʳ                to -‿inverseʳ
-    ; ⁻¹-cong                 to -‿cong
-    ; comm                    to +-comm
-    ; isMagma                 to +-isMagma
-    ; isSemigroup             to +-isSemigroup
-    ; isMonoid                to +-isMonoid
-    ; isUnitalMagma           to +-isUnitalMagma
-    ; isCommutativeMagma      to +-isCommutativeMagma
-    ; isCommutativeMonoid     to +-isCommutativeMonoid
-    ; isCommutativeSemigroup  to +-isCommutativeSemigroup
-    ; isInvertibleMagma       to +-isInvertibleMagma
-    ; isInvertibleUnitalMagma to +-isInvertibleUnitalMagma
-    ; isGroup                 to +-isGroup
-    )
-
-  *-isMagma : IsMagma *
-  *-isMagma = record
-    { isEquivalence = isEquivalence
-    ; ∙-cong        = *-cong
+  isRingWithoutOne : IsRingWithoutOne + * -_ 0#
+  isRingWithoutOne = record
+    { +-isAbelianGroup = +-isAbelianGroup
+    ; *-cong  = *-cong
+    ; *-assoc = *-assoc
+    ; distrib = distrib
     }
 
-  *-isSemigroup : IsSemigroup *
-  *-isSemigroup = record
-    { isMagma = *-isMagma
-    ; assoc   = *-assoc
-    }
+  open IsRingWithoutOne isRingWithoutOne public
+    hiding (+-isAbelianGroup; *-cong; *-assoc; distrib)
 
   *-isMonoid : IsMonoid * 1#
   *-isMonoid = record
@@ -855,18 +831,10 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
   open IsMonoid *-isMonoid public
     using ()
     renaming
-    ( ∙-congˡ     to *-congˡ
-    ; ∙-congʳ     to *-congʳ
-    ; identityˡ   to *-identityˡ
+    ( identityˡ   to *-identityˡ
     ; identityʳ   to *-identityʳ
     )
 
-  zeroˡ : LeftZero 0# *
-  zeroˡ = proj₁ zero
-
-  zeroʳ : RightZero 0# *
-  zeroʳ = proj₂ zero
-
   isSemiringWithoutAnnihilatingZero
     : IsSemiringWithoutAnnihilatingZero + * 0# 1#
   isSemiringWithoutAnnihilatingZero = record
@@ -885,7 +853,7 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
     }
 
   open IsSemiring isSemiring public
-    using (distribˡ; distribʳ; isNearSemiring; isSemiringWithoutOne)
+    using (isNearSemiring; isSemiringWithoutOne)
 
 
 record IsCommutativeRing

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ℓ