Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix #2195 by removing redundant zero from IsRing #2209

Merged
merged 7 commits into from
Nov 26, 2023
Merged
Show file tree
Hide file tree
Changes from 4 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,12 @@ Highlights
Bug-fixes
---------

* In `Algebra.Structures` the records `IsRing` and `IsRingWithoutOne` contained an unnecessary field
jamesmckinna marked this conversation as resolved.
Show resolved Hide resolved
`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.
Expand Down
3 changes: 0 additions & 3 deletions src/Algebra/Construct/DirectProduct.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
1 change: 0 additions & 1 deletion src/Algebra/Lattice/Properties/BooleanAlgebra.agda
Original file line number Diff line number Diff line change
Expand Up @@ -516,7 +516,6 @@ module XorRing
; *-assoc = ∧-assoc
; *-identity = ∧-identity
; distrib = ∧-distrib-⊕
; zero = ∧-zero
}

⊕-∧-isCommutativeRing : IsCommutativeRing _⊕_ _∧_ id ⊥ ⊤
Expand Down
1 change: 0 additions & 1 deletion src/Algebra/Morphism/RingMonomorphism.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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#₂ →
Expand Down
84 changes: 26 additions & 58 deletions src/Algebra/Structures.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down
55 changes: 35 additions & 20 deletions src/Algebra/Structures/Biased.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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# *
Copy link
Contributor

@jamesmckinna jamesmckinna Jan 12, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Too late! But is this field also now redundant as a consequence of this issue/PR?
Raised as issue #2253


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
Expand Down Expand Up @@ -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."
#-}
1 change: 0 additions & 1 deletion src/Data/Integer/Properties.agda
Original file line number Diff line number Diff line change
Expand Up @@ -1532,7 +1532,6 @@ private
; *-assoc = *-assoc
; *-identity = *-identity
; distrib = *-distrib-+
; zero = *-zero
}

+-*-isCommutativeRing : IsCommutativeRing _+_ _*_ -_ 0ℤ 1ℤ
Expand Down
1 change: 0 additions & 1 deletion src/Data/Parity/Properties.agda
Original file line number Diff line number Diff line change
Expand Up @@ -371,7 +371,6 @@ p+p≡0ℙ 1ℙ = refl
; *-assoc = *-assoc
; *-identity = *-identity
; distrib = *-distrib-+
; zero = *-zero
}

+-*-ring : Ring 0ℓ 0ℓ
Expand Down
1 change: 0 additions & 1 deletion src/Data/Rational/Unnormalised/Properties.agda
Original file line number Diff line number Diff line change
Expand Up @@ -1387,7 +1387,6 @@ nonNeg*nonNeg⇒nonNeg p q = nonNegative
; *-assoc = *-assoc
; *-identity = *-identity
; distrib = *-distrib-+
; zero = *-zero
}

+-*-isCommutativeRing : IsCommutativeRing _≃_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ
Expand Down
1 change: 0 additions & 1 deletion src/Relation/Binary/PropositionalEquality.agda
Original file line number Diff line number Diff line change
Expand Up @@ -135,4 +135,3 @@ isPropositional = Irrelevant
Please use Relation.Nullary.Irrelevant instead. "
#-}