------------------------------------------------------------------------
-- Some algebraic structures (not packed up with setoids and
-- operations)
------------------------------------------------------------------------

open import Relation.Binary

-- The structures are parameterised on an underlying equality.

module Algebra.Structures (s : Setoid) where

open Setoid s
import Algebra.FunctionProperties as P
open P s
import Relation.Binary.EqReasoning as EqR
open EqR s
open import Data.Function
open import Data.Product

private

  -- Some abbreviations:

  _Preserves-≈ : Op₁ → Set
  ∙ Preserves-≈ = ∙ Preserves _≈_ ⟶ _≈_

  _Preserves₂-≈ : Op₂ → Set
  ∙ Preserves₂-≈ = ∙ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_

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

record IsSemigroup (∙ : Op₂) : Set where
  field
    assoc    : Associative ∙
    ∙-pres-≈ : ∙ Preserves₂-≈

record IsMonoid (∙ : Op₂) (ε : carrier) : Set where
  field
    isSemigroup : IsSemigroup ∙
    identity    : Identity ε ∙

  open IsSemigroup isSemigroup public

record IsCommutativeMonoid (∙ : Op₂) (ε : carrier) : Set where
  field
    isMonoid : IsMonoid ∙ ε
    comm     : Commutative ∙

  open IsMonoid isMonoid public

record IsGroup (_∙_ : Op₂) (ε : carrier) (_⁻¹ : Op₁) : Set where
  infixl  _-_
  field
    isMonoid  : IsMonoid _∙_ ε
    inverse   : Inverse ε _⁻¹ _∙_
    ⁻¹-pres-≈ : _⁻¹ Preserves-≈

  open IsMonoid isMonoid public

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

record IsAbelianGroup (∙ : Op₂) (ε : carrier) (⁻¹ : Op₁) : Set where
  field
    isGroup : IsGroup ∙ ε ⁻¹
    comm    : Commutative ∙

  open IsGroup isGroup public

  isCommutativeMonoid : IsCommutativeMonoid ∙ ε
  isCommutativeMonoid = record
    { isMonoid = isMonoid
    ; comm     = comm
    }

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

