The Coq mailing list

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

Hi Jason,

I have tried this, I get

induction H ; eapply derI ; [ NLrule_I | ].
 > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Tactic failure: Incorrect number of goals (expected 14 tactics).

ie, exactly the same problem.   (I agree that the documentation seems to 
say it would do what I want).

Cheers,

Jeremy

On 8/5/19 3:56 AM, Jason -Zhong Sheng- Hu wrote:
> Hi Jeremy,
> 
> have you tried
> 
> eapply derI ; [ NLrule_I | ].
> 
> notice that > is dropped. you can read it from the refman: 
> https://coq.inria.fr/refman/proof-engine/ltac.html#coq:tacn.dispatch
> The tactic language — Coq 8.9.0 documentation 
> <https://coq.inria.fr/refman/proof-engine/ltac.html#coq:tacn.dispatch>
> The tactic language¶. This chapter gives a compact documentation of L 
> tac, the tactic language available in Coq.We start by giving the syntax, 
> and next, we present the informal semantics. If you want to know more 
> regarding this language and especially about its foundations, you can 
> refer to .Chapter Detailed examples of tactics is devoted to giving 
> small but nontrivial use examples of this ...
> coq.inria.fr
> 
> /Variant/ |expr_0 
> <https://coq.inria.fr/refman/proof-engine/ltac.html#grammar-token-expr> 
> ; [expr_i 
> <https://coq.inria.fr/refman/proof-engine/ltac.html#grammar-token-expr>*|]|
> 
>     This variant of local tactic application is paired with a sequence.
>     In this variant, there must be as many |expr_i
>     <https://coq.inria.fr/refman/proof-engine/ltac.html#grammar-token-expr>|
>     as goals generated by the application of |expr_0
>     <https://coq.inria.fr/refman/proof-engine/ltac.html#grammar-token-expr>|
>     to each of the individual goals independently. All the above
>     variants work in this form too. Formally, |expr
>     <https://coq.inria.fr/refman/proof-engine/ltac.html#grammar-token-expr>
>     ; [ ... ]| is equivalent to |[> expr
>     <https://coq.inria.fr/refman/proof-engine/ltac.html#grammar-token-expr>
>     ; [> ... ] .. ]|.
> 
> I suppose this is what you want.
> 
> *Thanks,*
> *Jason Hu*
> *https://hustmphrrr.github.io/*
> ****
> ------------------------------------------------------------------------
> *From:* 
> coq-club-request AT inria.fr
>  
> <coq-club-request AT inria.fr>
>  on behalf 
> of Laurent Thery 
> <Laurent.Thery AT inria.fr>
> *Sent:* August 4, 2019 1:14 PM
> *To:* 
> coq-club AT inria.fr
>  
> <coq-club AT inria.fr>
> *Subject:* Re: [Coq-Club] how to combine tactics
> Hi Jeremy,
> 
> the selector you try to apply seems to be work globally and not locally
> like you think. As a ssreflect user,
> 
> https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html
> 
> I will use the ssreflect tactical first to solve your goal
> 
> ================================================
> 
>  From Coq Require Import ssreflect.
> 
> Inductive Seven := one | two | three | four | five | six | seven.
> 
> Definition  double (x : Seven) := x.
> 
> Lemma derivI : forall (n y : Seven), y = y -> double n =  double n ->  n
> = n.
> Proof. now trivial. Qed.
> 
> Ltac NLrule_I := trivial.
> 
> Goal forall h : Seven, h = h.
> Proof.
> induction h; (eapply derivI; first NLrule_I).
> 
> ================================================================
> 
> 
> 
> As I usual
> 
> 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
>>