The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq Team and Users,

the reason why I sometimes keep nested lemmas where they are is that with 
proof automation it is not possible to get to the state where the lemma is 
used otherwise. When the lemma is there, the automation will use it and 
finish the goal. The only way to get to the point where one can see why the 
lemma is required is to remove it. Then the automation will leave the 
interesting cases for inspection. It is sometimes really difficult to explain 
why a lemma is required without seeing the proof context. Of cause I could 
copy the context to a comment to motivate the intermediate lemma. Or I could 
write a comment "please delete this lemma, run the proof below and you will 
see why you want it back".  I think in such cases one may argue that it is 
not bad style, but a reasonable help for others, to keep the lemma where it 
is, so that proof automation will stop there, one can look at the case(s) and 
then proof automation continues happily with the new lemma. There are cases 
where the lemma is useful in similar cases outside of the proof, so using 
local hypothesis in hint databases is not an option.

When I look at Coq developments, I frequently find fairly unmotivated rather 
obscure lemmas without a single line of comment on why they are there. Maybe 
mathematicians (I am physicist) are better trained to see through such 
things, but I would think if we want to make Coq accessible to a broader 
audience, we need to accept that some things are a bit harder to understand 
for others, and that ways which make it easier to see through what is going 
on are important. I use nested lemmas rarely for this purpose, but sometimes 
I do.

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Prof. Dr. Hermann Eul
Chairperson of the Supervisory Board: Tiffany Doon Silva
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928