The Coq mailing list

[Cyprien Mangin <cyprien.mangin AT m4x.org>]

Hi Jeremy,

The confusing thing to understand is that there is always a toplevel goal selector being applied to a tactic.

By default it is "1 : ", so when you write "repeat (only 2 : solve_eqs)", it is equivalent to "1 : repeat (only 2 : solve_eqs)", meaning the inner part will fail due to it having only one goal under focus.

The syntax error you get comes from the fact that a toplevel selector like "1 : " or "all :" cannot be used inside a tactic _expression_, so "repeat (2 : solve_eqs)" is not a valid _expression_.

What you probably meant is something like "all : repeat solve_eqs", or if you want to target specifically the goals 1 and 2, "1-2 : repeat solve_eqs".

Alternatively, "all : repeat (only 1-2 : solve_eqs)." might work, but it might do weird things if the number of goals changes.

Cyprien

On Thu, Jan 24, 2019 at 11:16 PM Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> wrote:

OK, well, no doubt I didn't try for quite the right way of expressing it
but surely being misled on this point wouldn't lead to syntax errors,
would it?

How do I correctly write the tactic I tried to write as
repeat (only 1 : solve_eqs || only 2 : solve_eqs).

And what should
repeat (only 2 : solve_eqs).
do?  I'm guessing that it means the second and subsequent invocations of
apply to the second subgoal produced by the previous invocation of
solve_eqs, but that doesn't explain why nothing happens on the first
invocation.

And what should
repeat (only 1-2 : try solve_eqs).
do?  Again, shouldn't the first invocation of
only 1-2 : try solve_eqs
apply solve_eqs to each of the two subgoals?

Anyway, what I would like to know how to do is to apply a tactic
repeatedly to all the goals in turn, until they are all solved or there
is no further progress

Thanks,

Jeremy

On 01/24/2019 11:05 PM, Laurent Thery wrote:
>
>
> On 1/24/19 5:35 AM, Jeremy Dawson wrote:
>> ow do I write a tactic to repeatedly apply solve_eqs to goals 1 and 2
>> until either both are solved or there is no further progress?
>
> Maybe you are mislead by the fact that the goal numbering is local but
> not global
>
> For example:
>
> Goal (True /\ True) /\ (False /\ True).
> split; only 2 : (split; only 2 : trivial).
>
> solves the 3th goal
>