The Coq mailing list

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

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