Skip to Content.
Sympa Menu

coq-club - [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?


Chronological Thread 
  • From: Pierre Courtieu <pierre.courtieu AT gmail.com>
  • To: "coq-club AT inria.fr" <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?
  • Date: Mon, 3 Aug 2015 21:56:36 +0200

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



Archive powered by MHonArc 2.6.18.

Top of Page