The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Have you read CPDT <http://adam.chlipala.net/cpdt/>?  I suggest looking 
into an even more automated proof style (described in CPDT), where there 
is no inherent case order in your scripts, not even at the level found 
in your first script below.

On 07/14/2013 10:10 AM, Michiel Helvensteijn wrote:
> 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.
>