Skip to content

Commit

Permalink
Merge branch 'master' into issue2458
Browse files Browse the repository at this point in the history
  • Loading branch information
@gallais
gallais authored Jan 29, 2025
2 parents 8d3cef6 + 34f5009 commit 355bbab
Show file tree
Hide file tree
Showing 8 changed files with 310 additions and 43 deletions.
59 changes: 59 additions & 0 deletions CHANGELOG.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,8 +26,67 @@ Deprecated names
homo ↦ ∙-homo
```

* In `Algebra.Definitions.RawMagma`:
```agda
_∣∣_ ↦ _∥_
_∤∤_ ↦ _∦_
```

* In `Algebra.Properties.Magma.Divisibility`:
```agda
∣∣-sym ↦ ∥-sym
∣∣-respˡ-≈ ↦ ∥-respˡ-≈
∣∣-respʳ-≈ ↦ ∥-respʳ-≈
∣∣-resp-≈ ↦ ∥-resp-≈
∤∤-sym -≈ ↦ ∦-sym
∤∤-respˡ-≈ ↦ ∦-respˡ-≈
∤∤-respʳ-≈ ↦ ∦-respʳ-≈
∤∤-resp-≈ ↦ ∦-resp-≈
```

* In `Algebra.Properties.Monoid.Divisibility`:
```agda
∣∣-refl ↦ ∥-refl
∣∣-reflexive ↦ ∥-reflexive
∣∣-isEquivalence ↦ ∥-isEquivalence
```

* In `Algebra.Properties.Semigroup.Divisibility`:
```agda
∣∣-trans ↦ ∥-trans
```

New modules
-----------

Additions to existing modules
-----------------------------

* In `Algebra.Construct.Pointwise`:
```agda
isNearSemiring : IsNearSemiring _≈_ _+_ _*_ 0# →
IsNearSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#)
isSemiringWithoutOne : IsSemiringWithoutOne _≈_ _+_ _*_ 0# →
IsSemiringWithoutOne (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#)
isCommutativeSemiringWithoutOne : IsCommutativeSemiringWithoutOne _≈_ _+_ _*_ 0# →
IsCommutativeSemiringWithoutOne (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#)
isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1# →
IsCommutativeSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
isIdempotentSemiring : IsIdempotentSemiring _≈_ _+_ _*_ 0# 1# →
IsIdempotentSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
isKleeneAlgebra : IsKleeneAlgebra _≈_ _+_ _*_ _⋆ 0# 1# →
IsKleeneAlgebra (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ _⋆) (lift₀ 0#) (lift₀ 1#)
isQuasiring : IsQuasiring _≈_ _+_ _*_ 0# 1# →
IsQuasiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1# →
IsCommutativeRing (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ -_) (lift₀ 0#) (lift₀ 1#)
commutativeMonoid : CommutativeMonoid c ℓ → CommutativeMonoid (a ⊔ c) (a ⊔ ℓ)
nearSemiring : NearSemiring c ℓ → NearSemiring (a ⊔ c) (a ⊔ ℓ)
semiringWithoutOne : SemiringWithoutOne c ℓ → SemiringWithoutOne (a ⊔ c) (a ⊔ ℓ)
commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne c ℓ → CommutativeSemiringWithoutOne (a ⊔ c) (a ⊔ ℓ)
commutativeSemiring : CommutativeSemiring c ℓ → CommutativeSemiring (a ⊔ c) (a ⊔ ℓ)
idempotentSemiring : IdempotentSemiring c ℓ → IdempotentSemiring (a ⊔ c) (a ⊔ ℓ)
kleeneAlgebra : KleeneAlgebra c ℓ → KleeneAlgebra (a ⊔ c) (a ⊔ ℓ)
quasiring : Quasiring c ℓ → Quasiring (a ⊔ c) (a ⊔ ℓ)
commutativeRing : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
```
5 changes: 3 additions & 2 deletions doc/style-guide.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -571,8 +571,9 @@ word within a compound word is capitalized except for the first word.

* Likewise, standard infix symbols for eg, divisibility on numeric
datatypes/algebraic structure, should be written `\|`, NOT the
unmarked `|` character. An exception to this is the *strict*
ordering relation, written using `<`, NOT `\<` as might be expected.
unmarked `|` character. Ditto. mutual divisibility `\||` etc. An
exception to this is the *strict* ordering relation, written using
`<`, NOT `\<` as might be expected.

* Since v2.0, the `Algebra` hierarchy systematically introduces
consistent symbolic notation for the negated versions of the usual
Expand Down
105 changes: 103 additions & 2 deletions src/Algebra/Construct/Pointwise.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,15 +22,14 @@ open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Structures using (IsEquivalence)


private

variable
c ℓ : Level
C : Set c
_≈_ : Rel C ℓ
ε 0# 1# : C
_⁻¹ -_ : Op₁ C
_⁻¹ -_ _⋆ : Op₁ C
_∙_ _+_ _*_ : Op₂ C

lift₀ : C → A → C
Expand Down Expand Up @@ -121,6 +120,36 @@ isAbelianGroup isAbelianGroup = record
}
where module M = IsAbelianGroup isAbelianGroup

isNearSemiring : IsNearSemiring _≈_ _+_ _*_ 0# →
IsNearSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#)
isNearSemiring isNearSemiring = record
{ +-isMonoid = isMonoid M.+-isMonoid
; *-cong = λ g h _ → M.*-cong (g _) (h _)
; *-assoc = λ f g h _ → M.*-assoc (f _) (g _) (h _)
; distribʳ = λ f g h _ → M.distribʳ (f _) (g _) (h _)
; zeroˡ = λ f _ → M.zeroˡ (f _)
}
where module M = IsNearSemiring isNearSemiring

isSemiringWithoutOne : IsSemiringWithoutOne _≈_ _+_ _*_ 0# →
IsSemiringWithoutOne (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#)
isSemiringWithoutOne isSemiringWithoutOne = record
{ +-isCommutativeMonoid = isCommutativeMonoid M.+-isCommutativeMonoid
; *-cong = λ g h _ → M.*-cong (g _) (h _)
; *-assoc = λ f g h _ → M.*-assoc (f _) (g _) (h _)
; distrib = (λ f g h _ → M.distribˡ (f _) (g _) (h _)) , (λ f g h _ → M.distribʳ (f _) (g _) (h _))
; zero = (λ f _ → M.zeroˡ (f _)) , (λ f _ → M.zeroʳ (f _))
}
where module M = IsSemiringWithoutOne isSemiringWithoutOne

isCommutativeSemiringWithoutOne : IsCommutativeSemiringWithoutOne _≈_ _+_ _*_ 0# →
IsCommutativeSemiringWithoutOne (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#)
isCommutativeSemiringWithoutOne isCommutativeSemiringWithoutOne = record
{ isSemiringWithoutOne = isSemiringWithoutOne M.isSemiringWithoutOne
; *-comm = λ f g _ → M.*-comm (f _) (g _)
}
where module M = IsCommutativeSemiringWithoutOne isCommutativeSemiringWithoutOne

isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _≈_ _+_ _*_ 0# 1# →
IsSemiringWithoutAnnihilatingZero (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
isSemiringWithoutAnnihilatingZero isSemiringWithoutAnnihilatingZero = record
Expand All @@ -140,6 +169,44 @@ isSemiring isSemiring = record
}
where module M = IsSemiring isSemiring

isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1# →
IsCommutativeSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
isCommutativeSemiring isCommutativeSemiring = record
{ isSemiring = isSemiring M.isSemiring
; *-comm = λ f g _ → M.*-comm (f _) (g _)
}
where module M = IsCommutativeSemiring isCommutativeSemiring

isIdempotentSemiring : IsIdempotentSemiring _≈_ _+_ _*_ 0# 1# →
IsIdempotentSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
isIdempotentSemiring isIdempotentSemiring = record
{ isSemiring = isSemiring M.isSemiring
; +-idem = λ f _ → M.+-idem (f _)
}
where module M = IsIdempotentSemiring isIdempotentSemiring

isKleeneAlgebra : IsKleeneAlgebra _≈_ _+_ _*_ _⋆ 0# 1# →
IsKleeneAlgebra (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ _⋆) (lift₀ 0#) (lift₀ 1#)
isKleeneAlgebra isKleeneAlgebra = record
{ isIdempotentSemiring = isIdempotentSemiring M.isIdempotentSemiring
; starExpansive = (λ f _ → M.starExpansiveˡ (f _)) , λ f _ → M.starExpansiveʳ (f _)
; starDestructive = (λ f g h i _ → M.starDestructiveˡ (f _) (g _) (h _) (i _))
, (λ f g h i _ → M.starDestructiveʳ (f _) (g _) (h _) (i _))
}
where module M = IsKleeneAlgebra isKleeneAlgebra

isQuasiring : IsQuasiring _≈_ _+_ _*_ 0# 1# →
IsQuasiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
isQuasiring isQuasiring = record
{ +-isMonoid = isMonoid M.+-isMonoid
; *-cong = λ g h _ → M.*-cong (g _) (h _)
; *-assoc = λ f g h _ → M.*-assoc (f _) (g _) (h _)
; *-identity = (λ f _ → M.*-identityˡ (f _)) , λ f _ → M.*-identityʳ (f _)
; distrib = (λ f g h _ → M.distribˡ (f _) (g _) (h _)) , λ f g h _ → M.distribʳ (f _) (g _) (h _)
; zero = (λ f _ → M.zeroˡ (f _)) , λ f _ → M.zeroʳ (f _)
}
where module M = IsQuasiring isQuasiring

isRing : IsRing _≈_ _+_ _*_ -_ 0# 1# →
IsRing (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ -_) (lift₀ 0#) (lift₀ 1#)
isRing isRing = record
Expand All @@ -151,6 +218,13 @@ isRing isRing = record
}
where module M = IsRing isRing

isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1# →
IsCommutativeRing (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ -_) (lift₀ 0#) (lift₀ 1#)
isCommutativeRing isCommutativeRing = record
{ isRing = isRing M.isRing
; *-comm = λ f g _ → M.*-comm (f _) (g _)
}
where module M = IsCommutativeRing isCommutativeRing

------------------------------------------------------------------------
-- Bundles
Expand All @@ -170,15 +244,42 @@ commutativeSemigroup m = record { isCommutativeSemigroup = isCommutativeSemigrou
monoid : Monoid c ℓ → Monoid (a ⊔ c) (a ⊔ ℓ)
monoid m = record { isMonoid = isMonoid (Monoid.isMonoid m) }

commutativeMonoid : CommutativeMonoid c ℓ → CommutativeMonoid (a ⊔ c) (a ⊔ ℓ)
commutativeMonoid m = record { isCommutativeMonoid = isCommutativeMonoid (CommutativeMonoid.isCommutativeMonoid m) }

group : Group c ℓ → Group (a ⊔ c) (a ⊔ ℓ)
group m = record { isGroup = isGroup (Group.isGroup m) }

abelianGroup : AbelianGroup c ℓ → AbelianGroup (a ⊔ c) (a ⊔ ℓ)
abelianGroup m = record { isAbelianGroup = isAbelianGroup (AbelianGroup.isAbelianGroup m) }

nearSemiring : NearSemiring c ℓ → NearSemiring (a ⊔ c) (a ⊔ ℓ)
nearSemiring m = record { isNearSemiring = isNearSemiring (NearSemiring.isNearSemiring m) }

semiringWithoutOne : SemiringWithoutOne c ℓ → SemiringWithoutOne (a ⊔ c) (a ⊔ ℓ)
semiringWithoutOne m = record { isSemiringWithoutOne = isSemiringWithoutOne (SemiringWithoutOne.isSemiringWithoutOne m) }

commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne c ℓ → CommutativeSemiringWithoutOne (a ⊔ c) (a ⊔ ℓ)
commutativeSemiringWithoutOne m = record
{ isCommutativeSemiringWithoutOne = isCommutativeSemiringWithoutOne (CommutativeSemiringWithoutOne.isCommutativeSemiringWithoutOne m) }

semiring : Semiring c ℓ → Semiring (a ⊔ c) (a ⊔ ℓ)
semiring m = record { isSemiring = isSemiring (Semiring.isSemiring m) }

commutativeSemiring : CommutativeSemiring c ℓ → CommutativeSemiring (a ⊔ c) (a ⊔ ℓ)
commutativeSemiring m = record { isCommutativeSemiring = isCommutativeSemiring (CommutativeSemiring.isCommutativeSemiring m) }

idempotentSemiring : IdempotentSemiring c ℓ → IdempotentSemiring (a ⊔ c) (a ⊔ ℓ)
idempotentSemiring m = record { isIdempotentSemiring = isIdempotentSemiring (IdempotentSemiring.isIdempotentSemiring m) }

kleeneAlgebra : KleeneAlgebra c ℓ → KleeneAlgebra (a ⊔ c) (a ⊔ ℓ)
kleeneAlgebra m = record { isKleeneAlgebra = isKleeneAlgebra (KleeneAlgebra.isKleeneAlgebra m) }

quasiring : Quasiring c ℓ → Quasiring (a ⊔ c) (a ⊔ ℓ)
quasiring m = record { isQuasiring = isQuasiring (Quasiring.isQuasiring m) }

ring : Ring c ℓ → Ring (a ⊔ c) (a ⊔ ℓ)
ring m = record { isRing = isRing (Ring.isRing m) }

commutativeRing : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
commutativeRing m = record { isCommutativeRing = isCommutativeRing (CommutativeRing.isCommutativeRing m) }
35 changes: 28 additions & 7 deletions src/Algebra/Definitions/RawMagma.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@
{-# OPTIONS --cubical-compatible --safe #-}

open import Algebra.Bundles.Raw using (RawMagma)
open import Data.Product.Base using (_×_; ∃)
open import Data.Product.Base using (_×_)
open import Level using (_⊔_)
open import Relation.Binary.Core using (Rel)
open import Relation.Nullary.Negation.Core using (¬_)
Expand All @@ -25,7 +25,7 @@ open RawMagma M renaming (Carrier to A)
------------------------------------------------------------------------
-- Divisibility

infix 5 _∣ˡ_ _∤ˡ_ _∣ʳ_ _∤ʳ_ _∣_ _∤_ _∣∣_ _∤∤_
infix 5 _∣ˡ_ _∤ˡ_ _∣ʳ_ _∤ʳ_ _∣_ _∤_ _∥_ _∦_

-- Divisibility from the left.
--
Expand All @@ -34,7 +34,7 @@ infix 5 _∣ˡ_ _∤ˡ_ _∣ʳ_ _∤ʳ_ _∣_ _∤_ _∣∣_ _∤∤_
-- make the use of pattern synonyms more ergonomic (see #2216 for
-- further details). The record field names are not designed to be
-- used explicitly and indeed aren't re-exported publicly by
-- `Algebra.X.Properties.Divisibility` modules.
-- `Algebra.Properties.X.Divisibility` modules.

record _∣ˡ_ (x y : A) : Set (a ⊔ ℓ) where
constructor _,_
Expand Down Expand Up @@ -79,8 +79,29 @@ x ∤ y = ¬ x ∣ y
-- Example: for ℕ this is equivalent to x ≡ y,
-- for ℤ this is equivalent to (x ≡ y or x ≡ - y).

_∣∣_ : Rel A (a ⊔ ℓ)
x ∣∣ y = x ∣ y × y ∣ x
_∥_ : Rel A (a ⊔ ℓ)
x ∥ y = x ∣ y × y ∣ x

_∦_ : Rel A (a ⊔ ℓ)
x ∦ y = ¬ x ∥ y


------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 2.3

_∣∣_ = _∥_
{-# WARNING_ON_USAGE _∣∣_
"Warning: _∣∣_ was deprecated in v2.3.
Please use _∥_ instead."
#-}
_∤∤_ = _∦_
{-# WARNING_ON_USAGE _∤∤_
"Warning: _∤∤_ was deprecated in v2.3.
Please use _∦_ instead."
#-}

_∤∤_ : Rel A (a ⊔ ℓ)
x ∤∤ y = ¬ x ∣∣ y
Loading

0 comments on commit 355bbab

Please sign in to comment.