module Application.Algebra where

open import Data.Nat using (; zero; suc; _+_)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; setoid)

import Relation.Binary.EqReasoning as EqR

Semigroup property

Let A be a type and let _∙_ be a binary operation on A. A with _∙_ forms a semigroup iff _∙_ is associative.

We can model the semigroup proposition as follows:


record IsSemigroup {A : Set} (_∙_ : A  A  A) : Set where
  field
    assoc         :  x y z   ((x  y)  z)    (x  (y  z))

Exercise

Prove that with _+_ forms a semigroup!


ℕ+-isSemigroup : IsSemigroup _+_

Usage

Usage example:


module Usage₁ where
  open IsSemigroup

  ex :  n  (n + 1) + 1  n + 2
  ex n = assoc ℕ+-isSemigroup n 1 1

With applied module opening:


module Usage₂ where
  open IsSemigroup ℕ+-isSemigroup

  ex :  n  (n + 1) + 1  n + 2
  ex n = assoc n 1 1

With local module opening:


module Usage₃ where
  ex :  n  (n + 1) + 1  n + 2
  ex n = assoc n 1 1  where
    open IsSemigroup ℕ+-isSemigroup

Monoid property

IsMonoid {A} _∙_ ε represents the proposition that (A, _∙_, ε) is a monoid:


record IsMonoid {A : Set} (_∙_ : A  A  A) (ε : A) : Set where
  field
    isSemigroup : IsSemigroup _∙_
    identity    : (∀ x  (ε  x)  x)  ×  (∀ x  (x  ε)  x)

  open IsSemigroup isSemigroup public

Public opening at the end makes usage of IsMonoid easier.

Exercise

Prove that (, _+_, 0) forms a monoid!


ℕ+0-isMonoid : IsMonoid _+_ 0

Usage

Usage example:


module Usage₄ where
  ex :  n  (n + 0) + n  n + n
  ex n = cong  x  x + n) (proj₂ identity n)  where
    open IsMonoid ℕ+0-isMonoid

  ex′ :  n  (n + 0) + n  n + n
  ex′ n = assoc n 0 n  where
    open IsMonoid ℕ+0-isMonoid   -- we opened IsMonoid, not IsSemigroup

Named binary operations

Instead of A → A → A we can write Op₂ A if we define


Op₂ : Set  Set
Op₂ A = A  A  A

Thus we can write


record IsSemigroup′ {A : Set} (_∙_ : Op₂ A) : Set where
  field
    assoc         :  x y z   ((x  y)  z)    (x  (y  z))

Exercise

Define the type of unary operations as Op₁!

Named function properties

We can name functions properties like


Associative : {A : Set}  Op₂ A  Set
Associative _∙_ =  x y z   ((x  y)  z)    (x  (y  z))

After this definition we can write


record IsSemigroup″ {A : Set} (_∙_ : Op₂ A) : Set where
  field
    assoc         : Associative _∙_

Exercises

Define the following function properties!


Commutative : {A : Set}  Op₂ A  Set _

The first parameter of LeftIdentity is the neutral element.


LeftIdentity : {A : Set}  A  Op₂ A  Set _


RightIdentity : {A : Set}  A  Op₂ A  Set _


Identity : {A : Set}  A  Op₂ A  Set _

Commutative monoid property

Consider the following definition of the commutative monoid proposition:


record IsCommutativeMonoid′ {A : Set} (_∙_ : A  A  A) (ε : A) : Set where
  field
    isMonoid : IsMonoid _∙_ ε
    comm     : Commutative _∙_

This definition is correct, but redundant because commutativity and left identity properties entail the right identity property.

A non-redundant and still easy-to-use definition is the following:


record IsCommutativeMonoid {A : Set} (_∙_ : A  A  A) (ε : A) : Set where
  field
    isSemigroup : IsSemigroup _∙_
    identityˡ   : LeftIdentity ε _∙_
    comm        : Commutative _∙_

  open IsSemigroup isSemigroup public

  identity : Identity ε _∙_
  identity = (identityˡ , identityʳ)
    where
    open EqR (setoid A)

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

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

Exercises

  1. Define the group property!

  2. Define the abelian group property!

The type of all semigroups

We can define the type of semigroups as


record Semigroup : Set₁ where
  infixl 7 _∙_
  field
    Carrier     : Set
    _∙_         : Op₂ Carrier
    isSemigroup : IsSemigroup _∙_

  open IsSemigroup isSemigroup public

Exercises

  1. Prove that (ℕ, +) is a semigroup (by proving that there is a corresponding element of Semigroup)!

  2. Define the types of all monoids as a record with fields Carrier, _∙_, ε and isMonoid!

Some defined operations

We can define the multiplication by a natural number in any monoid:


module MonoidOperations (m : Monoid) where

  open Monoid m

  infixr 7 _×′_

  _×′_ :   Carrier  Carrier
  0     ×′ x = ε
  suc n ×′ x = x  (n ×′ x)

Standard Library definitions

You can find the given definitions in the following Standard Library modules:


import Algebra.FunctionProperties using (Op₁; Op₂)
import Algebra.FunctionProperties using (Associative; Commutative; LeftIdentity; RightIdentity; Identity) -- and more function properties
import Algebra.Structures using (IsSemigroup; IsMonoid; IsCommutativeMonoid) -- and more
import Algebra using (Semigroup; Monoid; CommutativeMonoid) -- and more
import Algebra.Operations -- some defined operations

import Data.Nat.Properties using (isCommutativeSemiring) -- this contains definitions like ℕ+0-isMonoid

Notable differences

Example usage


module StdLibUsage where
  open import Algebra.Structures as A using (IsCommutativeMonoid)
  open import Data.Nat.Properties using (isCommutativeSemiring)

  open A.IsCommutativeSemiring
  open A.IsCommutativeMonoid (+-isCommutativeMonoid isCommutativeSemiring)

  ex :  n  (n + 1) + 1  n + 2
  ex n = assoc n 1 1