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 with following properties.
1). Closure.

2). Associativity.

3) Identity.

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