The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Robin Green wrote:
> I have just used the "generalize foo at i j k ..." tactic form for the
> first time (well, I think it's the first time I've used it, anyway). I
> used it to solve a problem with dependent types that I couldn't see any
> other reasonable way to solve. Now that I've actually used it, I am
> relieved to finally understand how the random-looking list of numbers
> one finds at the end of generalize ... at ... tactics can be rationally
> arrived at. And, indeed, the numbers at the end of its cousin,
> pattern ... at ... (e.g. in le_uniqueness_proof in the Coq FAQ).
>
> I am interested to know in what situations other people use these
> particular variants of generalize and pattern - I wonder if I should be
> using them more often.
>   

Any use of [generalize] can be replaced by an application of a new 
lemma.  I generally try to solve the kind of problem that you refer to 
by figuring out the right lemmas, rather than by including opaque lists 
of occurrence numbers in proof scripts.