The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

The problem is that repeat runs on goals independently
So if you have goals [1,2] and run "repeat foo"
it will run foo on goal 1, if this fails ignore the failure, if it 
succeeds run repeat on the generated subgoals
then it will run foo on goal 2, if this fails ignore the failure, etc
it never goes back to goal 1

in other words, repeat tac = for goal in goals (only goal: if progress 
tac then repeat tac else idtac)
(plus some subtleties wrt the fail tactic)

meanwhile OP wants something more like
repeat tac = if progress (for goal in goals (only goal: try tac)) then 
repeat tac else idtac

Gaëtan Gilbert

On 25/01/2019 14:46, 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.
>
> 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"