The Coq mailing list

[Eugene Kirpichov <ekirpichov AT gmail.com>]

Hello, coq-club.

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?

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