Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] goal selectors; tactic expressions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] goal selectors; tactic expressions


Chronological Thread 
  • From: Pierre Courtieu <pierre.courtieu AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] goal selectors; tactic expressions
  • Date: Mon, 28 Jan 2019 17:42:02 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f45.google.com
  • Ironport-phdr: 9a23:m4JEqRUtZsZDfcm5g/KZM+V+NqnV8LGtZVwlr6E/grcLSJyIuqrYYxyGt8tkgFKBZ4jH8fUM07OQ7/iwHzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9xIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KpwVhTmlDkIOCI48GHPi8x/kqRboA66pxdix4LYeZyZOOZicq/Ye94RWGhPUdtLVyFZDYy8YYkAAeoPM+hbsofzuUcBoxSlCAmwHePi0CNEimPq0aA41ekqDAHI3BYnH9ILqHnattT1O7kIUeCv0qbD0CvOb/RL2Tfn9IjIcw4uoeyRVr93acrRyFcgFxnfjlqOs4DqIzSV1vkXs2iH7upvS/+vhnUoqwF0uDevx8MshpPViYISz1DJ7CN0y5s2K92gUEN3f8KoHZ9KuyyZN4Z6WN4uTmBptSogxbALuZi2dzUQxps93R7QcfmHfpCI4h39UOaRJi91hHd/d7K+gxa+6EmgyurhWsWt3lZHoSpInsPDtnAK0BzT5cyHReVn8ki93jaP0hjf6uBCIU8qiarWM4AtzqI0m5YJsknOHjX6lFj3gaKXbEkp9eil5/ziYrr8p5+cM4F0ihv5MqQrgsG/GeU4PRYUX2iB5+uwzqHs/UrkQLVQkv02k7fWsI3BKMQUo662GQ5V0oI55xmjCDem1cwUnWMbI1JdZBKHk4/pNknSL/D/FPezmkijkDN2x//dJbDhGZXMLn3bkLj7Z7p96khcyBAyzd9F/Z5UBKsBc7rPXRras8WQJRskOUTgyOH+Td55y4k2WGSVA6bfPrmE4nGS4ed6G+iBfpUY8B36NuI55vPzxSshmFIHZ6Tv1pwKcmy5E+lOLECQYH6qidAERzRZ9jEiRfDn3QXRGQVYYGy/CudlvmliWdCWSLzbT4Xou4SvmSKyH5lYfGdDUwneHnLhdoHCUPAJOnvLfp1R1wccXL3kcLcPkAm0vVajmbViJ+vQvCYfsMC7jYUn16jojRg3sAdMIYGd3mWKFTwmm2oJQ3o32/k6rxAgjFiE1qd8jrpTEtkBv/4=

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"



Archive powered by MHonArc 2.6.18.

Top of Page