The Coq mailing list

[Casteran Pierre <pierre.casteran AT labri.fr>]

Hi,

  I think your proof is correct, but too complex.
  Since list concatenation is already a function (if you use Standard 
Library's  one), you don't need to do a proof by cases.


Require Import List.
Theorem list_monoid :  forall ( X : Type ) ( l1 l2 : list X ), exists (
l3 : list X ),
    l1 ++ l2 = l3.
Proof.
 intros X l1 l2 ; now exists (l1 ++ l2).
Qed.


Pierre





Le 08/09/2014 08:31, mukesh tiwari a écrit :
> 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.