The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Mihai ANDRIES wrote:
> "eapply" sure does the job in my case, but keeping the arguments for 
> my simple "apply" allows me to check easier the proof by hand.

Interesting perspective.  I've never heard someone previously say that 
it's important to be able to "check Coq proofs by hand."

> At the same time, I find that tactics like eapply and eauto obscure a 
> little bit the way the proof is executed.

Right, but the very fact that [eauto] succeeds tells you that the proof 
isn't very interesting and may be best left to automation.

> Explicitly naming the variables in a proof was taught to me as a "good 
> practice" for beginners.

I disagree.  I think working explicitly with names coming from anywhere 
but the theorem statement is an anti-pattern for any Coq development, 
but especially so for beginners.  It's fine and very useful for 
exploratory proving, but a final proof should be automated.

> Is there a reason why the naming of variables is affected by the name 
> of the types involved in the proof ?

I think it's an attempt to help the user quickly map a name to its type, 
mentally.