The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Well, as I've just wrote in the aforementioned tracker issue (#3969), the solution is not due to repeat. But to the goal-distribution tactic `[> t..]`. Indeed it's important, here, to keep calls to `reflexivity` close to their `constructor`: as Arthur wrote it, all the `constructor`s are called first, then all the `reflexivity`-s and the search-space is just to big. So `all:[> constructor;reflexivity ..]` will work as desired. If other tactics are called later, it is probably wise to call `once [> constructor;reflexivity ..]` because the tactics are not smart enough to figure out that backtracking inside these calls to `constructor` is pointless.

On 30 January 2015 at 21:59, Arthur Azevedo de Amorim <arthur.aa AT gmail.com> wrote:

Great, your black magic work-around seems to work like a charm! Thanks a lot!

2015-01-30 15:54 GMT-05:00 Jason Gross <jasongross9 AT gmail.com>:

> It is not forever.  Just approximately 2 * 10^(number of goals - 4) s.  On
> 10 goals, you should expect to wait about 2 * 10^10 seconds, or over 600
> years.
>
> I've reported this as bug 3969.
>
> Here is a black magic work-around (I'll post a description of how I'm
> guessing this works to the bug tracker):
>   repeat ([ > once (constructor; reflexivity) | .. ])
>
> If you want, you could even do:
>
> Tactic Notation "constructor" tactic3(tac) := repeat ([ > once (constructor;
> tac) | .. ]).
>
> and then [constructor (reflexivity)] does what it used to.
>
>
> On Fri, Jan 30, 2015 at 3:31 PM, Arthur Azevedo de Amorim
> <arthur.aa AT gmail.com> wrote:
>>
>> Dear Club,
>>
>> The CHANGES file for 8.5beta1 states that the old "constructor tac"
>> idiom has been superseeded by "once (constructor; tac)", but I haven't
>> been able to get it to work: right now, putting "once (constructor;
>> tac)" causes the script to run seemingly forever, *even though copying
>> and pasting that line multiple times makes it solve the goal
>> instantly*.
>>
>> I've attached a simplified test case illustrating the behavior.
>>
>> Any ideas on what causes this or how to get it fixed?
>>
>> Thanks!
>>
>> --
>> Arthur Azevedo de Amorim
>
>



--
Arthur Azevedo de Amorim