coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
- To: James McKinna <james.mckinna AT ed.ac.uk>
- Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: RE: [Coq-Club] proving a lemma in a proof
- Date: Wed, 23 Jan 2019 10:09:30 +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 mga09.intel.com
- Dlp-product: dlpe-windows
- Dlp-reaction: no-action
- Dlp-version: 11.0.400.15
- Ironport-phdr: 9a23:F2MCwxw8ha10n8DXCy+O+j09IxM/srCxBDY+r6Qd2+MWIJqq85mqBkHD//Il1AaPAd2Lraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HQbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDtU7s6RSqt4LtqSB/wiScIKTg58H3MisdtiK5XuQ+tqwBjz4LRZoyeKfhwcb7Hfd4CRWRPQNtfVzBPDI2/YYsADesBMvpXoIfyvFYOsQCxCA2wCO/z1jNFhHn71rA63eQ7FgHG2RQtE9wTvnTTstr1O7sSUfqyzKnQ1TnIcvRY2Tbh54jIaB8uv/WMUbxtesfWzEkvFh/KjlWKpoP7OzOZzP8Ns2+F4OpvSeKvkWknqxlqrziuwMcslpfGhoYPxl/Y8iV5xZ84KNulQ0B1Zt6kFYFftyCcN4ZuQ8MiRX1otzg+yrEcpJG0Yi4Hw4kkyR7Hc/GLboaF7x35WOqMLzp1i2hpdK+xihuz60Ss1OLxWtGp3FtLoCdJiNfBu34X2xDN5MWKTuFx8lqi1DqSzwzf9+BJLEQumabFK5MszaQ8moQJvUnCHiL7nlj9grWMeUU+4Oeo7vzqYrX4qZ+YMI95kgT+Mqs0lcCjBek0KAkOX26H+eui0L3v51H2QLJPjvEuk6nZto7VJdgDq6KkDQJY3Zwv5wuxAjqpytgUgHcKIVNfdB6ZgIXlI1TOL+r5Dfe7jVSsijBrx/XeM73kA5XCMnjDn63/crZ58UJc0w0zws5Q55JIELEBJ+rzV1TwtNzeEh82LQi0z/z7B9V604MSQXiPDbOBMKPOrV+I4foiLPWLZI8MoTryN/wl5+P1gnIigl8cfayp3YMNZ3yiH/RmJV+ZYXv2jdsbH2cKpFl2cOu/qlSHXCUbQn2RXqQ673lvCoujAJyFQ4uugbqH1Q+2EttfbSZbCQbfP23vctDOYPABZz6IJdcl2hkFXrioRotrnUWrtQT6wrdjaPHT9yIEr5X7/Nlz++DX0xo18GonXIymz2iRQjQszSszTDgs0fU6+BQlkwbR4e1Dm/VdUOdrybZMWwY+O4TbyrUjWdH0Rg/FONyOTQT/G4n0MXQKVts0huQ2TQNlAdz710LC2TanB/kekLnZXMVpoJKZ5GD4IoNG81iD1KQliAB5EM5APDX3wK956wXXQYXOlhfBmg==
Dear James,
I must admit that I have only very rudimentary knowledge of Haskell and Agda
(I know this is a mistake for both, but I can't help it right now), so I fear
I can understand at most half of your answer. But I want to point out that my
proposal was to *remove* possible dependencies of nested proofs, not to add
them.
I use nested proofs mostly in cases where automated proofs fail for a
specific subcase and need some additional human insight, which I then
formulate as nested proof. To me the communication with proof automation is
very similar to the communication between humans discussing a proof. I give a
proof sketch and let the automation fill in the details. Sometimes the
automations "says" "yes I see it", like a human would. Sometimes it says
"hmm, I agree on everything except this case", and then I explain some
additional aspect like in the discussion with a human. I usually can't do
this with assert, because I need to add the lemma to some hint database or
other proof automation system so that automation can find it. Usually the
lemma does not solve the goal immediately, it just helps the automation is
some way to solve it.
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, Théo Zimmermann, 01/22/2019
- Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/22/2019
- Re: [Coq-Club] proving a lemma in a proof, Andrew Appel, 01/22/2019
- Re: [Coq-Club] proving a lemma in a proof, Maxime Dénès, 01/22/2019
- Re: [Coq-Club] proving a lemma in a proof, Jim Fehrle, 01/22/2019
- RE: [Coq-Club] proving a lemma in a proof, Soegtrop, Michael, 01/23/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, Soegtrop, Michael, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, James McKinna, 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, Gaëtan Gilbert, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Jeremy Dawson, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/22/2019
- Re: [Coq-Club] proving a lemma in a proof, Laurent Thery, 01/22/2019
- Re: [Coq-Club] proving a lemma in a proof, Jan Bessai, 01/22/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, Pierre Courtieu, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Maxime Dénès, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Ralf Jung, 01/24/2019
- Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Maxime Dénès, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Pierre Courtieu, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Théo Zimmermann, 01/22/2019
Archive powered by MHonArc 2.6.18.