coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?
Chronological Thread
- From: Adam Chlipala <adamc AT csail.mit.edu>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?
- Date: Mon, 03 Aug 2015 14:23:41 -0400
On 08/03/2015 12:38 PM, Cedric Auger wrote: 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". I'd like to second the request for keeping nested lemmas. The big difference vs. [assert] is that nested lemmas may be used in parts of the proof script that are not in the binding scope of the point where you put the lemma proof. The overwhelming motivation (for me) is to avoid wasting time rerunning the part of the current proof script, up to the point where you realize the lemma is called for. I expect that the Coq team doesn't generally plan in terms of supporting cases where single lines of Ltac run for minutes or hours, but those cases are important to me and probably others, too. [assert] avoids those problems but then limits the scope where the new lemma can be referenced. Also, adding the lemma in the current context can cause undesirable perturbations in Ltac automation. If the lemma statement is long, there can be a substantial performance cost. |
- [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?, 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.