The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

Hi all!

I'm defining some functions using proof techniques. I like the
interactive mode. Still, often I'll need to match on an instance of an
inductive type like so:

exact match X with
  |  case2 _ a => a
  |  _  => b.

But that's a lot to type without any intermediate feedback. I'd rather
use interactive mode. I can switch to the 'case' or 'destruct' tactic:

case X.
(* case1 *) exact b.
(* case2 *) exact a.
(* case3 *) exact b.
(* case4 *) exact b.

But there are two important problems with this approach. First of all,
I have to retype "exact b" a number of times now. The one fix I found
for this is not very pretty, but:

Ltac tac := exact b.
destruct X; [ tac | | tac | tac ].
(* case2 *) exact a.

Even if I was happy with this notation, there is still the other
problem: this technique is sensitive to the textual order of the
inductive type definition. I'd rather recognize cases by their
constructor.

Is there a way to have my cake and eat it too?

Thanks!

--
www.mhelvens.net