Skip to content

[ new ] added IsMagma, RawMagma and Magma to Algebra #456

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.

Sign up for GitHub

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

Merged
merged 6 commits into from
Nov 12, 2018
Merged

[ new ] added IsMagma, RawMagma and Magma to Algebra #456

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
5574758
Added IsMagma, RawMagma and Magma to Algebra
MatthewDaggitt Sep 7, 2018
827f983
Merge branch 'master' into moreAlgebraicStructures
MatthewDaggitt Nov 4, 2018
e529c7b
Added CHANGELOG entry and deprecated rawSemigroup
MatthewDaggitt Nov 4, 2018
2345b8d
Re-exported magmas and rawMagmas out of various structures
MatthewDaggitt Nov 4, 2018
7a82c92
Merge branch 'master' into moreAlgebraicStructures
MatthewDaggitt Nov 12, 2018
8991d8c
Merge branch 'master' into moreAlgebraicStructures
MatthewDaggitt Nov 12, 2018
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
27 changes: 22 additions & 5 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,12 @@ Splitting up `Data.Maybe` into the standard hierarchy.
Eq-isDecEquivalence ↦ isDecEquivalence
```

#### Changes to the algebra hierarchy

* Added `Magma` and `IsMagma` to the algebra hierarchy.

* The name `RawSemigroup` in `Algebra` has been deprecated in favour of `RawMagma`.

#### Relaxation of ring solvers requirements

* In the ring solvers below, the assumption that equality is `Decidable`
Expand Down Expand Up @@ -79,11 +85,27 @@ Deprecated features
Other minor additions
---------------------

* Added new records to `Algebra`:
```agda
record RawMagma c ℓ : Set (suc (c ⊔ ℓ))
record Magma c ℓ : Set (suc (c ⊔ ℓ))
```

* Added new proof to `Algebra.FunctionProperties.Consequences`:
```agda
wlog : Commutative f → Total _R_ → (∀ a b → a R b → P (f a b)) → ∀ a b → P (f a b)
```

* Added new operator to `Algebra.Solver.Ring`.
```agda
_:×_
```

* Added new records to `Algebra.Structures`:
```agda
record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ)
```

* Added new functions to `Codata.Stream`:
```agda
splitAt : (n : ℕ) → Stream A ∞ → Vec A n × Stream A ∞
Expand All @@ -96,11 +118,6 @@ Other minor additions
splitAt-map : splitAt n (map f xs) ≡ map (map f) (map f) (splitAt n xs)
```

* Added new proof to `Algebra.FunctionProperties.Consequences`:
```agda
wlog : Commutative f → Total _R_ → (∀ a b → a R b → P (f a b)) → ∀ a b → P (f a b)
```

* Added new function to `Data.Fin.Base`:
```agda
cast : m ≡ n → Fin m → Fin n
Expand Down
190 changes: 121 additions & 69 deletions src/Algebra.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,15 +14,32 @@ open import Function
open import Level

------------------------------------------------------------------------
-- Semigroups
-- Magmas

record RawMagma c ℓ : Set (suc (c ⊔ ℓ)) where
infixl 7 _∙_
infix 4 _≈_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ
_∙_ : Op₂ Carrier

record RawSemigroup c ℓ : Set (suc (c ⊔ ℓ)) where
record Magma c ℓ : Set (suc (c ⊔ ℓ)) where
infixl 7 _∙_
infix 4 _≈_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ
_∙_ : Op₂ Carrier
isMagma : IsMagma _≈_ _∙_

open IsMagma isMagma public

rawMagma : RawMagma _ _
rawMagma = record { _≈_ = _≈_; _∙_ = _∙_ }

------------------------------------------------------------------------
-- Semigroups

record Semigroup c ℓ : Set (suc (c ⊔ ℓ)) where
infixl 7 _∙_
Expand All @@ -35,11 +52,10 @@ record Semigroup c ℓ : Set (suc (c ⊔ ℓ)) where

open IsSemigroup isSemigroup public

rawSemigroup : RawSemigroup _ _
rawSemigroup = record
{ _≈_ = _≈_
; _∙_ = _∙_
}
magma : Magma c ℓ
magma = record { isMagma = isMagma }

open Magma magma public using (rawMagma)

record Band c ℓ : Set (suc (c ⊔ ℓ)) where
infixl 7 _∙_
Expand All @@ -55,7 +71,7 @@ record Band c ℓ : Set (suc (c ⊔ ℓ)) where
semigroup : Semigroup c ℓ
semigroup = record { isSemigroup = isSemigroup }

open Semigroup semigroup public using (rawSemigroup)
open Semigroup semigroup public using (magma; rawMagma)

