# My Weblog

## List with concatenation operation is monoid.

We will try to prove in Coq that list with concatenation ( ++ ) is monoid. Monoid is set S with binary operation $\bullet$ with following properties.
1). Closure.

$\forall a, b \in S,\hspace{1 mm} \exists c \in S \hspace{1 mm}such \hspace{1 mm}that\hspace{1 mm} c = a \bullet b.$

2). Associativity.

$\forall a, b, c \in S \hspace{1 mm} then \hspace{1 mm} a \bullet ( b \bullet c ) = ( a \bullet b) \bullet c$

3) Identity.

$\exists e \in S \hspace{1 mm} such \hspace{1 mm} that \hspace{1 mm} \forall a \in S,\hspace{1 mm} e \bullet a = a \bullet e = a$

Proof in Coq.

Require Import List.

Theorem Closure : forall ( X : Type ) ( l1 l2 : list X ) , exists ( l3 : list X ),
l1 ++ l2 = l3.
Proof.
intros X l1 l2. exists ( l1 ++ l2) .
reflexivity.
Qed.

Theorem Association : forall ( X : Type ) ( l1 l2 l3 : list X ) ,
l1 ++ ( l2 ++ l3 ) = ( l1 ++  l2 ) ++ l3.
Proof.
intros X l1 l2 l3.
simpl. rewrite -> app_assoc_reverse. reflexivity.
Qed.

Theorem Existence_identity_left : forall ( X : Type ) ( l : list X ), exists e,
e ++ l = l.
Proof.
intros X l. exists nil. simpl.
reflexivity.
Qed.

Theorem Existence_identify_right : forall ( X : Type ) ( l : list X ) , exists e,
l ++ e = l.
Proof.
intros X l. exists nil.
apply app_nil_r.
Qed.



We don’t need to prove the closure property because all the functions in Coq is total. See thec discussion . Source code on github[1] and other proofs from software foundation[2].
[1] https://github.com/mukeshtiwari/Coq/blob/master/Monoid.v
[2] https://github.com/mukeshtiwari/Coq/blob/master/Poly.v