The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2015-08-03 17:14 GMT+02:00 Soegtrop, Michael <michael.soegtrop AT intel.com>:

Dear Coq Users and Team,

recent versions of Coq give this message when proofs are nested (a new Lemma is started inside of a proof)

"Nested proofs are deprecated and will stop working in the next Coq version"

I would like to have a discussion on this because I use this regularly. I like a heavily automated proof style and when automation gets stuck, I tend to solve this by providing some additional idea in a new lemma and add this to the hint database. It makes sense to do this inline/nested for 2 reasons:

- it is quicker (at least during proof development) in case the automation did laboriously crunch through a few 100 cases successfully and left over only 1 or 2.

​You can still use the "assert" tactic, almost exactly the same way you use "Lemma".​

 

- It documents why you are proving this lemma, which sometimes states something which is fairly unmotivated without looking at the proof state at this point.

​That does not document that much. If you are not running Coq interactively, you only see a lemma in the middle of a Coq script.

If you run it interactively, you may still not see why the lemma is needed, if your previous tactic did some black magic to make that goal appear.​

In the cases where "Lemma" documents your proof, "assert" is likely to also document it.

 

 What do others think about this feature?

​I never felt the need of it. Furthermore, if this mechanism works like I think it works, it can be a "not so nice" feature.

I guess it works the following way: all your current hypotheses are exported, even unneeded ones into a new lemma which can be called later even once your proof is finished.

I mean, if you have the following context:

x:nat

y:nat

H:P x

z:nat

Inf1:x<y

Inf2:y<=z
==========

Q z

and you want "x<z" as auxiliary goal, will "Lemma trans : x<z." export a new term at top-level with following signature:

"∀ x y, P x → ∀ z, x<y → y≤z → x<z"?

If so, the "P x" argument is totally useless, and, from my point of view, should be pruned before starting the nested lemma, but you may need it later in the "P x → x<z → Q z" part. Thus, you may need to first do something like: "assert (x<z); [clear H|].".

If this is the intended behaviour, then it works like the "abstract" tactic. It is a nice feature, but you should consider cleaning your context before using it, otherwise, you may end with unusable exported lemmas and needlessly unreadable big terms.

 

What are the reasons for dropping it?

​Probably because maintaining it is not that funny, and not enough people seem to use this feature to be worth maintaining it.​

 

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