The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Pierre,

 

the reason I am using nested lemmas instead of assert is that I want to add them to a hint database. I don’t think this works with assert. There are several reasons for using hint databases:

 

-          I might have several remaining goals which might profit from the new lemma. An assert is limited to the current goal.

-          It might be very tedious to use the new lemma without the proof automation system.

 

If I want to do this without nested lemmas, I can only go back and start the proof from scratch.

 

The documentation argument can of cause be discussed. I still think this style gives the motivation for a lemma, but I wouldn’t call it justification. Quite a few of the lemmas I create this way are useful in other contexts as well, but it is sometimes quite hard to explain in which situation this lemma is useful. If someone is interested, he can still go to the specific point in the proof and see why the lemma is useful at least in this specific case. This usually gives good hints on why it might be useful in other cases as well. For the not so curious reader of a proof, her does still see that this lemma was required to get through this proof without additional documentation.

 

I think it is an interesting question if somebody uses the current proof context in the new lemma as you described. I actually never did this. The lemmas I proof nested are independent lemmas and could be stated at the top level in the same way. Otherwise it wouldn’t make sense to add them to a hint database. So would it simplify things if we restrict nested lemmas such that they may not depend in any way on the current proof context? I think if I would like to have a lemma only useful in the current context, I rather would use assert as you suggest.

 

Best regards,

 

Michael

 

 

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

 

Hi, my two cents:

 

IMHO there is a contradiction between the "documentation" argument and the need of having nested lemma visible outside their scope. If you consider a lemma is only justified by the current state of the outer proof then it has no reason to be visible outside, and you should use assert. If your lemma is useful outside the current proof then it should not stay nested except temporarily for efficiency reason and it should be documented on its own. The same probably applies to Adam's remark on the bad side effects of moving a lemma from the nested position to the outside position. If your nested lemma is used elsewhere then the side effect is likely to appear later anyway. Better play with hint stuff inside lemmas then (btw is it possible to add a hypothesis to hints?)

 

I think that having a strict document structure is important. For scalability, tooling, documenting etc. nested lemmas as they are currently implemented is a serious hole in this structure. That said I use them very frequently but always as a temporary state when it would take too much time right now to rerun the current proof. I also hope that this use will remain possible.

 

Best

Pierre

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