The Coq mailing list

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

Hi

Well, the advantage (to my understanding) of nested proofs is mainly the development process, not needing to step back (outside the proof), state the lemma (out of context, e.g., you do no longer see the goals, and other terms). In my limited experience, I have usually copied the context, pasted in as a comment so you see what you are dealing with, formulated/proved the “help” lemma (above the proof). And then gone back to the main part (using the help lemma). In that way, the lemma is explicilty in the environment of the whole proof (inlcluding the <part 1>). I guess the issue would be automatic/implicit lifting of inner lemmas, would in cases imply some unexpected side effects (to <part 1> and the like..).

Makes sense?

/Per

On 04 Aug 2015, at 16:04, Cedric Auger <sedrikov AT gmail.com> wrote:

If so, I was wrong about how nested lemma work (I did not tried it). And almost all what I wrote could be forgotten.

I simply guessed that the mechanism was similar to what occurs with the "abstract" tactic.

But well, in that case, I could not find really relevant arguments to remove this feature (but even less to keep it, in fact, beside retrocompatibility).

Thus I will only state that it needlessly (from my point of view) complicates the syntax, and I find it simpler to keep the "Lemma L1 : … Qed. Lemma L2 : … Qed …" form, rather than having well parenthesized "Dyck" lemmas.

In my experience of Coq, I never needed that feature.

2015-08-04 15:39 GMT+02:00 Soegtrop, Michael <michael.soegtrop AT intel.com>:

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