The Coq mailing list

[ldou AT cs.ecnu.edu.cn]

Thanks again for the replies from Adam , Pierre and  Jeremy.
I am not familiar with Coq , so maybe the question i asked is quite naive.

the tactic induction  generates subgoals, one for each possible form of term.
In Pierre's case, when do "induction d as y", it  generates:
exists o' : o, set_mem o_dec o' (interp (DE y)) = true
then  do "simpl" and it turns out :
exists o' : o, (if o_dec o' ((y :: nil) :: nil) then true else false) = true.
i still cann't understand why interp (DE y) evaluates to ((y::nil)::nil). i 
thought it would be (((y::nil)::nil)::nil) ,just like what Compute interp (DE 
y) do.   ((y::nil)::nil) and (((y::nil)::nil)::nil) are different, right?

Anyway , Pierre's solution and Jeremy's solution really work in my proof. I'm 
really appreciate.


------------------ ԭʼÓʼþ ------------------
>From: Adam Chlipala 
><adamc AT csail.mit.edu>
>Reply-To: 
>To: 
>ldou AT cs.ecnu.edu.cn
>Subject: Re: [Coq-Club] [Coq Club]a strange question when using function
>Date: Thu, 25 Aug 2011 08:04:40 -0400
>
>ldou AT cs.ecnu.edu.cn
> wrote:
>> when proving lemma "existselement", i do "induction d" and  "simpl", then 
>> Coq system produce a paticular "e0:e" and replace "d" with "(DE e0)". 
>> That's why you see such a particular constant string.
>>   
>
>I don't call [e0] there a constant string. ["e0"] would be a constant
>string.
>
>> What confuse me is the difference when Coq compute the "interp" function. 
>> if i do:
>>
>> Compute (interp (DE "e0")).
>>
>> then i can get the following result  which is what i expect : 
>>      = (("e0" :: nil) :: nil) :: nil
>>      : m
>>
>> but when do "induction d" and  "simpl" in lemma "existselement", i get a 
>> different result:
>> ((e0 :: nil) :: nil)
>> which i think is wrong.
>>   
>
>Pierre already sent a solution, so I won't go into much more detail
>here, except to reiterate that Pierre and I are pretty sure that there
>is nothing wrong with this output, and the version you expected would be
>wrong. Perhaps the problem here is a misunderstanding of the meaning of
>double quotes in Coq? I asked you before why you expected a different
>outcome, but your message that I'm replying to doesn't seem to answer
>that question. Why would you think that [interp (DE "e0")] would yield
>the same term as your [induction] call?
>