coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Théo Zimmermann <theo.zimmi AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] goal selectors; tactic expressions
- Date: Fri, 25 Jan 2019 15:18:16 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua1-f46.google.com
- Ironport-phdr: 9a23:HIVXuRO3eVNRKIWCpxol6mtUPXoX/o7sNwtQ0KIMzox0Lfn9rarrMEGX3/hxlliBBdydt6oUzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlLiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0vRz+s87lkRwPpiCcfNj427mfXitBrjKlGpB6tvgFzz5LIbI2QMvd1Y6HTcs4ARWdZUclRWS5ODIOyYYUMEuQPI/pXoYbmqlsStBuzHxWgCP/zxjJKgHL9wK000/4mEQHDxAEuAdIOt27TrNrtN6gSUOW1zKzWwjXZavNZwzH96I7VeR0mvfGMXax/cc3LxUguFgPFi1CQqY3+MjOa0+QCqWmb7+56We2zjG4nrhh8rz6yzckvkonEnpwZxkzA+Cljw4s4Jce0RFBlbdK6CpdduCCXOo1rSc04WW5oojw1yrgetJ67YicKzJMnygbaa/OdcoiI5gvvVPuLLjtlnX5ldr2yiheo/Uivze38Uca00FJUoSZfjtbMsXUN2wTS6siBVPR94l+s1SiT2w3X8O1JIkA5mbDFJ5I/3LI8jJUevEXbEi/zgkr2jauWdks++uiv7uTqeqnmpp+COI9zkA3/M6Uumsm6AeQ5KQUOUG2b9v691L3n50H2XLJKjvgunqnDrJ/aPdgbprK+AwJNzokj7A+/Ay6639QcgHkIN0lIeAmHjojsI1HBOur0Dfa5g1S2kTdk3erKPrP7AsaFEn+Wu7D4NZ159kQUnAE01JVU449eIrAHOvP6HEHr4o/2FBg8ZjC0QuHQOtR4044EXGuJBOfNLKPfthma5+cqIsGDYYYUvHD2LP1ztK2mtmMwhVJIJfrh5pAQcn3tW60+exzIM0qpuc8IFCIxhiR7SeXrjFOYVjsKPiS9Wqs94ncwD4f0VN6fFLDou6SI2WKAJrMTfnpPUwneHnLhdoHCUPAJOnrLf51R1wccXL3kcLcPkBGjsAigluhiJ+vQvzAR7NftiIYz6OrUmhU/szdzCpbF3g==
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"
- Re: [Coq-Club] goal selectors; tactic expressions, (continued)
- Re: [Coq-Club] goal selectors; tactic expressions, David Holland, 01/24/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/24/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Cyprien Mangin, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Gaëtan Gilbert, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jason -Zhong Sheng- Hu, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jason -Zhong Sheng- Hu, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Gaëtan Gilbert, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Théo Zimmermann, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Pierre Courtieu, 01/28/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Gaëtan Gilbert, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Cyprien Mangin, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Gaëtan Gilbert, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/25/2019
Archive powered by MHonArc 2.6.18.