The Coq mailing list

[t x <txrev319 AT gmail.com>]

If I'm understand this correctly (and I'm not convinced I am), the essential trick here is to:

* ensure that every tactic "solves" the goal as follows:

1) after it makes progress, create a new evar. Have the evar solve the current state.

2) instantiatte the evar later

Assuming that I understand the above correctly -- can you assume how step (1) is done? I.e. given a goal, how do I generate (in Ltac) an evar that "solves" the goal?

Thanks!

On Sat, Sep 21, 2013 at 8:44 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

It may already be possible to do such a thing with auto, though I have not tried this.  (I'm writing from my phone at an airport.)  You can try [let T := fresh in evar (T : Type); cut T; subst T; [ solve [ eauto with my_db ] | ]; instantiate; intros], where my_db should include a very low priority hint which can solve any goal with an evar H whose type is an evar, by reverting all other hypotheses (using is_evar to distinguish the hypothesis you don't want to revert), and then doing exact H (again finding the relevant hypothesis using is_evar).  Again, I haven't tested this, so I'm not completely sure that it will work.  Also, I think it won't work for hints which generate more than one goal which isn't completely solvable.  You might be able to pull a trick where you try to solve each goal with (fst H), then (fst (snd H)), and so on, so that your evar is resolved into a product, and then you instantiate the extra component at the very end with something like [repeat (exact tt || split)] between the instantiate and the intros.

-Jason

On Sep 21, 2013 3:38 PM, "Pierre Courtieu" <Pierre.Courtieu AT cnam.fr> wrote:

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