The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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?