The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Mon, 21 Mar 2011 15:18:54 +0100,
Thomas Strathmann 
<thomas AT pdp7.org>
 a écrit :

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

Can you tell us more of your "T" tactic and the context where you want
to apply it a certain number of times?

For me, having a tactic which performs a "T.T.T. …" until it fails
would be one of the nightmarest to debug!

If you want your tactic to act in the subgoals which are not in its
scope, you may tell the tactic which generate them to use your tactic:

If your context is like this one:
destruct X.
  (* first case of X *)
  apply x.
 (* second case of X *)
 T.
(* third case of X *)
T.

and you want to do:
destruct X.
 (* first case of X *)
 apply x.
(* all the other cases *)
dot_repeat T.

then you may consider:
destruct X; try T.
(* first case of X *)
apply x.
(* all the other cases are solved *)

Note that it is very specific, since if the first case would have use
of T, and not the second, what you want wouldn't be that helpful.

Also note that the last solution can also be replaced by:
destruct X; repeat T.
(* first case of X *)
apply x.
(* all the other cases are solved *)