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?)
Best
Pierre
- [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?, Soegtrop, Michael, 08/03/2015
- Re: [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?, Cedric Auger, 08/03/2015
- Re: [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?, Adam Chlipala, 08/03/2015
- RE: [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?, Nick Benton, 08/03/2015
- [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?, Pierre Courtieu, 08/03/2015
- RE: [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?, Soegtrop, Michael, 08/04/2015
- Re: [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?, Cedric Auger, 08/04/2015
- Re: [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?, Per Lindgren, 08/04/2015
- RE: [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?, Soegtrop, Michael, 08/04/2015
- Re: [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?, Pierre Courtieu, 08/04/2015
- RE: [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?, Soegtrop, Michael, 08/04/2015
- Re: [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?, Per Lindgren, 08/04/2015
- Re: [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?, Cedric Auger, 08/04/2015
- Re: [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?, Per Lindgren, 08/04/2015
- Re: [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?, Cedric Auger, 08/04/2015
- RE: [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?, Soegtrop, Michael, 08/04/2015
- Re: [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?, Adam Chlipala, 08/03/2015
- Re: [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?, Cedric Auger, 08/03/2015
Archive powered by MHonArc 2.6.18.