The Coq mailing list

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

On Mon, Sep 8, 2014 at 9:56 AM, mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:

Thank you Beta Ziliani and Casteran Pierre.

On Mon, Sep 8, 2014 at 12:46 PM, Beta Ziliani <beta AT mpi-sws.org> wrote:
> 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

The hesitation was because of I never used exists.

Still, my point is that you shouldn't distrust a proof that Coq accepted after Qed.  It doesn't matter which tactics you use for building the proof: if in the end Qed says "X is defined" then X's proof is correct.

 

>
>
>
>
> 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

Right now I am learning Coq from software foundation so no import of
library. Thank you for simple and elegant proof.

-Mukesh Tiwari

>>
>>
>>
>>
>>
>> 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.
>>
>>
>