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 + ) +  ≡ n + 
  ex n = assoc ℕ+-isSemigroup n  

With applied module opening:

module Usage₂ where
  open IsSemigroup ℕ+-isSemigroup

  ex : ∀ n → (n + ) +  ≡ n + 
  ex n = assoc n  

With local module opening:

module Usage₃ where
  ex : ∀ n → (n + ) +  ≡ n + 
  ex n = assoc n    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 _+_ 

Usage

Usage example:

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

  ex′ : ∀ n → (n + ) + n ≡ n + n
  ex′ n = assoc n  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
    }

• When constructing IsCommutativeMonoid, we should provide the semigroup, left identity and commutativity properties.
• When using IsCommutativeMonoid, we have semigroup, associativity, monoid, identity and commutativity properties.

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  _∙_
  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  _×′_

  _×′_ : ℕ → Carrier → Carrier
       ×′ 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

• The definitions are generalized from _≡_ to an arbitrary equivalence relation.
• The definitions are universe polymorphic (see later).

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 + ) +  ≡ n + 
  ex n = assoc n