The Coq mailing list

[Li-yao Xia <lysxia AT gmail.com>]

The manual presents "... ; [ ... | ... ]" as a separate construct from 
"... ; ...", that's one way to keep the latter associative:

https://coq.inria.fr/refman/proof-engine/ltac.html#coq:tacn.dispatch

Li-yao

On 8/5/19 11:34 AM, Jason -Zhong Sheng- Hu wrote:
> this is surprising. I've been using [...|...] and I experienced nothing like 
> this. if my memory did not fail me, I read somewhere that ; is associative. 
> what's your coq version?
>
> Thanks,
> Jason Hu
> https://hustmphrrr.github.io/
> ________________________________
> 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: August 5, 2019 9:44 AM
> To: 
> coq-club AT inria.fr
>  
> <coq-club AT inria.fr>
> Subject: Re: [Coq-Club] how to combine tactics
>
> Further to my previous messages I have experimented some more, and find that
>
> induction H ; (eapply derI ; [ NLrule_I | idtac]).
>
> does work.  Ie the parentheses are needed, and make a difference, in
> this case.
>
> (contrast tac1 ; tac2 ; tac3 where parentheses don't make any
> difference, though I would have expected them to).
>
> Cheers,
>
> Jeremy
>
> On 8/5/19 11:27 PM, Jeremy Dawson wrote:
> > Hi Laurent,
> >
> > I'm guessing you mean something like this (but not exactly)
> >
> > induction H ; (eapply derI; [apply: NLrule_I | idtact]).
> >
> > but not exactly, since it gives this error
> >    >                                   ^
> > Error:
> > Syntax error: '<-' or '->' or [constr_with_bindings_arg] expected after
> > 'apply' (in [tactic:simple_tactic]).
> >
> > I've never seen the "apply:" construct, can you clarify?
> >
> > Thanks
> >
> > Jeremy
> >
> >
> > On 8/5/19 3:22 AM, Laurent Thery wrote:
> > > If you are sure that  eapply derI always generates 2 subgoals,
> > >
> > > you can of course do (eapply derI; [apply: NLrule_I | idtact]).
> > >
> > >
> > > On 8/4/19 3:57 PM, Jeremy Dawson wrote:
> > > > Hi,
> > > >
> > > > I have a tactic eapply derI
> > > > which when applied to a goal produces two resulting goals.
> > > > Of these two I want to apply the tactic NLrule_I to the first one.
> > > > The tactic induction H results in 7 goals.
> > > >
> > > > So when I try
> > > > Proof. intros. induction H ; eapply derI ; [> NLrule_I | ].
> > > > I get the error (not unexpected)
> > > > Error: Incorrect number of goals (expected 14 tactics, was given 2).
> > > >
> > > > When I try
> > > > Proof. intros. induction H ; (eapply derI ; [> NLrule_I | ]).
> > > > I get the same error, which I don't understand at all
> > > > (though the fact that putting in parentheses doesn't have the
> > > > expected result has been discussed on this list previously).
> > > >
> > > > When I try
> > > > Ltac derI_NLr := eapply derI ; [> NLrule_I | ].
> > > > Proof. intros. induction H ; derI_NLr.
> > > > although sometimes defining a tactic using Ltac
> > > > has previously given me what I want and expect,
> > > > in this case again I get the error
> > > > Ltac call to "derI_NLr" failed.
> > > > Incorrect number of goals (expected 14 tactics, was given 2).
> > > >
> > > > How do I apply eapply derI to all goals, then NLrule_I to
> > > > the first subgoal resulting from each instance of eapply derI?
> > > >
> > > > Thanks,
> > > >
> > > > Jeremy