The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 05/01/2014 09:45 PM, Jonathan wrote:
> On 05/01/2014 08:34 PM, Gregory Malecha wrote:
> > Hi, Jonathan --
> >
> > A usual way to prevent this is to introduce a hypothesis at the end 
> > of the
> > tactic and then look for it at the beginning and fail if you find it. It
> > isn't the most elegant solution, but it does work. To be concrete (code
> > untested):
> >
> > Definition Stop := True.
> >
> > Ltac my_tac :=
> >    match goal with | H : Stop |- _ => fail 1 | |- _ => idtac end ;
> >    ...your tactic... ;
> >    assert (Stop) by (exact I).
>
> Thanks for the response, Gregory.  In the example you give above, the 
> problematic tactic won't run again after some other eauto step runs.  
> In other words, the above solution works if you want an extern hint to 
> run at most once during an eauto search.  But I want it to run as 
> often as necessary, but not (much) more than that.

I dismissed this approach too quickly.  I'm now using something very 
similar.  The trick is to have the blocking hypothesis (H: Stop above) 
capture the goal's consequent type as a parameter, and then prevent the 
problematic tactic from running until the goal changes sufficiently such 
that its consequent no longer matches the captured one.

See the domemoed tactic in memo.v and its use in common.v in 
https://github.com/jonleivent/mindless-coding for details.

-- Jonathan