The Coq mailing list

[Brandon Moore <brandon_m_moore AT yahoo.com>]

> On 2001-03-21 9:18:54 AM Thomas Strathmann 
> <thomas AT pdp7.org>
>  wrote:

> Subject: Re: [Coq-Club] Iterating Ltac tactics
> 
> On 3/21/11 15:10 , Adam Chlipala wrote:
> > Thomas Strathmann  wrote:
> >> I've yet to find a way to apply a tactic T again and again to  the
> >> current goal exactly like
> >> 
> >> T. T. T. T.  T. ...
> > 
> > Perhaps [repeat T] would do? None of the structured Ltac  support
> > duplicates exactly the semantics of the period operator, as far  as I
> > know, but that's a feature, not a bug. :)
> 
> Sadly, it doesn't.  I should have mentioned that [repeat T] behaves like 
> [T] in 
>this particular  situation. I had this ominous feeling that it might be a 
>feature that what I  want to do is not supported (directly).
> It's not earth shattering, but it  would have been nice to be able to 
> automate 
>just a tad more given that among  other reasons I was drawn to Coq because 
>of 
>the automation  facilities.

I'm having trouble thinking of a case where repeatedly applying T works, but 
adding a ; (try T) somewhere earlier
in the derivation is not successful.

Please provide a bit more detailed example.

I've found ; is almost always usable, but you may have to group some manual 
steps with [|], so that
a case split plus some subsequent solving is a single tactic expression you 
can 
extend with ; try T.
abbreviations here can be helpful

I'll often manually work out some proof steps like

destruct x. A (* solve first case *). B (* solves second case *). (* now, 
lots 
of leftover cases T solves *)

Then group them as

destruct x;[A|B|..].

which can be completed like

destruct x;[A|B|..];solve[T].

The abbreviations can be pretty handy:

http://coq.inria.fr/refman/Reference-Manual012.html#htoc306

You haven't mentioned existential variables, but if they are
involved then "instantiate" might help. It applies all the instantiations
made in earlier branches of a [||] split to the current goal, to replace
the effect of "." automatically propagating the instantiations to
other remaining goals after applying your tactic.

Brandon