------------------------------------------------------------------------
-- Some algebraic structures (not packed up with sets, operations,
-- etc.)
------------------------------------------------------------------------

{-# OPTIONS --universe-polymorphism #-}

open import Relation.Binary

module Algebra.Structures where

import Algebra.FunctionProperties as FunctionProperties
open import Data.Product
open import Function
open import Level hiding (zero)
import Relation.Binary.EqReasoning as EqR

open FunctionProperties using (Op₁; Op₂)

------------------------------------------------------------------------
-- One binary operation

record IsSemigroup {a } {A : Set a} ( : Rel A )
( : Op₂ A) : Set (a  ) where
open FunctionProperties
field
isEquivalence : IsEquivalence
assoc         : Associative
∙-cong        :  Preserves₂

open IsEquivalence isEquivalence public

record IsMonoid {a } {A : Set a} ( : Rel A )
( : Op₂ A) (ε : A) : Set (a  ) where
open FunctionProperties
field
isSemigroup : IsSemigroup
identity    : Identity ε

open IsSemigroup isSemigroup public

record IsCommutativeMonoid {a } {A : Set a} ( : Rel A )
(_∙_ : Op₂ A) (ε : A) : Set (a  ) where
open FunctionProperties
field
isSemigroup : IsSemigroup  _∙_
identityˡ   : LeftIdentity ε _∙_
comm        : Commutative _∙_

open IsSemigroup isSemigroup public

identity : Identity ε _∙_
identity = (identityˡ , identityʳ)
where
open EqR (record { isEquivalence = isEquivalence })

identityʳ : RightIdentity ε _∙_
identityʳ = λ x  begin
(x  ε)  ≈⟨ comm x ε
(ε  x)  ≈⟨ identityˡ x
x

isMonoid : IsMonoid  _∙_ ε
isMonoid = record
{ isSemigroup = isSemigroup
; identity    = identity
}

record IsGroup {a } {A : Set a} ( : Rel A )
(_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a  ) where
open FunctionProperties
infixl 7 _-_
field
isMonoid  : IsMonoid  _∙_ ε
inverse   : Inverse ε _⁻¹ _∙_
⁻¹-cong   : _⁻¹ Preserves

open IsMonoid isMonoid public

_-_ : Op₂ A
x - y = x  (y ⁻¹)

record IsAbelianGroup
{a } {A : Set a} ( : Rel A )
( : Op₂ A) (ε : A) (⁻¹ : Op₁ A) : Set (a  ) where
open FunctionProperties
field
isGroup : IsGroup   ε ⁻¹
comm    : Commutative

open IsGroup isGroup public

isCommutativeMonoid : IsCommutativeMonoid   ε
isCommutativeMonoid = record
{ isSemigroup = isSemigroup
; identityˡ   = proj₁ identity
; comm        = comm
}

------------------------------------------------------------------------
-- Two binary operations

record IsNearSemiring {a } {A : Set a} ( : Rel A )
(+ * : Op₂ A) (0# : A) : Set (a  ) where
open FunctionProperties
field
+-isMonoid    : IsMonoid  + 0#
*-isSemigroup : IsSemigroup  *
distribʳ      : * DistributesOverʳ +
zeroˡ         : LeftZero 0# *

open IsMonoid +-isMonoid public
renaming ( assoc       to +-assoc
; ∙-cong      to +-cong
; isSemigroup to +-isSemigroup
; identity    to +-identity
)

open IsSemigroup *-isSemigroup public
using ()
renaming ( assoc    to *-assoc
; ∙-cong   to *-cong
)

record IsSemiringWithoutOne {a } {A : Set a} ( : Rel A )
(+ * : Op₂ A) (0# : A) : Set (a  ) where
open FunctionProperties
field
+-isCommutativeMonoid : IsCommutativeMonoid  + 0#
*-isSemigroup         : IsSemigroup  *
distrib               : * DistributesOver +
zero                  : Zero 0# *

open IsCommutativeMonoid +-isCommutativeMonoid public
hiding (identityˡ)
renaming ( assoc       to +-assoc
; ∙-cong      to +-cong
; isSemigroup to +-isSemigroup
; identity    to +-identity
; isMonoid    to +-isMonoid
; comm        to +-comm
)

open IsSemigroup *-isSemigroup public
using ()
renaming ( assoc       to *-assoc
; ∙-cong      to *-cong
)

isNearSemiring : IsNearSemiring  + * 0#
isNearSemiring = record
{ +-isMonoid    = +-isMonoid
; *-isSemigroup = *-isSemigroup
; distribʳ      = proj₂ distrib
; zeroˡ         = proj₁ zero
}

record IsSemiringWithoutAnnihilatingZero
{a } {A : Set a} ( : Rel A )
(+ * : Op₂ A) (0# 1# : A) : Set (a  ) where
open FunctionProperties
field
-- Note that these structures do have an additive unit, but this
-- unit does not necessarily annihilate multiplication.
+-isCommutativeMonoid : IsCommutativeMonoid  + 0#
*-isMonoid            : IsMonoid  * 1#
distrib               : * DistributesOver +

open IsCommutativeMonoid +-isCommutativeMonoid public
hiding (identityˡ)
renaming ( assoc       to +-assoc
; ∙-cong      to +-cong
; isSemigroup to +-isSemigroup
; identity    to +-identity
; isMonoid    to +-isMonoid
; comm        to +-comm
)

open IsMonoid *-isMonoid public
using ()
renaming ( assoc       to *-assoc
; ∙-cong      to *-cong
; isSemigroup to *-isSemigroup
; identity    to *-identity
)

record IsSemiring {a } {A : Set a} ( : Rel A )
(+ * : Op₂ A) (0# 1# : A) : Set (a  ) where
open FunctionProperties
field
isSemiringWithoutAnnihilatingZero :
IsSemiringWithoutAnnihilatingZero  + * 0# 1#
zero : Zero 0# *

open IsSemiringWithoutAnnihilatingZero
isSemiringWithoutAnnihilatingZero public

isSemiringWithoutOne : IsSemiringWithoutOne  + * 0#
isSemiringWithoutOne = record
{ +-isCommutativeMonoid = +-isCommutativeMonoid
; *-isSemigroup         = *-isSemigroup
; distrib               = distrib
; zero                  = zero
}

open IsSemiringWithoutOne isSemiringWithoutOne public
using (isNearSemiring)

record IsCommutativeSemiringWithoutOne
{a } {A : Set a} ( : Rel A )
(+ * : Op₂ A) (0# : A) : Set (a  ) where
open FunctionProperties
field
isSemiringWithoutOne : IsSemiringWithoutOne  + * 0#
*-comm               : Commutative *

open IsSemiringWithoutOne isSemiringWithoutOne public

record IsCommutativeSemiring
{a } {A : Set a} ( : Rel A )
(_+_ _*_ : Op₂ A) (0# 1# : A) : Set (a  ) where
open FunctionProperties
field
+-isCommutativeMonoid : IsCommutativeMonoid  _+_ 0#
*-isCommutativeMonoid : IsCommutativeMonoid  _*_ 1#
distribʳ              : _*_ DistributesOverʳ _+_
zeroˡ                 : LeftZero 0# _*_

private
module +-CM = IsCommutativeMonoid +-isCommutativeMonoid
open module *-CM = IsCommutativeMonoid *-isCommutativeMonoid public
using () renaming (comm to *-comm)
open EqR (record { isEquivalence = +-CM.isEquivalence })

distrib : _*_ DistributesOver _+_
distrib = (distribˡ , distribʳ)
where
distribˡ : _*_ DistributesOverˡ _+_
distribˡ x y z = begin
(x * (y + z))        ≈⟨ *-comm x (y + z)
((y + z) * x)        ≈⟨ distribʳ x y z
((y * x) + (z * x))  ≈⟨ *-comm y x  +-CM.∙-cong  *-comm z x
((x * y) + (x * z))

zero : Zero 0# _*_
zero = (zeroˡ , zeroʳ)
where
zeroʳ : RightZero 0# _*_
zeroʳ x = begin
(x * 0#)  ≈⟨ *-comm x 0#
(0# * x)  ≈⟨ zeroˡ x
0#

isSemiring : IsSemiring  _+_ _*_ 0# 1#
isSemiring = record
{ isSemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = +-isCommutativeMonoid
; *-isMonoid            = *-CM.isMonoid
; distrib               = distrib
}
; zero                              = zero
}

open IsSemiring isSemiring public
hiding (distrib; zero; +-isCommutativeMonoid)

isCommutativeSemiringWithoutOne :
IsCommutativeSemiringWithoutOne  _+_ _*_ 0#
isCommutativeSemiringWithoutOne = record
{ isSemiringWithoutOne = isSemiringWithoutOne
; *-comm               = *-CM.comm
}

record IsRing
{a } {A : Set a} ( : Rel A )
(_+_ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a  ) where
open FunctionProperties
field
+-isAbelianGroup : IsAbelianGroup  _+_ 0# -_
*-isMonoid       : IsMonoid  _*_ 1#
distrib          : _*_ DistributesOver _+_

open IsAbelianGroup +-isAbelianGroup public
renaming ( assoc               to +-assoc
; ∙-cong              to +-cong
; isSemigroup         to +-isSemigroup
; identity            to +-identity
; isMonoid            to +-isMonoid
; inverse             to -‿inverse
; ⁻¹-cong             to -‿cong
; isGroup             to +-isGroup
; comm                to +-comm
; isCommutativeMonoid to +-isCommutativeMonoid
)

open IsMonoid *-isMonoid public
using ()
renaming ( assoc       to *-assoc
; ∙-cong      to *-cong
; isSemigroup to *-isSemigroup
; identity    to *-identity
)

zero : Zero 0# _*_
zero = (zeroˡ , zeroʳ)
where
open EqR (record { isEquivalence = isEquivalence })

zeroˡ : LeftZero 0# _*_
zeroˡ x = begin
0# * x                              ≈⟨ sym \$ proj₂ +-identity _
(0# * x) +            0#             ≈⟨ refl  +-cong  sym (proj₂ -‿inverse _)
(0# * x) + ((0# * x)  + - (0# * x))  ≈⟨ sym \$ +-assoc _ _ _
((0# * x) +  (0# * x)) + - (0# * x)   ≈⟨ sym (proj₂ distrib _ _ _)  +-cong  refl
((0# + 0#) * x) + - (0# * x)   ≈⟨ (proj₂ +-identity _  *-cong  refl)
+-cong
refl
(0# * x) + - (0# * x)   ≈⟨ proj₂ -‿inverse _
0#

zeroʳ : RightZero 0# _*_
zeroʳ x = begin
x * 0#                              ≈⟨ sym \$ proj₂ +-identity _
(x * 0#) + 0#                       ≈⟨ refl  +-cong  sym (proj₂ -‿inverse _)
(x * 0#) + ((x * 0#) + - (x * 0#))  ≈⟨ sym \$ +-assoc _ _ _
((x * 0#) + (x * 0#)) + - (x * 0#)  ≈⟨ sym (proj₁ distrib _ _ _)  +-cong  refl
(x * (0# + 0#)) + - (x * 0#)        ≈⟨ (refl  *-cong  proj₂ +-identity _)
+-cong
refl
(x * 0#) + - (x * 0#)               ≈⟨ proj₂ -‿inverse _
0#

isSemiringWithoutAnnihilatingZero
: IsSemiringWithoutAnnihilatingZero  _+_ _*_ 0# 1#
isSemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = +-isCommutativeMonoid
; *-isMonoid            = *-isMonoid
; distrib               = distrib
}

isSemiring : IsSemiring  _+_ _*_ 0# 1#
isSemiring = record
{ isSemiringWithoutAnnihilatingZero =
isSemiringWithoutAnnihilatingZero
; zero = zero
}

open IsSemiring isSemiring public
using (isNearSemiring; isSemiringWithoutOne)

record IsCommutativeRing
{a } {A : Set a} ( : Rel A )
(+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set (a  ) where
open FunctionProperties
field
isRing : IsRing  + * - 0# 1#
*-comm : Commutative *

open IsRing isRing public

isCommutativeSemiring : IsCommutativeSemiring  + * 0# 1#
isCommutativeSemiring = record
{ +-isCommutativeMonoid = +-isCommutativeMonoid
; *-isCommutativeMonoid = record
{ isSemigroup = *-isSemigroup
; identityˡ   = proj₁ *-identity
; comm        = *-comm
}
; distribʳ              = proj₂ distrib
; zeroˡ                 = proj₁ zero
}

open IsCommutativeSemiring isCommutativeSemiring public
using ( *-isCommutativeMonoid
; isCommutativeSemiringWithoutOne
)

record IsLattice {a } {A : Set a} ( : Rel A )
(  : Op₂ A) : Set (a  ) where
open FunctionProperties
field
isEquivalence : IsEquivalence
∨-comm        : Commutative
∨-assoc       : Associative
∨-cong        :  Preserves₂
∧-comm        : Commutative
∧-assoc       : Associative
∧-cong        :  Preserves₂
absorptive    : Absorptive

open IsEquivalence isEquivalence public

record IsDistributiveLattice {a } {A : Set a} ( : Rel A )
(  : Op₂ A) : Set (a  ) where
open FunctionProperties
field
isLattice    : IsLattice
∨-∧-distribʳ :  DistributesOverʳ

open IsLattice isLattice public

record IsBooleanAlgebra
{a } {A : Set a} ( : Rel A )
(  : Op₂ A) (¬ : Op₁ A) (  : A) : Set (a  ) where
open FunctionProperties
field
isDistributiveLattice : IsDistributiveLattice
∨-complementʳ         : RightInverse  ¬
∧-complementʳ         : RightInverse  ¬
¬-cong                : ¬ Preserves

open IsDistributiveLattice isDistributiveLattice public