The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

Hi Jason,

In fact there is a long chain of emails earlier this year with the 
subject Re: [Coq-Club] "Sequence is associative." (?)

It seems that pure ; which you'd expect not to be associative, but is,
but it seems that ... ; ... ; [ ... ] is different

coq version is opam-coq.8.8.2/4.02.3 (not sure exactly what this means, 
but is what I get from "which coqtop"

Cheers,

Jeremy

On 8/6/19 1: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
>>>>