The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

On 01/26/2019 12:46 AM, Jason -Zhong Sheng- Hu wrote:
> It's strange that solve_eqs can succeed twice but repeat fails to 
> execute it more than once. You can try in the first goal `repeat 
> solve_eqs` only and see if it solves the goal.
> 
No, it doesn't.  As I have been led to expect, it does exactly the same 
as 1 : repeat solve_eqs. (see below).

> How's solve_eqs defined though? There seems like some problem with it.
> 
I don't see why you should suggest that.  Anyhow, it's not the point of 
my question, which was how to repeatedly apply a (any given) tactic to 
all current subgoals.

Cheers,

Jeremy

> *Sincerely Yours,
> *
> *
> Jason Hu*
> ------------------------------------------------------------------------
> *From:* 
> coq-club-request AT inria.fr
>  
> <coq-club-request AT inria.fr>
>  on behalf 
> of Jeremy Dawson 
> <Jeremy.Dawson AT anu.edu.au>
> *Sent:* January 25, 2019 8:37 AM
> *To:* 
> coq-club AT inria.fr
> *Subject:* Re: [Coq-Club] goal selectors; tactic expressions
> Hi Jason,
> 
> No, I used { on a subgoal, which subsequently gave two subgoals at the
> point at the start of the output shown in my email below
> 
> Cheers,
> 
> Jeremy
> 
> On 01/26/2019 12:32 AM, Jason -Zhong Sheng- Hu wrote:
>> Are you in an assert or something? all: won't catch a goal that is not 
>> visible in the current scope.
>> 
>> Thanks,
>> Jason Hu
>> 
>> On Jan 25, 2019 08:19, Jeremy Dawson 
>> <Jeremy.Dawson AT anu.edu.au>
>>  wrote:
>> Hi Gaëtan,
>> 
>> all: repeat solve_eqs
>> doesn't succeed, I don't know exactly what all : repeat solve_eqs does
>> (previous emails addressed this question and the answer I was given)
>> though in this case it's consistent with applying
>> 1: repeat solve_eqs (which leaves one subgoal, so subgoal 2: is the
>> original subgoal 2)
>> then applying 2 : repeat solve_eqs.
>> or maybe just
>> 1: solve_eqs. then 2: solve_eqs. (ie without "repeat", I can't tell)
>> 
>> It doesn't go back to try 1 : solve_eqs again.
>> 
>> eg see the following, where the
>> second application of the tactic
>> all : repeat solve_eqs
>> makes progress beyond the results of the first application of it.
>> 
>> 2 focused subgoals
>> (shelved: 5)
>> 
>>     V : Set
>>     Φ2, Ψ1, Ψ2, Γ1 : list (PropF V)
>>     Q : PropF V
>>     sel1, l, l1 : list (PropF V)
>>     ============================
>>     ((Γ1 ++ Q :: sel1) ++ l ++ Φ2, Ψ1 ++ l1 ++ Ψ2) =
>>     (?Γ1 ++ ?Q :: ?Γ2 ++ ?Γ3, ?Δ)
>> 
>> subgoal 2 is:
>>    G ++ (?Γ1 ++ ?Γ2 ++ ?Q :: ?Γ3, ?Δ, d0) :: H6 =
>>    G ++ ((Γ1 ++ sel1) ++ l ++ Q :: Φ2, Ψ1 ++ l1 ++ Ψ2, d0) :: H6
>> 
>> gen_moveL < all : repeat solve_eqs.
>> 1 subgoal
>> 
>>     V : Set
>>     Φ2, sel1, l : list (PropF V)
>>     ============================
>>     sel1 ++ l ++ Φ2 = (sel1 ++ l) ++ Φ2
>> 
>> gen_moveL < all : repeat solve_eqs.
>> This subproof is complete, but there are some unfocused goals.
>> Try unfocusing with "}".
>> 
>> Cheers,
>> 
>> Jeremy
>> 
>> 
>> On 01/25/2019 08:53 PM, Gaëtan Gilbert wrote:
>>> Note that repeat runs the inner tactic focused on each goal separately
>>> so "repeat (all: solve_eqs)" would (if the syntax allowed it) be the 
>>> same as "repeat (only 1: solve_eqs)" which is also the same as "repeat 
>>> solve_eqs", and "repeat (only 2: solve_eqs)" is the same as "repeat 
>>> fail" ie idtac.
>>> 
>>> I feel like "all: repeat solve_eqs" should work given what you describe, 
>>> can you explain how it fails?
>>> 
>>> Gaëtan Gilbert
>>> 
>>> On 25/01/2019 06:54, Jeremy Dawson wrote:
>>>>
>>>> Hi Cyprian,
>>>>
>>>> What I wanted is what I would express as
>>>> repeat (all : solve_eqs)
>>>> but it seems as though that form is forbidden.
>>>>
>>>> The various things I tried as indicated in my earlier email were simply
>>>> looking for alternatives that work.
>>>>
>>>> Detailed background to what I want: solve_eqs doesn't seem to enlarge
>>>> the number of goals in the cases where I want to use it, and sometimes
>>>> solves a goal, sometimes only after solve_eqs has instantiated an evar
>>>> in another goal, sometimes only after being repeatedly called on the
>>>> same goal (where each time it simplifies the goal)
>>>>
>>>> Cheers,
>>>>
>>>> Jeremy
>>>>
>>>>
>>>> On 01/25/2019 10:00 AM, Cyprien Mangin wrote:
>>>>> What you probably meant is something like "all : repeat solve_eqs"