The Coq mailing list

[Thomas Strathmann <thomas AT pdp7.org>]

On 3/21/11 15:33 , AUGER Cedric wrote:
> Can you tell us more of your "T" tactic and the context where you want
> to apply it a certain number of times?

The tactic T in this case does nothing more fancy than applying the 
constructors of an inductively defined relation (reduction relation for 
a combinatory logik) based on what the head of the term to be reduced 
looks like (i.e. if it's a weak redex like [S x y z], a weak normal form
or the application of a weakly reducible term to another term that may 
or may not be already in normal form). Invoking the rules dealing with
transitivity and "uncovering" a weak redex that is "buried" under a 
(number of) applications necessarily produces more than one subgoal, but 
after those are proved I'm left with just one goal and in most cases I 
can actually solve the whole obligation by repeating T a number of times 
using the . tactical (or whatever else I should call it). I suspected 
that there's some conceptual error on my part, but because of your 
replies I am now pretty certain that I should reorganize the tactic and 
have made some progress towards a (partial) solution to my original 
problem. But, as I already mentioned, it's not really that important for 
the overall development, and so it's kind of on the back burner for now. 
Thanks for all your kind replies and offers of help, but I have had the 
experience that in order to really understand something it's not 
sufficient to look at solutions or hints provided by other people, but 
to come up with a solution oneself (apart from the fact that sadly I 
don't really have the time to engage in a discussion of particulars of 
my development).

        Thomas