The Coq mailing list

[Eugene Kirpichov <ekirpichov AT gmail.com>]

2010/1/30 Adam Chlipala 
<adam AT chlipala.net>:
> Eugene Kirpichov wrote:
>>
>> Suppose I'm proving the following theorem.
>> Theorem t : forall n, match n with | O =>  O | S x =>  S x end = n.
>>   intros n.
>>
>>   (* Here I could just do "destruct n", but I'd like to do that
>> automatically *)
>>
>>   match goal with [ |- match ?n with _ end ] =>  destruct n end.
>>
>> This doesn't work. Replacing _ with _ =>  _ doesn't work, either, and
>> neither does work anything that I managed to invent.
>>
>> Is there a way to achieve what I'm trying to do? namely, say,
>> "destruct" all variables that are being the head of a match?
>>
>
> The only way I know is to write a pattern that includes the [O] and [S]
> cases explicitly.  You can safely leave underscores for the case bodies and
> pattern variables, but Coq needs to know which inductive type you're
> matching on.
>

Thanks, but the following statement also doesn't work.

  match goal with [ |- match ?n with | O => _ | S _ => _ end ] =>
destruct n end.

Which way are you refering to?

By the way, I still don't understand why Coq needs type information in
this case, if Ltac is untyped and operates over syntax...

-- 
Eugene Kirpichov
Web IR developer, market.yandex.ru