The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Le ven. 25 janv. 2019 à 15:19, Théo Zimmermann 
<theo.zimmi AT gmail.com>
 a écrit :
>
> Does this amount to saying that `repeat` is (unexpectedly) not a
> multi-goal tactic?

It seems so. And it is actually documented as such iiuc.

do n tac is a multigoal tactic for instance.

> If yes, should we change this?

Yes probably. Actually we should provide both semantics but the single
goal repeat is easy to redefine in ltac.



> Le ven. 25 janv. 2019 à 14:54, Gaëtan Gilbert
> <gaetan.gilbert AT skyskimmer.net>
>  a écrit :
> >
> > 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"