------------------------------------------------------------------------
-- Definitions of algebraic structures like monoids and rings
-- (packed in records together with setoids and operations)
------------------------------------------------------------------------

module Algebra where

open import Relation.Binary
import Algebra.FunctionProperties as P
open import Algebra.Structures
open import Data.Function

------------------------------------------------------------------------
-- Semigroups, (commutative) monoids and (abelian) groups

record Semigroup : Set1 where
  infixl  _∙_
  field
    setoid      : Setoid
    _∙_         : P.Op₂ setoid
    isSemigroup : IsSemigroup setoid _∙_

  open Setoid setoid public
  open IsSemigroup setoid isSemigroup public

-- A raw monoid is a monoid without any laws (except for the
-- underlying equality).

record RawMonoid : Set1 where
  infixl  _∙_
  field
    setoid : Setoid
    _∙_    : P.Op₂ setoid
    ε      : Setoid.carrier setoid

  open Setoid setoid public

record Monoid : Set1 where
  infixl  _∙_
  field
    setoid   : Setoid
    _∙_      : P.Op₂ setoid
    ε        : Setoid.carrier setoid
    isMonoid : IsMonoid setoid _∙_ ε

  open Setoid setoid public
  open IsMonoid setoid isMonoid public

  semigroup : Semigroup
  semigroup = record { isSemigroup = isSemigroup }

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

record CommutativeMonoid : Set1 where
  infixl  _∙_
  field
    setoid              : Setoid
    _∙_                 : P.Op₂ setoid
    ε                   : Setoid.carrier setoid
    isCommutativeMonoid : IsCommutativeMonoid setoid _∙_ ε

  open Setoid setoid public
  open IsCommutativeMonoid setoid isCommutativeMonoid public

  monoid : Monoid
  monoid = record { isMonoid = isMonoid }

  open Monoid monoid public using (semigroup; rawMonoid)

record Group : Set1 where
  infix   _⁻¹
  infixl  _∙_
  field
    setoid  : Setoid
    _∙_     : P.Op₂ setoid
    ε       : Setoid.carrier setoid
    _⁻¹     : P.Op₁ setoid
    isGroup : IsGroup setoid _∙_ ε _⁻¹

  open Setoid setoid public
  open IsGroup setoid isGroup public

  monoid : Monoid
  monoid = record { isMonoid = isMonoid }

  open Monoid monoid public using (semigroup; rawMonoid)

record AbelianGroup : Set1 where
  infix   _⁻¹
  infixl  _∙_
  field
    setoid         : Setoid
    _∙_            : P.Op₂ setoid
    ε              : Setoid.carrier setoid
    _⁻¹            : P.Op₁ setoid
    isAbelianGroup : IsAbelianGroup setoid _∙_ ε _⁻¹

  open Setoid setoid public
  open IsAbelianGroup setoid isAbelianGroup public

  group : Group
  group = record { isGroup = isGroup }

  open Group group public using (semigroup; monoid; rawMonoid)

  commutativeMonoid : CommutativeMonoid
  commutativeMonoid =
    record { isCommutativeMonoid = isCommutativeMonoid }

------------------------------------------------------------------------
-- Various kinds of semirings

record NearSemiring : Set1 where
  infixl  _*_
  infixl  _+_
  field
    setoid         : Setoid
    _+_            : P.Op₂ setoid
    _*_            : P.Op₂ setoid
    0#             : Setoid.carrier setoid
    isNearSemiring : IsNearSemiring setoid _+_ _*_ 0#

  open Setoid setoid public
  open IsNearSemiring setoid isNearSemiring public

  +-monoid : Monoid
  +-monoid = record { isMonoid = +-isMonoid }

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

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

record SemiringWithoutOne : Set1 where
  infixl  _*_
  infixl  _+_
  field
    setoid               : Setoid
    _+_                  : P.Op₂ setoid
    _*_                  : P.Op₂ setoid
    0#                   : Setoid.carrier setoid
    isSemiringWithoutOne : IsSemiringWithoutOne setoid _+_ _*_ 0#

  open Setoid setoid public
  open IsSemiringWithoutOne setoid isSemiringWithoutOne public

  nearSemiring : NearSemiring
  nearSemiring = record { isNearSemiring = isNearSemiring }

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

  +-commutativeMonoid : CommutativeMonoid
  +-commutativeMonoid =
    record { isCommutativeMonoid = +-isCommutativeMonoid }

record SemiringWithoutAnnihilatingZero : Set1 where
  infixl  _*_
  infixl  _+_
  field
    setoid                            : Setoid
    _+_                               : P.Op₂ setoid
    _*_                               : P.Op₂ setoid
    0#                                : Setoid.carrier setoid
    1#                                : Setoid.carrier setoid
    isSemiringWithoutAnnihilatingZero :
      IsSemiringWithoutAnnihilatingZero setoid _+_ _*_ 0# 1#

  open Setoid setoid public
  open IsSemiringWithoutAnnihilatingZero
         setoid isSemiringWithoutAnnihilatingZero public

  +-commutativeMonoid : CommutativeMonoid
  +-commutativeMonoid =
    record { isCommutativeMonoid = +-isCommutativeMonoid }

  open CommutativeMonoid +-commutativeMonoid public using ()
         renaming ( 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
                  )

record Semiring : Set1 where
  infixl  _*_
  infixl  _+_
  field
    setoid     : Setoid
    _+_        : P.Op₂ setoid
    _*_        : P.Op₂ setoid
    0#         : Setoid.carrier setoid
    1#         : Setoid.carrier setoid
    isSemiring : IsSemiring setoid _+_ _*_ 0# 1#

  open Setoid setoid public
  open IsSemiring setoid isSemiring public

  semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero
  semiringWithoutAnnihilatingZero = record
    { isSemiringWithoutAnnihilatingZero =
        isSemiringWithoutAnnihilatingZero
    }

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

  semiringWithoutOne : SemiringWithoutOne
  semiringWithoutOne =
    record { isSemiringWithoutOne = isSemiringWithoutOne }

  open SemiringWithoutOne semiringWithoutOne public
         using (nearSemiring)

