The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Does this amount to saying that `repeat` is (unexpectedly) not a
multi-goal tactic?
If yes, should we change this?

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"