The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

I just realized the problem.  My intent was to have an n*m algorithm where n and m are the number of leaves in the two trees.  However the way I had the search setup before, the ComposeFirst... and ComposeSecond... rules could be arbitrarily interleaved causing an exponential explosion.  I have attached the corrected code.  It executes very quickly.

                   - Ken

> Date: Thu, 28 Jul 2011 20:08:00 -0400
> From: adam AT chlipala.net
> To: kendroe AT hotmail.com
> CC: coq-club AT inria.fr
> Subject: Re: [Coq-Club] Ltac infinite loop (or at least very slow
>
> 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."

Attachment: test.v
Description: Binary data