The Coq mailing list

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

On 07/14/2013 11:14 AM, Michiel Helvensteijn wrote:
> On Sun, Jul 14, 2013 at 4:37 PM, Adam 
> Chlipala<adamc AT csail.mit.edu>
>   wrote
> > I suggest looking into an even more automated proof style (described in CPDT),
> >      
> Sounds good. Could you perhaps point me to the right chapter or give
> me an example of the technique you would recommend in my case?
>    

It's hard to point to a specific chapter.  Chapter 14 is most directly 
relevant, but the earlier chapters build up to that point by applying an 
automated proof style from the start.

> > where there is no inherent case order in your scripts, not even at the level
> > found in your first script below.
> >      
> The only inherent case order in my `match` script is that the wildcard
> pattern never matches `case2` because it is given last. And that might
> actually be considered a "good thing", as it saves typing.
>    

Maybe, though, your problem domain actually admits some simple proof 
automation, such that there's no need to think about case split details 
yourself.