------------------------------------------------------------------------
-- Monoids
Expand Down Expand Up @@ -87,11 +103,9 @@ record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where
semigroup = record { isSemigroup = isSemigroup }

rawMonoid : RawMonoid _ _
rawMonoid = record
{ _≈_ = _≈_
; _∙_ = _∙_
; ε = ε
}
rawMonoid = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε}

open Semigroup semigroup public using (rawMagma; magma)

record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
infixl 7 _∙_
Expand All @@ -108,7 +122,7 @@ record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
monoid : Monoid _ _
monoid = record { isMonoid = isMonoid }

open Monoid monoid public using (semigroup; rawMonoid)
open Monoid monoid public using (rawMagma; magma; semigroup; rawMonoid)

record IdempotentCommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
infixl 7 _∙_
Expand All @@ -126,7 +140,7 @@ record IdempotentCommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }

open CommutativeMonoid commutativeMonoid public
using (semigroup; rawMonoid; monoid)
using (rawMagma; magma; semigroup; rawMonoid; monoid)

------------------------------------------------------------------------
-- Groups
Expand Down Expand Up @@ -157,17 +171,12 @@ record Group c ℓ : Set (suc (c ⊔ ℓ)) where
open IsGroup isGroup public

rawGroup : RawGroup _ _
rawGroup = record
{ _≈_ = _≈_
; _∙_ = _∙_
; ε = ε
; _⁻¹ = _⁻¹
}
rawGroup = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε; _⁻¹ = _⁻¹}

monoid : Monoid _ _
monoid = record { isMonoid = isMonoid }

open Monoid monoid public using (semigroup; rawMonoid)
open Monoid monoid public using (rawMagma; magma; semigroup; rawMonoid)

record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
infix 8 _⁻¹
Expand All @@ -187,7 +196,7 @@ record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
group = record { isGroup = isGroup }

open Group group public
using (semigroup; monoid; rawMonoid; rawGroup)
using (rawMagma; magma; semigroup; monoid; rawMonoid; rawGroup)

commutativeMonoid : CommutativeMonoid _ _
commutativeMonoid =
Expand Down Expand Up @@ -226,13 +235,24 @@ record NearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
+-monoid = record { isMonoid = +-isMonoid }

open Monoid +-monoid public
using ()
renaming ( semigroup to +-semigroup
; rawMonoid to +-rawMonoid)
using ()
renaming
( rawMagma to +-rawMagma
; magma to +-magma
; semigroup to +-semigroup
; rawMonoid to +-rawMonoid
)

*-semigroup : Semigroup _ _
*-semigroup = record { isSemigroup = *-isSemigroup }

open Semigroup *-semigroup public
using ()
renaming
( rawMagma to *-rawMagma
; magma to *-magma
)

record SemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
infixl 7 _*_
infixl 6 _+_
Expand All @@ -251,9 +271,10 @@ record SemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
nearSemiring = record { isNearSemiring = isNearSemiring }

open NearSemiring nearSemiring public
using ( +-semigroup; +-rawMonoid; +-monoid
; *-semigroup
)
using
( +-rawMagma; +-magma; +-semigroup; +-rawMonoid; +-monoid
; *-rawMagma; *-magma; *-semigroup
)

+-commutativeMonoid : CommutativeMonoid _ _
+-commutativeMonoid =
Expand Down Expand Up @@ -281,20 +302,26 @@ record SemiringWithoutAnnihilatingZero c ℓ : Set (suc (c ⊔ ℓ)) where
record { isCommutativeMonoid = +-isCommutativeMonoid }

open CommutativeMonoid +-commutativeMonoid public
using ()
renaming ( semigroup to +-semigroup
; rawMonoid to +-rawMonoid
; monoid to +-monoid
)
using ()
renaming
( rawMagma to +-rawMagma
; magma to +-magma
; semigroup to +-semigroup
; rawMonoid to +-rawMonoid
; monoid to +-monoid
)

*-monoid : Monoid _ _
*-monoid = record { isMonoid = *-isMonoid }

open Monoid *-monoid public
using ()
renaming ( semigroup to *-semigroup
; rawMonoid to *-rawMonoid
)
using ()
renaming
( rawMagma to *-rawMagma
; magma to *-magma
; semigroup to *-semigroup
; rawMonoid to *-rawMonoid
)

record Semiring c ℓ : Set (suc (c ⊔ ℓ)) where
infixl 7 _*_
Expand Down Expand Up @@ -328,17 +355,19 @@ record Semiring c ℓ : Set (suc (c ⊔ ℓ)) where

