From c62a716f8d5b4183b2581764076d599468a6ff55 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Sat, 25 Nov 2023 18:01:52 +0800 Subject: [PATCH] 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 | 6 ++ src/Algebra/Bundles.agda | 3 + src/Algebra/Construct/DirectProduct.agda | 3 - .../Lattice/Properties/BooleanAlgebra.agda | 1 - src/Algebra/Morphism/RingMonomorphism.agda | 1 - src/Algebra/Properties/Ring.agda | 62 ++------------ src/Algebra/Properties/RingWithoutOne.agda | 31 +++++-- src/Algebra/Structures.agda | 84 ++++++------------- 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 - 13 files changed, 98 insertions(+), 152 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 25065935ce..99a3224706 100644 --- a/CHANGELOG.md +++ b/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. diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 9c1c14fec0..6b6384458a 100644 --- a/src/Algebra/Bundles.agda +++ b/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 } diff --git a/src/Algebra/Construct/DirectProduct.agda b/src/Algebra/Construct/DirectProduct.agda index ef9f377d29..3c0ec699ee 100644 --- a/src/Algebra/Construct/DirectProduct.agda +++ b/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 diff --git a/src/Algebra/Lattice/Properties/BooleanAlgebra.agda b/src/Algebra/Lattice/Properties/BooleanAlgebra.agda index 702e9fa1c8..673434a48f 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/Properties/Ring.agda b/src/Algebra/Properties/Ring.agda index 22dabbac29..461a9a040b 100644 --- a/src/Algebra/Properties/Ring.agda +++ b/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 ∎ diff --git a/src/Algebra/Properties/RingWithoutOne.agda b/src/Algebra/Properties/RingWithoutOne.agda index cab4d405cb..d81ef58477 100644 --- a/src/Algebra/Properties/RingWithoutOne.agda +++ b/src/Algebra/Properties/RingWithoutOne.agda @@ -38,10 +38,10 @@ 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)) ⟩ @@ -49,11 +49,26 @@ open AbelianGroupProperties +-abelianGroup public -‿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 ∎ diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 237e50a876..1ae7201f9a 100644 --- a/src/Algebra/Structures.agda +++ b/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 diff --git a/src/Algebra/Structures/Biased.agda b/src/Algebra/Structures/Biased.agda index cb730e9ba6..da7438b74f 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 01bdfcfe0c..ca69682633 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 13fdb3ed57..079257482b 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. " #-} -