The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

What's the local context? It sounds like the following, however that 
doesn't work:


Set Nested Proofs Allowed.
Lemma fo (n:nat) : Prop.
Proof.

  Lemma ba : n = n.



Gaëtan Gilbert

On 23/01/2019 08:53, Soegtrop, Michael wrote:
> Dear Maxime,
>
> if I remember right, we had a discussion on the topic during the Coq 
> Implementers Workshop in Nice last year. I think you said that the main 
> difficulty with nested proofs is that they may depend on the local context 
> (the context of the outer proof). I also use nested proofs frequently, but I 
> don't use nested proofs which depend on the local context, that is which 
> could not be moved in front of the outer lemma. Since Andrew said he usually 
> moves the proofs outside eventually, I guess he also doesn't use nested 
> lemmas which depend on the local context. Maybe Adam and other friends of 
> this feature can comment on their usage.
>
> In cases others agree to this, would it be an option to remove support for 
> nested lemmas which depend on the current context? I don't see how this would 
> be in any way more complicated than parallel proofs - essentially it should 
> be the same. Also I think removing the feature that a nested lemma can depend 
> on the outer proof's context would be even an advantage, because I would 
> think most people who use this feature use it accidentally and not willingly.
>
> 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