record CommutativeSemiringWithoutOne : Set1 where
  infixl  _*_
  infixl  _+_
  field
    setoid                          : Setoid
    _+_                             : P.Op₂ setoid
    _*_                             : P.Op₂ setoid
    0#                              : Setoid.carrier setoid
    isCommutativeSemiringWithoutOne :
      IsCommutativeSemiringWithoutOne setoid _+_ _*_ 0#

  open Setoid setoid public
  open IsCommutativeSemiringWithoutOne
         setoid isCommutativeSemiringWithoutOne public

  semiringWithoutOne : SemiringWithoutOne
  semiringWithoutOne =
    record { isSemiringWithoutOne = isSemiringWithoutOne }

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

record CommutativeSemiring : Set1 where
  infixl  _*_
  infixl  _+_
  field
    setoid                : Setoid
    _+_                   : P.Op₂ setoid
    _*_                   : P.Op₂ setoid
    0#                    : Setoid.carrier setoid
    1#                    : Setoid.carrier setoid
    isCommutativeSemiring : IsCommutativeSemiring setoid _+_ _*_ 0# 1#

  open Setoid setoid public
  open IsCommutativeSemiring setoid isCommutativeSemiring public

  semiring : Semiring
  semiring = record { isSemiring = isSemiring }

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

  *-commutativeMonoid : CommutativeMonoid
  *-commutativeMonoid =
    record { isCommutativeMonoid = *-isCommutativeMonoid }

  commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne
  commutativeSemiringWithoutOne = record
    { isCommutativeSemiringWithoutOne = isCommutativeSemiringWithoutOne
    }

------------------------------------------------------------------------
-- (Commutative) rings

-- A raw ring is a ring without any laws (except for the underlying
-- equality).

record RawRing : Set1 where
  infix   -_
  infixl  _*_
  infixl  _+_
  field
    setoid : Setoid
    _+_    : P.Op₂ setoid
    _*_    : P.Op₂ setoid
    -_     : P.Op₁ setoid
    0#     : Setoid.carrier setoid
    1#     : Setoid.carrier setoid

  open Setoid setoid public

record Ring : Set1 where
  infix   -_
  infixl  _*_
  infixl  _+_
  field
    setoid : Setoid
    _+_    : P.Op₂ setoid
    _*_    : P.Op₂ setoid
    -_     : P.Op₁ setoid
    0#     : Setoid.carrier setoid
    1#     : Setoid.carrier setoid
    isRing : IsRing setoid _+_ _*_ -_ 0# 1#

  open Setoid setoid public
  open IsRing setoid isRing public

  +-abelianGroup : AbelianGroup
  +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup }

  semiring : Semiring
  semiring = record { isSemiring = isSemiring }

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

  rawRing : RawRing
  rawRing = record
    { setoid = setoid
    ; _+_    = _+_
    ; _*_    = _*_
    ; -_     = -_
    ; 0#     = 0#
    ; 1#     = 1#
    }

record CommutativeRing : Set1 where
  infix   -_
  infixl  _*_
  infixl  _+_
  field
    setoid            : Setoid
    _+_               : P.Op₂ setoid
    _*_               : P.Op₂ setoid
    -_                : P.Op₁ setoid
    0#                : Setoid.carrier setoid
    1#                : Setoid.carrier setoid
    isCommutativeRing : IsCommutativeRing setoid _+_ _*_ -_ 0# 1#

  open Setoid setoid public
  open IsCommutativeRing setoid isCommutativeRing public

  ring : Ring
  ring = record { isRing = isRing }

  commutativeSemiring : CommutativeSemiring
  commutativeSemiring =
    record { isCommutativeSemiring = isCommutativeSemiring }

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

------------------------------------------------------------------------
-- (Distributive) lattices and boolean algebras

record Lattice : Set1 where
  infixr  _∧_
  infixr  _∨_
  field
    setoid    : Setoid
    _∨_       : P.Op₂ setoid
    _∧_       : P.Op₂ setoid
    isLattice : IsLattice setoid _∨_ _∧_

  open Setoid setoid public
  open IsLattice setoid isLattice public

record DistributiveLattice : Set1 where
  infixr  _∧_
  infixr  _∨_
  field
    setoid                : Setoid
    _∨_                   : P.Op₂ setoid
    _∧_                   : P.Op₂ setoid
    isDistributiveLattice : IsDistributiveLattice setoid _∨_ _∧_

  open Setoid setoid public
  open IsDistributiveLattice setoid isDistributiveLattice public

  lattice : Lattice
  lattice = record { isLattice = isLattice }

record BooleanAlgebra : Set1 where
  infix   ¬_
  infixr  _∧_
  infixr  _∨_
  field
    setoid           : Setoid
    _∨_              : P.Op₂ setoid
    _∧_              : P.Op₂ setoid
    ¬_               : P.Op₁ setoid
    ⊤                : Setoid.carrier setoid
    ⊥                : Setoid.carrier setoid
    isBooleanAlgebra : IsBooleanAlgebra setoid _∨_ _∧_ ¬_ ⊤ ⊥

  open Setoid setoid public
  open IsBooleanAlgebra setoid isBooleanAlgebra public

  distributiveLattice : DistributiveLattice
  distributiveLattice =
    record { isDistributiveLattice = isDistributiveLattice }

  open DistributiveLattice distributiveLattice public
         using (lattice)