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: "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 08:57:07 +0000
  • Accept-language: de-DE, en-US
  • Authentication-results: mail2-smtp-roc.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 mga06.intel.com
  • Dlp-product: dlpe-windows
  • Dlp-reaction: no-action
  • Dlp-version: 11.0.400.15
  • Ironport-phdr: 9a23:vvDiSBekOWu9QDlhR7PHWK/9lGMj4u6mDksu8pMizoh2WeGdxcS/ZB7h7PlgxGXEQZ/co6odzbaO4+a4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahYr5+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM38H/ZhNFsjKxVoxyhqR5ww4/Ib46aO/RzZb/dcsgeSGZdQspdSy5MD4WhZIUPFeoBOuNYopHzq1UTqhuxGwasBP/1yj9Pnn/6xbAx3eMgEQ7a3AwvBcwBsHDaoN7oM6oSVOG1w7XIzTrZcfxW3S3x6JPPch8/rvGMQahwcc3JyUQ0FgPFiEmQppLhPz+PyusNtG2b4vNmWOmyhWAnrARxrSKuxscqkoTJh4QVykza+iV92oo6OMO3RUhmatCnCJtdrzyWOoV5T884Xm1ltik3xqcbtZO1fSUG0poqywPHZ/CacoWF7AjvWeifLDtimn5odrayiwyv/UWj1uHwTtS43VdOoyZfjNXBtn8A2wbN5sSdS/Zw/kGs0iuV2Q/J8OFLO0U0mLLbK5E/xr4wkYIesUHMHiDshEn7jbWadkQi+ui09evnZq/qqYObN49xkg3+M6IuldKjAekgLwQDUWeW9f6h2LDt8kD1WqhGg/M3n6XDvp3WONwXpqujDA9U1oYj5Qy/DzCj0NkAmHkHLU5KeBKdgIf3P1HCOuv4DfChjFSjjDdr3ffGPqX6D5XMKHjDjKnufbJn50FAzwozyMhT54hIBbEZPPLzRkjxucTEAR8+Kgy42vroCNFg1owFQm+PGa+YMKbKsVCS/O4vIu+MZJUUuDnnMfQl6eTu3jcFngpXdq6wmJATdXqQH/J8Ikzfb2CmyoMKFn5PtQ4jRsTrjkeDWHhdfSDhcbg742RxM4WrApvZQZjpyJmA1yeyE5kcLjRDC1uMGHrsMZ6DVvgQciWKCs5njjEAE7OmTtlyhlmVqAbmxu8/faLv8SoCuMe7jYkn16jojRg3sAdMIYGY2mCJQXtzmzpRFT4wwK1750d6zwXaiPQqs7ljDdVWoshxfEIiL5eFlr57Dcz/XkTKedLbEA/7EOXjOik4S5cK+/FLY0t5HIz93BXM1nL0Rb4Ti7GPQpcz9/CE0g==

Dear Enrico,

referring to the workflow Adam describes (which is the same I use): I simply
wouldn't care if in a "batch" proof check a nested lemma would be treated as
if it was written before the proof and in a step by step proof check as if it
was written in place. This is what I meant with "undefined behavior". I would
even like this, because then in a batch check the automation wouldn't spend
time to try to solve cases it can't solve without the lemma (because it
already has it on the first trial on all sub goals) while in single step mode
one could see in which failing case the lemma was required. Many of the
nested lemmas I write have so strange statements that it is hard to see why
they are needed without seeing the failing case. So for me such a deviation
in semantics would even be a feature because I could leave the nested lemma
in place so that people can analyze why it was needed in single step mode
while I can still have fast batch proof checks (failing automation usually
takes much longer than successful automation). I frequently move nested
lemmas in front of the outer proof with a comment "please move it after
par:<automate> to see why this is required".

This of cause doesn't mean that the semantics should be exactly like this
(different in batch and single step mode) - what I want to say is that I
think the users of this feature can live with a wider variety of semantics of
nested lemmas than you might think. And some of the thinkable sematic
variations might be much easier to implement and even better in practice.

I can imagine that mathematicians/logicians get upset about such impure
thoughts. But in the end nested lemmas are a hack to get work done and as
long as it works in practice it is fine.

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