The Coq mailing list

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