The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Dear Coq-club.
 Pardon me if it's a stupid question. I am trying to prove that list
with ++ is monoid. I am able to prove

1). Identity
         l ++ [] = [] ++ l  = l
2). Associativity
         l1 ++ ( l2 ++ l3 ) = ( l1 ++ l2 ) ++ l3.

 and trying to prove the existence of closure.

3. Existence of closure.

Theorem list_monoid : forall ( X : Type ) ( l1 l2 : list X ), exists (
l3 : list X ),
    l1 ++ l2 = l3.
Proof.
    intros X l1 l2. destruct l1 as [ | h' l1'].
    Case "l1 = nil".
       simpl. exists l2. reflexivity.
    Case "l1 = cons h' l1'".
       simpl. exists ( h' :: l1' ++ l2 ). reflexivity.
Qed.

Could some one please tell that my proof of closure is sound. It's
accepted by Coq but I never used exists tactic ( currently on 4th
chapter of software foundation ) so I am bit skeptical.

-Mukesh Tiwari