record IsNearSemiring (+ * : Op₂) (0# : carrier) : Set where
  field
    +-isMonoid    : IsMonoid + 0#
    *-isSemigroup : IsSemigroup *
    distribʳ      : * DistributesOverʳ +
    zeroˡ         : LeftZero 0# *

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

  open IsSemigroup *-isSemigroup public
         renaming ( assoc    to *-assoc
                  ; ∙-pres-≈ to *-pres-≈
                  )

record IsSemiringWithoutOne (+ * : Op₂) (0# : carrier) : Set where
  field
    +-isCommutativeMonoid : IsCommutativeMonoid + 0#
    *-isSemigroup         : IsSemigroup *
    distrib               : * DistributesOver +
    zero                  : Zero 0# *

  open IsCommutativeMonoid +-isCommutativeMonoid public
         renaming ( assoc       to +-assoc
                  ; ∙-pres-≈    to +-pres-≈
                  ; isSemigroup to +-isSemigroup
                  ; identity    to +-identity
                  ; isMonoid    to +-isMonoid
                  ; comm        to +-comm
                  )

  open IsSemigroup *-isSemigroup public
         renaming ( assoc       to *-assoc
                  ; ∙-pres-≈    to *-pres-≈
                  )

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

record IsSemiringWithoutAnnihilatingZero (+ * : Op₂) (0# 1# : carrier)
         : Set where
  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
         renaming ( assoc       to +-assoc
                  ; ∙-pres-≈    to +-pres-≈
                  ; isSemigroup to +-isSemigroup
                  ; identity    to +-identity
                  ; isMonoid    to +-isMonoid
                  ; comm        to +-comm
                  )

  open IsMonoid *-isMonoid public
         renaming ( assoc       to *-assoc
                  ; ∙-pres-≈    to *-pres-≈
                  ; isSemigroup to *-isSemigroup
                  ; identity    to *-identity
                  )

record IsSemiring (+ * : Op₂) (0# 1# : carrier) : Set where
  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 (+ * : Op₂) (0# : carrier)
         : Set where
  field
    isSemiringWithoutOne : IsSemiringWithoutOne + * 0#
    *-comm               : Commutative *

  open IsSemiringWithoutOne isSemiringWithoutOne public

record IsCommutativeSemiring (+ * : Op₂) (0# 1# : carrier) : Set where
  field
    isSemiring : IsSemiring + * 0# 1#
    *-comm     : Commutative *

  open IsSemiring isSemiring public

  *-isCommutativeMonoid : IsCommutativeMonoid * 1#
  *-isCommutativeMonoid = record
      { isMonoid = *-isMonoid
      ; comm     = *-comm
      }

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

record IsRing (_+_ _*_ : Op₂) (-_ : Op₁) (0# 1# : carrier) : Set where
  field
    +-isAbelianGroup : IsAbelianGroup _+_ 0# -_
    *-isMonoid       : IsMonoid _*_ 1#
    distrib          : _*_ DistributesOver _+_

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

  open IsMonoid *-isMonoid public
         renaming ( assoc       to *-assoc
                  ; ∙-pres-≈    to *-pres-≈
                  ; isSemigroup to *-isSemigroup
                  ; identity    to *-identity
                  )

  zero : Zero 0# _*_
  zero = (zeroˡ , zeroʳ)
    where
    zeroˡ : LeftZero 0# _*_
    zeroˡ x = begin
        0# * x                              ≈⟨ sym $ proj₂ +-identity _ ⟩
       (0# * x) +            0#             ≈⟨ byDef ⟨ +-pres-≈ ⟩ sym (proj₂ --inverse _) ⟩
       (0# * x) + ((0# * x)  + - (0# * x))  ≈⟨ sym $ +-assoc _ _ _ ⟩
      ((0# * x) +  (0# * x)) + - (0# * x)   ≈⟨ sym (proj₂ distrib _ _ _) ⟨ +-pres-≈ ⟩ byDef ⟩
             ((0# + 0#) * x) + - (0# * x)   ≈⟨ (proj₂ +-identity _ ⟨ *-pres-≈ ⟩ byDef)
                                                 ⟨ +-pres-≈ ⟩
                                               byDef ⟩
                    (0# * x) + - (0# * x)   ≈⟨ proj₂ --inverse _ ⟩
                             0#             ∎

    zeroʳ : RightZero 0# _*_
    zeroʳ x = begin
      x * 0#                              ≈⟨ sym $ proj₂ +-identity _ ⟩
      (x * 0#) + 0#                       ≈⟨ byDef ⟨ +-pres-≈ ⟩ sym (proj₂ --inverse _) ⟩
      (x * 0#) + ((x * 0#) + - (x * 0#))  ≈⟨ sym $ +-assoc _ _ _ ⟩
      ((x * 0#) + (x * 0#)) + - (x * 0#)  ≈⟨ sym (proj₁ distrib _ _ _) ⟨ +-pres-≈ ⟩ byDef ⟩
      (x * (0# + 0#)) + - (x * 0#)        ≈⟨ (byDef ⟨ *-pres-≈ ⟩ proj₂ +-identity _)
                                               ⟨ +-pres-≈ ⟩
                                             byDef ⟩
      (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 (+ * : Op₂) (- : Op₁) (0# 1# : carrier)
         : Set where
  field
    isRing : IsRing + * - 0# 1#
    *-comm : Commutative *

  open IsRing isRing public

  isCommutativeSemiring : IsCommutativeSemiring + * 0# 1#
  isCommutativeSemiring = record
    { isSemiring = isSemiring
    ; *-comm     = *-comm
    }

  open IsCommutativeSemiring isCommutativeSemiring public
         using (isCommutativeSemiringWithoutOne)

record IsLattice (∨ ∧ : Op₂) : Set where
  field
    ∨-comm     : Commutative ∨
    ∨-assoc    : Associative ∨
    ∨-pres-≈   : ∨ Preserves₂-≈
    ∧-comm     : Commutative ∧
    ∧-assoc    : Associative ∧
    ∧-pres-≈   : ∧ Preserves₂-≈
    absorptive : Absorptive ∨ ∧

record IsDistributiveLattice (∨ ∧ : Op₂) : Set where
  field
    isLattice    : IsLattice ∨ ∧
    ∨-∧-distribʳ : ∨ DistributesOverʳ ∧

  open IsLattice isLattice public

record IsBooleanAlgebra (∨ ∧ : Op₂) (¬ : Op₁) (⊤ ⊥ : carrier) : Set where
  field
    isDistributiveLattice : IsDistributiveLattice ∨ ∧
    ∨-complementʳ         : RightInverse ⊤ ¬ ∨
    ∧-complementʳ         : RightInverse ⊥ ¬ ∧
    ¬-pres-≈              : ¬ Preserves-≈

  open IsDistributiveLattice isDistributiveLattice public