Skip to Content.
Sympa Menu

coq-club - RE: [Coq-Club] proving a lemma in a proof

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] proving a lemma in a proof


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page