\documentclass{article}
% this is a LaTeX comment
\usepackage{agda}
\usepackage[utf8x]{inputenc}
\usepackage{amsmath,amssymb,amsfonts}
\DeclareUnicodeCharacter{"2261}{$\equiv$}
\DeclareUnicodeCharacter{"2237}{$::$}
\begin{document}
\paragraph{Note.} This is a \texttt{lagda} file; it means that if you download it it (almost) compiles when you open as if it was an agda file, and that it (almost) generates a pdf when you compile with latex. Enjoy!
Recall that a \emph{monoid} is a set endowed with an operation that is associative and has an identity element; we now want to define this (and others) property and prove that the \texttt{List} construction gives a monoid \texttt{List A} for every object/type \texttt{A}.
We start with a boilerplate declaration or Agda will complain:
\begin{code}
module Monoidi where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
\end{code}
Then we define the data type and the constructors for our wannabe monoid: lists of elements on $A$ are either the empty tuple, or are construed inductively from an element \AgdaDatatype{a : A} and a list \AgdaDatatype{as : List A}, joined together with a \AgdaFunction{∷} (pron. \emph{cons}):
\begin{code}
data List (A : Set) : Set where
[] : List A
_∷_ : A → List A → List A
\end{code}
This definition matches the usual behaviour of lists that you might have known to love-hate from Haskell: the term \AgdaDatatype{[1,2,3]} consists of \AgdaDatatype{1 ∷ 2 ∷ 3 ∷ []}. One can define \AgdaFunction{head}, \AgdaFunction{tail}, etc. in the usual way; no heterogeneous lists, etc.
But this doesn't have to become a lesson on Functional Programming! There's another course for that. Instead, let's concentrate on the functions that will be useful for our proof: lists can be joined with the \AgdaFunction{++} operation (pron.: \emph{concat}):
\begin{code}
_++_ : {A : Set} → List A → List A → List A
[] ++ v = v
(u ∷ us) ++ v = u ∷ (us ++ v)
\end{code}
Easy peasy: concatenating an empty list with \AgdaDatatype{v} yields just \AgdaDatatype{v}, and the concat of an inhabited list with \AgdaDatatype{v} is just the head of the first, cons the concat of its tail with \AgdaDatatype{v}.
For the sake of completeness now let's define \emph{properties} that operations might enjoy: the good ol' associativity and commutativity for an operation $A\times A → A$. What is beautiful about these declarations is that they define types that can be read as proofs that some propositions are true!
The associative property says that
\begin{code}
Associative :
{A : Set} →
-- for all given type A
(f : A → A → A) → Set
-- `the function ∘ : A × A → A
Associative {A} f =
-- is associative' means that
∀ {x y z : A} → f (f x y) z ≡ f x (f y z)
-- if (x y z : A), then x ∘ (y ∘ z) = (x ∘ y) ∘ z
\end{code}
One interprets commutativity in a similar way.
\begin{code}
Commutative : ∀ {A} → (A → A → A) → Set
Commutative {A} f = ∀ {x y : A} → f x y ≡ f y x
\end{code}
Now, a semigroup is just a set endowed with an associative binary operation:
\begin{code}
record IsSemigroup {A} (_∘_ : A → A → A) : Set where
field
assoc : Associative {A} (_∘_)
record HasIdentity {A} (_∘_ : A → A → A) (z : A) : Set where
field
lId : {a : A} → z ∘ a ≡ a
rId : {a : A} → a ∘ z ≡ a
record IsMonoid (A : Set) (_∘_ : A → A → A) (z : A) : Set where
field
isSemigroup : IsSemigroup {A} (_∘_)
hasIdentity : HasIdentity {A} (_∘_) z
\end{code}
For the sake of completeness, let's state also the definition of a commutative (`abelian') monoid:
\begin{code}
record IsAbelianMonoid (A : Set) (_∘_ : A → A → A) (z : A) : Set where
field
isMonoid : IsMonoid A (_∘_) z
isAbelian : Commutative (_∘_)
\end{code}
Now for the proof that \AgdaDatatype{List A} is a monoid for every A (in poorer typesetting, alas; also, note that the highlighted lines might need further refinement):
\begin{code}
proof : ∀ {A : Set} → IsMonoid (List A) (_++_) ([])
proof {A} =
record
{ isSemigroup =
record { assoc = asso-proof }
; hasIdentity =
record { lId = refl
; rId = rId-proof {A}
}
}
where
rId-proof : {A : Set} (a : List A) → (a ++ []) ≡ a
rId-proof {A} [] = refl
rId-proof {A} (a ∷ as) =
begin
(a ∷ as) ++ []
≡⟨ cong (\x → a ∷ x) (rId-proof {A} as) ⟩
(a ∷ as)
∎
emma : {a b c : List A} → (x : A) →
(x ∷ (a ++ b)) ++ c ≡ ((x ∷ a) ++ b) ++ c
emma {[]} {b} {c} x = refl
emma {(a ∷ as)} {b} {c} x =
begin
(x ∷ ((a ∷ as) ++ b)) ++ c
≡⟨ cong (\t → (x ∷ t) ++ c) refl ⟩
(x ∷ (a ∷ (as ++ b))) ++ c
≡⟨ cong ((\t → (x ∷ t) ++ c)) refl ⟩
(x ∷ ((a ∷ as) ++ b)) ++ c
∎
asso-proof : Associative {List A} (_++_)
asso-proof {[]} {y} {z} = refl
asso-proof {x ∷ xs} {[]} {z} =
begin
((x ∷ xs) ++ []) ++ z
≡⟨ cong (\t → t ++ z) (rId-proof {A} (x ∷ xs)) ⟩
(x ∷ xs) ++ ([] ++ z)
∎
asso-proof {x ∷ xs} {y ∷ ys} {[]} =
begin
((x ∷ xs) ++ (y ∷ ys)) ++ []
≡⟨ rId-proof {A} ((x ∷ xs) ++ (y ∷ ys)) ⟩
(x ∷ xs) ++ (y ∷ ys)
≡⟨ cong (\t → (x ∷ xs) ++ t) (sym (rId-proof {A} (y ∷ ys))) ⟩
(x ∷ xs) ++ ((y ∷ ys) ++ [])
∎
asso-proof {x ∷ xs} {y} {z} =
begin
((x ∷ xs) ++ y) ++ z
≡⟨ cong (\t → t ++ z) refl ⟩
(x ∷ (xs ++ y)) ++ z
≡⟨ emma {xs} {y} {z} x ⟩
x ∷ ((xs ++ y) ++ z)
≡⟨ cong (\t → x ∷ t) (asso-proof {xs} {y} {z}) ⟩
x ∷ (xs ++ (y ++ z))
≡⟨ refl ⟩
(x ∷ xs) ++ (y ++ z)
∎
\end{code}
\end{document}