The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi, it is obviously the same syntactic factor, the match ... end
acting like the parenthesis here.

Actually you have to make a choice, either you use ";[]" (i.e. what
you did but mistakenly wrote ";[>]") and you lose associativity. Or
you use "[>]" and ";" and you have associativity but it is a bit more
verbose to apply tactics locally like you did.

So either you write

induction h; (eapply derivI;[ NLrule_I | ]).
but you need the parenthesis.
or
induction h; [> eapply derivI;[> NLrule_I | ]..].
which is a shortcut for this:
induction h; eapply derivI;[> NLrule_I | | NLrule_I | | NLrule_I | |
NLrule_I | | NLrule_I | |NLrule_I | |NLrule_I | ].
which is not intuitive but associative:
induction h; (eapply derivI;[> NLrule_I | | NLrule_I | | NLrule_I | |
NLrule_I | | NLrule_I | |NLrule_I | |NLrule_I | ]).
(induction h; eapply derivI);[> NLrule_I | | NLrule_I | | NLrule_I | |
NLrule_I | | NLrule_I | |NLrule_I | |NLrule_I | ].

You can also write it like this:
induction h; eapply derivI; only 1,3,5,7,9,11,13:NLrule_I.

all of these formulation being associative.

Most people use ;[] as it is how we think about tactic composition.
And being non associative is generally not a problem.

Hope this helps

Pierre

Le jeu. 15 août 2019 à 19:52, David Holland 
<dholland-coq AT netbsd.org>
 a écrit :
> I have also found that you can work around these problems by inserting
> a dummy match, along these lines:
>
>    induction H;
>    match goal with
>    | [ |- _ ] => eapply derI; [ apply NLrule_I | ]
>    end.
>
> After reading the rest of this thread I'm now not sure if this is a
> consequence of the same syntactic factors or whether the matching
> does actually changes the way the goals are processed like I
> originally thought it did. :-/