The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Kenneth Roe wrote:
> Now on to the next issue--the call to the tactic solvePick2Vars at the 
> very end of the example I've attached seems to go into an infinite 
> loop (or at least is very slow).  Can anyone tell me what is happening?

Isn't your algorithm here exponential time, such that it shouldn't be 
surprising that the algorithm runs for a long while for n = 12?  
(Constant factors in Ltac aren't very good in the first place!)

> Does auto implement backtracking?  My impression was that it just 
> keeps applying its rules until none are applicable.

Yes, [auto] does backtracking; no, [auto] doesn't keep applying rules 
until none are applicable.  The depth argument to [auto] (which is 
mandatory and defaults to 5) determines the depth of the search tree, so 
there is always a cut-off point, even when further rules apply.

I just checked the manual and was surprised to see that, indeed, it is 
not at all clear there that [auto] backtracks!  The hint is the text 
"Prolog-like resolution procedure."