My Weblog

Blog about programming and math

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

Advertisements

September 10, 2014 Posted by | Programming | , , , , | 2 Comments