Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Ltac-matching a "match..with"

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Ltac-matching a "match..with"


chronological Thread 
  • From: Eugene Kirpichov <ekirpichov AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Ltac-matching a "match..with"
  • Date: Sat, 30 Jan 2010 00:27:57 +0300
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=eKMvALA+b3gC8sXECAQcOtjx3NhG2turFfqquFCRQ7214ZIu+TxKxcL2Fw60JWIj7W uVyHxP92tFn77fZ8kSWcqIn1QDs7cJNN1X1/5W3Mo3AkavAEKaiDVoUnaN+to3tik/DE FoLnkLjbbRV+ZfRq96EdjbqugKLAxTuxnScQE=

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



Archive powered by MhonArc 2.6.16.

Top of Page