The Coq mailing list

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

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
>>