The Coq mailing list

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

Dear Enrico,

referring to the workflow Adam describes (which is the same I use): I simply 
wouldn't care if in a "batch" proof check a nested lemma would be treated as 
if it was written before the proof and in a step by step proof check as if it 
was written in place. This is what I meant with "undefined behavior". I would 
even like this, because then in a batch check the automation wouldn't spend 
time to try to solve cases it can't solve without the lemma (because it 
already has it on the first trial on all sub goals) while in single step mode 
one could see in which failing case the lemma was required. Many of the 
nested lemmas I write have so strange statements that it is hard to see why 
they are needed without seeing the failing case. So for me such a deviation 
in semantics would even be a feature because I could leave the nested lemma 
in place so that people can analyze why it was needed in single step mode 
while I can still have fast batch proof checks (failing automation usually 
takes much longer than successful automation). I frequently move nested 
lemmas in front of the outer proof with a comment "please move it after 
par:<automate> to see why this is required".

This of cause doesn't mean that the semantics should be exactly like this 
(different in batch and single step mode) - what I want to say is that I 
think the users of this feature can live with a wider variety of semantics of 
nested lemmas than you might think. And some of the thinkable sematic 
variations might be much easier to implement and even better in practice.

I can imagine that mathematicians/logicians get upset about such impure 
thoughts. But in the end nested lemmas are a hack to get work done and as 
long as it works in practice it is fine.

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
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928