The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 11/09/2016 11:43 AM, Soegtrop, Michael wrote:
> Dear Jonathan,
>
> thanks for pointing out the Tactic Notation trick! I give it a try. I would 
> make sure that I do this in a way so that I can use sed to change to whatever 
> other mechanism for this is supported in future versions of Coq.

Would you consider running the Coq scripts through a macro preprocessor, 
so that those ugly foo/bar redefinitions can be abstracted into a macro?

I recall once asking someone whether there was a way to place a macro 
preprocessor between coqtop and its IDE (PG in my case), but I don't 
recall the answer...

>   This method might be much faster than the eauto method I use currently, 
> because eauto repeatedly checks all hints if they solve the goal, which is 
> never the case in this situation and thus a waste of time.

One feature of typeclasses eauto is that it prunes the search space a 
bit.  It won't backtrack to alternative successes in a non-depended-on 
subgoal - because such alternative successes can't possibly have an 
impact on the overall proof (except to waste time).  I'm not sure that 
will help in your situation, though.

-- Jonathan