open SemiringWithoutAnnihilatingZero
semiringWithoutAnnihilatingZero public
using ( +-semigroup; +-rawMonoid; +-monoid
; +-commutativeMonoid
; *-semigroup; *-rawMonoid; *-monoid
)
using
( +-rawMagma; +-magma; +-semigroup
; *-rawMagma; *-magma; *-semigroup
; +-rawMonoid; +-monoid; +-commutativeMonoid
; *-rawMonoid; *-monoid
)

semiringWithoutOne : SemiringWithoutOne _ _
semiringWithoutOne =
record { isSemiringWithoutOne = isSemiringWithoutOne }

open SemiringWithoutOne semiringWithoutOne public
using (nearSemiring)
using (nearSemiring)

record CommutativeSemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
infixl 7 _*_
Expand All @@ -361,11 +390,12 @@ record CommutativeSemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
record { isSemiringWithoutOne = isSemiringWithoutOne }

open SemiringWithoutOne semiringWithoutOne public
using ( +-semigroup; +-rawMonoid; +-monoid
; +-commutativeMonoid
; *-semigroup
; nearSemiring
)
using
( +-rawMagma; +-magma; +-semigroup
; *-rawMagma; *-magma; *-semigroup
; +-rawMonoid; +-monoid; +-commutativeMonoid
; nearSemiring
)

record CommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
infixl 7 _*_
Expand All @@ -386,13 +416,15 @@ record CommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
semiring = record { isSemiring = isSemiring }

open Semiring semiring public
using ( +-semigroup; +-rawMonoid; +-monoid
; +-commutativeMonoid
; *-semigroup; *-rawMonoid; *-monoid
; nearSemiring; semiringWithoutOne
; semiringWithoutAnnihilatingZero
; rawSemiring
)
using
( +-rawMagma; +-magma; +-semigroup
; *-rawMagma; *-magma; *-semigroup
; +-rawMonoid; +-monoid; +-commutativeMonoid
; *-rawMonoid; *-monoid
; nearSemiring; semiringWithoutOne
; semiringWithoutAnnihilatingZero
; rawSemiring
)

*-commutativeMonoid : CommutativeMonoid _ _
*-commutativeMonoid =
Expand Down Expand Up @@ -444,15 +476,17 @@ record Ring c ℓ : Set (suc (c ⊔ ℓ)) where
semiring = record { isSemiring = isSemiring }

open Semiring semiring public
using ( +-semigroup; +-rawMonoid; +-monoid
; +-commutativeMonoid
; *-semigroup; *-rawMonoid; *-monoid
; nearSemiring; semiringWithoutOne
; semiringWithoutAnnihilatingZero
)
using
( +-rawMagma; +-magma; +-semigroup
; *-rawMagma; *-magma; *-semigroup
; +-rawMonoid; +-monoid ; +-commutativeMonoid
; *-rawMonoid; *-monoid
; nearSemiring; semiringWithoutOne
; semiringWithoutAnnihilatingZero
)

open AbelianGroup +-abelianGroup public
using () renaming (group to +-group)
using () renaming (group to +-group)

rawRing : RawRing _
rawRing = record
Expand Down Expand Up @@ -489,12 +523,15 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where

open Ring ring public using (rawRing; +-group; +-abelianGroup)
open CommutativeSemiring commutativeSemiring public
using ( +-semigroup; +-rawMonoid; +-monoid; +-commutativeMonoid
; *-semigroup; *-rawMonoid; *-monoid; *-commutativeMonoid
; nearSemiring; semiringWithoutOne
; semiringWithoutAnnihilatingZero; semiring
; commutativeSemiringWithoutOne
)
using
( +-rawMagma; +-magma; +-semigroup
; *-rawMagma; *-magma; *-semigroup
; +-rawMonoid; +-monoid; +-commutativeMonoid
; *-rawMonoid; *-monoid; *-commutativeMonoid
; nearSemiring; semiringWithoutOne
; semiringWithoutAnnihilatingZero; semiring
; commutativeSemiringWithoutOne
)

------------------------------------------------------------------------
-- Lattices and boolean algebras
Expand All @@ -513,7 +550,7 @@ record Semilattice c ℓ : Set (suc (c ⊔ ℓ)) where
band : Band c ℓ
band = record { isBand = isBand }

open Band band public using (semigroup)
open Band band public using (rawMagma; magma; semigroup)

record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where
infixr 7 _∧_
Expand Down Expand Up @@ -572,3 +609,18 @@ record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where

open DistributiveLattice distributiveLattice public
using (setoid; lattice)


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

-- Version 0.18

RawSemigroup = RawMagma
{-# WARNING_ON_USAGE RawSemigroup
"Warning: RawSemigroup was deprecated in v0.18.
Please use RawMagma instead."
#-}
Loading