------------------------------------------------------------------------
-- 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