The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

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.

How's solve_eqs defined though? There seems like some problem with it.

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"