The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Le lun. 28 janv. 2019 à 10:03, Soegtrop, Michael
<michael.soegtrop AT intel.com>
 a écrit :
>
> Dear Pierre,
>
>
>
> > I think it is pointless to try to be consistent in presence of nested 
> > proofs if
>
> > everyone agrees that it cannot remain in a finished proof (like admit).
>
>
>
> I would put it slightly differently. As I explained I sometimes do keep 
> lemmas nested or at least keep my proves such that I can move the lemma 
> back for the purpose of explaining why one needs a lemma with a rather 
> bizarre statement.
>

I think I understand your use case but it seems more of a coqdoc
feature to me: link a statement to a part of a further proof and have
it displayed there for pedagogical reason.

> The point is that most people are using nested lemmas together with fancy 
> automation, and an automation system which cannot handle the semantic 
> differences which have been discussed in this thread is simply useless for 
> practical purposes. So the conclusion is the same.

AFAIU nobody has ever had an automation system that handles this for
now. People just "know what they are doing" when writing a nested
lemma: i.e. "the only problems I will get when I move this lemma
outside (hint stuff, name shadowing...) will be easy to solve". Of
course warning you for these problems earlier would be nice but complicated.


> 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