The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi, to summarize previous answers:

1) first of all, "++" is a function and functions in coq are total
(you don't need to prove totality, this is hardcoded in the very
notion of function in coq). So there is no point in proving that there
exists a l3 that is equal to l1++l2, since l1++l2 exists by totality
of ++. Each time you need to talk about l3, just put l1++l2.

2) In coq, tactics do not need to be trusted or correct, they only
build a proof term *that will be completely checked* at Qed. So
whatever tactic you use in the proof (exists, intros, induction etc)
if the Qed succeeds it means that you built a correct proof of the
property you stated at first.

Hope this helps
Pierre



2014-09-09 17:09 GMT+02:00 Christopher Jenkins 
<cjenkin1 AT trinity.edu>:
> Forgive me if I'm missing something, but if the type signature of list
> concatenation says it takes two lists and return a list, and Coq is a total
> language, why would you need to show closure?
>
> On Mon, Sep 8, 2014 at 3:02 AM, Beta Ziliani 
> <beta AT mpi-sws.org>
>  wrote:
>>
>>
>> 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.
>>> >>
>>> >>
>>> >
>>
>>
>
>
>
> --
> Christopher Jenkins
> Computer Science 2013
> Trinity University