The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

More importantly, Mukesh, you need to know that the very purpose of Coq is to check proofs: if it accepted your proof at Qed, then that is a valid proof.

Best,
Beta

On Mon, Sep 8, 2014 at 9:08 AM, Casteran Pierre <pierre.casteran AT labri.fr> wrote:

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.