The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

Stefan Monnier wrote:
> The problem I have with separate lemmas is that it forces you to write the
> whole statement (i.e. type) of the lemma, which may be large and is
> otherwise automatically computed/inferred by Coq.

Even that forces you to know the order in which the inductive cases are 
generated, to match cases with names in a sensible way.  My personal 
preference is for working toward automating all proofs, meaning not 
using any tactics that refer to variables/hypotheses by name, except for 
initial 'induction' invocations and similar.  This obviously doesn't 
lead to readable proof argument that tell "why" a theorem is true, but 
I'm very skeptical that such arguments will ever exist for proofs about 
real software systems, for instance.  Thus, I think it makes sense to 
focus just on establishing that theorems hold and leave the "readable" 
step-by-step proofs for results simple enough to fit in a conference 
paper in informal form (in other words, not proofs about real systems!).