The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

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