The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

Hi,
As Cyril suggest, auto is a "searching" tactic, in contrast with for
example intuition that is a "advance without risk" tactic.

When auto applies successfully a tactic it tries to prove the
generated subgoals but if it fails to prove all of them recursively
(stopping at a certain depth) then it backtracks and tries another
tactic (and again recursively try to prove subgoals). Failing to
finish the proof is the base case of the recursion, and we need it.

What you want with your repeat (... if we can apply x, apply x) is
much simpler: there is no backtrack.

I suggest the following tactic:

Ltac mytac := repeat (apply L1 || apply l2 || apply l3 || ....).

where Li are the lemmas you want to use. But be aware that if at some
point L1 and L2 can be applied, L2 will never have a chance (unless it
is still applicable after applying L1).

The question of having a hint database for such tactic instead of
writing one single tactic with so many "apply" is a good question
anyway.

Best regards,
Pierre



2013/9/21 Cyril Cohen 
<cohen AT crans.org>:
> Hi,
>
> Le 21/09/2013 18:25, t x a écrit :
>> To check if I understand your logic correctly --
>>
>> Suppose we defined "agressive_auto" =
>>   // this is probably not really correct
>>   repeat (
>>     forall x in Hint Extern (sorted by precedence);
>>       if we can apply x, apply x
>>   )
>>
>> Then basically, the property of "don't change state if it can't be proved" 
>> can
>> be simulated with:
>>
>>   solve[ agressive_auto ];
>>
>> and the property of never fail can be simulated with
>>
>>   try( solve [ agressive_auto ] );
>>
>> in which case, auto "sorta =" try (solve [agressive_auto]) ?
>
> What you suggest would work only when there is only one possible path (or no
> backtracking).
>
> Best,
> --
> Cyril Cohen