The Coq mailing list

[Per Lindgren <per.lindgren AT ltu.se>]

Hi

The issue here is not the nested proof by itself, but rather the lifting inner proofs to be available to <part 1>, and thus changing its behavior? Or am I missing something (being a newbie)…

  Per

On 04 Aug 2015, at 15:39, Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

Dear Pierre, Cedric,

 

then I don’t understand what the problem with supporting nested lemmas is.

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Pierre Courtieu
Sent: Tuesday, August 04, 2015 3:16 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?

 

Nested lemmas are started in a fresh environment. Context dependent nested lemmas are not possible afaik.

 

Lemma A: TA.

Proof.

<part 1>

  Lemma B: TB.

   Proof.

   <part 2>

   Qed.

 <part 3>. 

Qed.

 

There is no reference to the  proof context of A in the statement and proof of B. Once proved B is added to the global environment just as if it was proved before A. The only difference is that the <part 1> Is evaluated before B exists (hence if B Is moved outside of A <part 1> may behave differently especially if B Is added to some hint db).

 

Pierre

 

 

Le mardi 4 août 2015, Soegtrop, Michael <michael.soegtrop AT intel.com> a écrit :

Dear Cedric,

 

I checked some of the lemmas I created as nested lemmas. None of them depends on the proof context explicitly and none of them gets any implicit context dependency added by Coq. When I “Check” the lemmas, they look as expected: no dependency on hypothesis in the proof context of when the lemma was started.

 

So how about disallowing context dependent nested lemmas? Of cause I need dependency on section variables, but not on the current proof context. As far as I understood, the others, who expressed interest in this feature, use it in a similar way.

 

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