The Coq mailing list

[Fabian Kunze <kunze AT ps.uni-saarland.de>]

Hi,

; is associative, but you are using a different operator, namely the combinator "t;[ ...]" (There is no primitive "[...]"). It works only when giving a tactic for each goal opened by t, and therefore "t1;t2;[...]", which is parsed as "(t1;t2);[...]", behaves differently then t1;(t2;[...]).

Best,

Fabian

On Mon, 5 Aug 2019, 17:34 Jason -Zhong Sheng- Hu, <fdhzs2010 AT hotmail.com> 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
>>>