The Coq mailing list

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

Dear Enrico, Pierre,

thanks for the detailed explanations! @Enrico: sorry for my bad memory - I 
had to get too much new stuff into my brains recently.

I can imagine that there are complicated cases and that in full generality it 
is indeed difficult. But I wonder if instead of trying to solve this in full 
generality, it wouldn't be a possibility to simply disallow such cases. E.g. 
the case you detailed below (hiding a library lemma by a nested lemma and 
using both in the outer lemma) I wouldn't expect to work and I don't see 
useful applications for this. I would even prefer an error, when I 
accidentally would try to do this, since the proof wouldn't work anymore if I 
move the nested lemma out.

Can't we say: "A nested lemma is only supported if it's effect is 
indistinguishable from the same lemma in front of the outer lemma"? I 
wouldn’t have a problem with defining the semantics of a nested lemma like 
this. In case the meaning of the outer proof is different with the nested 
lemma nested and with the nested lemma in front of the proof, it is an error 
(or if it has to be undefined behavior). 

Would this simplify the situation?

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