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