From e46ab4d329a881ca2f4f2208d3506d1f6e21079f Mon Sep 17 00:00:00 2001 From: matthewdaggitt Date: Fri, 24 Nov 2023 11:21:36 +0800 Subject: [PATCH] Fix #2195 by removing redundant zero from IsRing --- CHANGELOG.md | 6 ++ src/Algebra/Construct/DirectProduct.agda | 1 - .../Lattice/Properties/BooleanAlgebra.agda | 1 - src/Algebra/Morphism/RingMonomorphism.agda | 1 - src/Algebra/Structures.agda | 10 +++- src/Algebra/Structures/Biased.agda | 55 ++++++++++++------- src/Data/Integer/Properties.agda | 1 - src/Data/Parity/Properties.agda | 1 - .../Rational/Unnormalised/Properties.agda | 1 - .../Binary/PropositionalEquality.agda | 1 - 10 files changed, 48 insertions(+), 30 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 51966c2176..2db2c7fa4e 100644 --- a/CHANGELOG.md +++ b/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. diff --git a/src/Algebra/Construct/DirectProduct.agda b/src/Algebra/Construct/DirectProduct.agda index ef9f377d29..72f0cab3b1 100644 --- a/src/Algebra/Construct/DirectProduct.agda +++ b/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 diff --git a/src/Algebra/Lattice/Properties/BooleanAlgebra.agda b/src/Algebra/Lattice/Properties/BooleanAlgebra.agda index 450527ddc0..6560fa0836 100644 --- a/src/Algebra/Lattice/Properties/BooleanAlgebra.agda +++ b/src/Algebra/Lattice/Properties/BooleanAlgebra.agda @@ -516,7 +516,6 @@ module XorRing ; *-assoc = ∧-assoc ; *-identity = ∧-identity ; distrib = ∧-distrib-⊕ - ; zero = ∧-zero } ⊕-∧-isCommutativeRing : IsCommutativeRing _⊕_ _∧_ id ⊥ ⊤ diff --git a/src/Algebra/Morphism/RingMonomorphism.agda b/src/Algebra/Morphism/RingMonomorphism.agda index 9230c802a9..35a191a0f8 100644 --- a/src/Algebra/Morphism/RingMonomorphism.agda +++ b/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#₂ → diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index ed55226d67..fd4d0dec2e 100644 --- a/src/Algebra/Structures.agda +++ b/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# diff --git a/src/Algebra/Structures/Biased.agda b/src/Algebra/Structures/Biased.agda index c0c6994e3f..120deb7a14 100644 --- a/src/Algebra/Structures/Biased.agda +++ b/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." +#-} diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index 43152bceee..b10e223288 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -1532,7 +1532,6 @@ private ; *-assoc = *-assoc ; *-identity = *-identity ; distrib = *-distrib-+ - ; zero = *-zero } +-*-isCommutativeRing : IsCommutativeRing _+_ _*_ -_ 0ℤ 1ℤ diff --git a/src/Data/Parity/Properties.agda b/src/Data/Parity/Properties.agda index 0d5d29607a..570f2db555 100644 --- a/src/Data/Parity/Properties.agda +++ b/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ℓ diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index dce11c3f21..5a18639aae 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/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ℚᵘ diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda index 7ba3825e31..6c2eb19bed 100644 --- a/src/Relation/Binary/PropositionalEquality.agda +++ b/src/Relation/Binary/PropositionalEquality.agda @@ -135,4 +135,3 @@ isPropositional = Irrelevant Please use Relation.Nullary.Irrelevant instead. " #-} -