The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

The eauto tactic has an undocumented bfs mode, which is triggered via [eauto <arbitrary number> <maximum cost/depth>], I believe.  Does this side-step your problem? 

-Jason

On May 1, 2014 9:46 PM, "Jonathan" <jonikelee AT gmail.com> 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.

Suppose there was a tactic "eauto_step Cost" that takes one eauto step (not idtac) with cost < Cost.  Then I could write:

  Hint Extern 999 => my_tactic; eauto_step 999.

Then eauto wouldn't ever get caught in a "my_tactic; my_tactic; my_tactic..." loop.  But, it could run as often as needed, as long as some intervening step with cost < 999 ran in between.

The problem with looping is made worse because my_tactic has several (4, actually) alternative successes in it - so without something like eauto_step, "Hint Extern 999 => my_tactic" would blow up exponentially, making eauto searches of even moderate depth take way too long.

That would be an acceptable solution, I think.  Not ideal - because it looks like one would have problems with multiple such tactics.

-- Jonathan

On Thu, May 1, 2014 at 3:15 PM, Jonathan <jonikelee AT gmail.com> wrote:

I'm trying to write an extern hint for eauto that does some rearrangement
of terms for the benefit of other eauto hints. Unfortunately, this hint
sometimes causes eauto to loop forever because it is always applicable
immediately after itself (and there isn't any easy way to make it fail only
after itself).

  It seems I could break the loop if I could force eauto to take any lower
cost step prior to using that hint again.

Does anyone know if there is a way to accomplish this?

-- Jonathan