coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: RE: [Coq-Club] proving a lemma in a proof
- Date: Fri, 25 Jan 2019 14:09:44 +0000
- Accept-language: de-DE, en-US
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga04.intel.com
- Dlp-product: dlpe-windows
- Dlp-reaction: no-action
- Dlp-version: 11.0.400.15
- Ironport-phdr: 9a23:r0nJux+uefFWhf9uRHKM819IXTAuvvDOBiVQ1KB31+wcTK2v8tzYMVDF4r011RmVBdWds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+557ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/2hikaKz43/mLZisJyg6JavB2uqBNxzpXIYI6OMPdyYr/Rcc8YSGdHQ81fVzZBAoS5b4YXAeYPIOFYoJfyp1sStxu+AhGsCPvywTFPh3/5wa063P4/HgHC0gArAtUDsHHVrNrpNKcdS/66zK3SwTXYaPNZxzj96JTSchAmufGBRrNwcczNyUYxEwPJlEmfqYvgPz6M0OkGrmaV7+1lVe21im4nrRl8ojmpxscwlIbJgpgZxU3a+ih/3Y07JsW4RVZmbdOgDpdcrSGXOotsTs4iXW1kojs2xqMatZKjYSQHyZoqywTRZvGJaYSE/BzuWeKLLTtlh39pZKqziwuz/EWk0OHwSMm53VlQoiZbiNXBt3AA2hrO4cadUPR95F2u2TOX2gDT9O5EJUc0mLLeK54u2LE8ipUevV7CHi/whEX5kquWel849eiv7uTrerTmppmCOI9okgzyL6AjltKlDek4MgUCRWiW9fqm2LH+40H1XK1GjvgsnanYtJDaK94bpqm8AwJN14Yj6gqwDze839sGmXkLNklFeBWZgIjmJ1HOOvf4De+kjlStljdr2+7JPrn7DprRKXjDla/tfaxh5E5E1Aoz0ddf6opIBbEGOfL/Q1P+tNjFDhAiKAG02ObmCNBl1owEQ26PA6mZMLnTsVCS/O4vLfOMN8cpv2O3IP88ovXqkHURmFkHfKDv04FdICSzGe0jKEGEa1LthM0AGCEEpFxtYvbtjQjIajleaGqoWLp4rhQ6A4KvAIOJDtSogbeB1Sq/WIZRa29aEFeUOXbua4iAHfwLbXTBcYdajjUYWO35GMca3ha0uVqikus1Hq/v4iQd8Knb+p1w7uzXmws18GUtXcWbz2yJCWpzmzFRHmNk7OVEuUV4j2y7/+1gmfUBTI5S4e9EVkExMpuOl7UnWeC3YRrIe5KycHjjQtiiBmhuHNc+yodSJUd7B9imyBvE2njyDg==
Dear Adam,
> That effect is harder to support with hint commands, which at least in my
> uses
> often follow nested lemmas.
Indeed for hints it is trickier, since it does make sense to modify a hint
database in the middle of a proof, e.g. add and later remove some expensive
hint. So I would say for nested lemmas one should be able to define in the
Hint statement if the Hint shall be implicitly moved out in batch proofs with
the nested Lemma or stay in the middle of the proof.
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
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928
- Re: [Coq-Club] proving a lemma in a proof, (continued)
- Re: [Coq-Club] proving a lemma in a proof, Gaëtan Gilbert, 01/23/2019
- RE: [Coq-Club] proving a lemma in a proof, Soegtrop, Michael, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Enrico Tassi, 01/24/2019
- Re: [Coq-Club] proving a lemma in a proof, Jan Bessai, 01/24/2019
- Re: [Coq-Club] proving a lemma in a proof, Enrico Tassi, 01/25/2019
- Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/24/2019
- RE: [Coq-Club] proving a lemma in a proof, Soegtrop, Michael, 01/25/2019
- RE: [Coq-Club] proving a lemma in a proof, Soegtrop, Michael, 01/25/2019
- Re: [Coq-Club] proving a lemma in a proof, Enrico Tassi, 01/25/2019
- RE: [Coq-Club] proving a lemma in a proof, Soegtrop, Michael, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/25/2019
- RE: [Coq-Club] proving a lemma in a proof, Soegtrop, Michael, 01/25/2019
- Re: [Coq-Club] proving a lemma in a proof, Pierre Courtieu, 01/26/2019
- RE: [Coq-Club] proving a lemma in a proof, Soegtrop, Michael, 01/28/2019
- Re: [Coq-Club] proving a lemma in a proof, Pierre Courtieu, 01/28/2019
- Re: [Coq-Club] proving a lemma in a proof, Gaëtan Gilbert, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Christian Doczkal, 01/23/2019
- RE: [Coq-Club] proving a lemma in a proof, Soegtrop, Michael, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Jan Bessai, 01/22/2019
Archive powered by MHonArc 2.6.18.