coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] That time we proved False in Coq

From: Abhishek Anand <aa755 AT pm.me>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] That time we proved False in Coq
Date: Wed, 29 Dec 2021 02:43:41 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=aa755 AT pm.me; spf=Pass smtp.mailfrom=aa755 AT pm.me; spf=Pass smtp.helo=postmaster AT mail-4316.protonmail.ch
Ironport-data: A9a23:velgt6yTmehYDSk74YR6t+drxyrEfRIJ4+MujC/XYbTApDonhDdTyTBND2iDb/bZYWTwetEgOo3g8B8DsJHXzYBrOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA/3z27AsFehsJpPnjkrrYuiJQUVUj/nSH+OmUr+cY0ideCc9IMsfoUI78wIGqtUw6TSJK1vlVeLa+6UzCnf9s9JHGj58B5a4lf9alK+aVAX0EbAJTasjUFf2zxH5BX+ETE27ByOQroJ8RoZWSwtfpYxV8F81/z91Yj+kurPyc0lPHuWLY06WkH1KXK6nixlG4Ccyuko5HKNMNAEI03PVxJYolr2htrToIestFqTFx7lAewFdVSRzVUFD0OadcSbn7pfOp6HBWyC0kqg/XBFe0Zcj0u1wGCRF8eESACscawiKweOw2rOyDOd27vnPhuH/ZNZE/Cx0lGSBS64yG8WbBf+Xu4FMh2JowJ1aQqP3eewybBxDbDDhajtzIHEDUcprxKPwkhETaBVdoVOR4PZsujaV1BZ2zL/rNdPUfpqBRa1oco+jjjqu1wzE7tsybbRzCAZp805AQsfKlCL/Hd5JTeP+7uRtnFqVw2USDFsdVTNXZNGn31WmVYs3x1M8o0ITQWoarSRHjeURmzWgpTiBs3bwnvJORvYi5ljlJrX8um6k66ttctKFQMQj8so7LdDv/jdlgPuxbQFSXHappb5xO1taQf5e+cTYEIPaWRI5cA==
Ironport-hdrordr: A9a23:X5FT6a4JYkJPDSYiMwPXwL3XdLJyesId70hD6qkfc3Bom6Cj+vxG4s506facsl94M03I8uruBEDvexnhyaI=
Ironport-phdr: A9a23:A+D8kRejLrhDaZa0s38ng15ElGM+q97LVj580XLHo4xHfqnrxZn+JkuXvawr0AWQG9yBs7kY2qL/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHNfglEniexba1uIBm5ogjcstQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/ZlMJ+jLhbrg+iqRN9zY7bb52aOeFkca/BZ94XX3ZNUtpTWiFHH4iyb5EPD+0EPetAs4TyvFsOrRqlBQmsGuzvySJDi2Pw3aIg1eQuDBzN0Qs6EN0UsnnZrNX4ObwKUeCw1qXIyCvMYupQ1Dzg54fGbgovruuQXbJsb8XR008vGhvKgFiQq4HoIS2Y2+YRvmSH4OdtVO2ihnM5pw1trDWi28chhpTHi4waxV3J6Dh1zoYoKNC2VEN2bsKoHZRMuyyZMYZ9X80sQ2ZtuCkgy70Gv4a2fCcLyJQ7xx7fdueIf5KU7RLkUeacJypzinF9eL+nmhq/8kitxvf+W8WoylpHoSRInsPRun0M0RHY99KJReFn/ki73DaCzwDT5f9AIUAzjafbLoQuwr80lpYKvknOEDL6lUTsgK+ObEUk/fSo6+PhYrXjvJCcNot0hhviPaQugsC/AOI4PRYSX2WD5Oix173u8Vf7TblWlPE7nafUvIrHKckavqK5BhVa0ocn6xaxFTem19EYkGEdI11feh+Kj4jkNkrWIPD9F/u/hkqjnC9xx//aJr3hHonNLn/bnbj9erZ98ldQxxY3zdBC/J1ZEaoBIfL2Wk/prtPUFB45Mwquw+bmEtpxzI0eWXjcSpOeZajVqBqD4v8lC+iKfo4c/jjneMIo//r/sXhssFUdfLKp0JhfQXaxGPgud0yQPiexqs8EV2IH6FkQVuvv3XSIUT9IZ3uxF4s67zc3QNavBNieG6i1hfqE0XHoTdVtemlaBwXUQj/TfIKeVqJUAMp3Ctdk1DkJB+DJo24J0BivsEqmkOM5aPLO/TEfs5fq1dwz7O2BzHnaGhRsCoKY3jPUJ1w=

I have a small side question regarding the wiki article. It contains a sentence:

> As a result, not all the legitimate functions that satisfy the current (unsound) guardedness checker will satisfy the new sized type based typechecker.
My impression was that all the actual soundness holes in the guardedness checker were patched, so what unsoundness remains in the checker in recent versions of Coq? Would a hypothetical proof of consistency of the entire Coq kernel as it currently exists be possible in principle, or do we know that this is false without avoiding certain areas?

Yes, as far as I know, the guardedness checker was patched. I fixed the article: https://github.com/coq/coq/wiki/CoqTerminationDiscussion/_compare/8f9576e00875b77614eae47dbd5cbbbc86c7adfd...fd05a250486919dc8035174017acf65667f66967

Mario Carneiro

On Tue, Dec 28, 2021 at 3:34 PM public <aa755 AT pm.me> wrote:
I wrote a wiki article about the last such incident I remember.
https://github.com/coq/coq/wiki/CoqTerminationDiscussion
(others have since contributed to the article)

Regards,
Abhishek Anand

‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐

On Tuesday, December 28th, 2021 at 3:19 PM, Marco Servetto <marco.servetto AT gmail.com> wrote:

> Hi,
>
> I'm writing a little document talking about soundness/unsoundesses in
>
> verification systems.
>
> I remember that there was a time we managed to prove False in Coq, and
>
> the community came together effectively and promptly to fix it, and
>
> all major proofs were unaffected by the fix. I also remember members
>
> from other communities (Agda?) coming to give a hand.
>
> While I'm not a Coq genius, seeing the honesty and the clear polite
>
> and direct action made by this community filled me up with hope for
>
> the
>
> future.
>
> Do I remember correctly? Can someone help me to summarise the event
>
> and provide some references? Do you have references to other important
>
> tools that have been proved unsound and any discussions about the
>
> response of their community?
>
> Marco.

[Coq-Club] That time we proved False in Coq, Marco Servetto, 12/28/2021
- Re: [Coq-Club] That time we proved False in Coq, public, 12/28/2021
  - Re: [Coq-Club] That time we proved False in Coq, Mario Carneiro, 12/29/2021
    - Re: [Coq-Club] That time we proved False in Coq, Abhishek Anand, 12/29/2021
      - Re: [Coq-Club] That time we proved False in Coq, Jason Gross, 12/29/2021
        
        Re: [Coq-Club] That time we proved False in Coq, Mario Carneiro, 12/29/2021
        
        Re: [Coq-Club] That time we proved False in Coq, roux cody, 12/29/2021
        
        Re: [Coq-Club] That time we proved False in Coq, Jason Gross, 12/29/2021
        
        Re: [Coq-Club] That time we proved False in Coq, Yannick Forster, 12/30/2021
        
        Re: [Coq-Club] That time we proved False in Coq, Pierre-Marie Pédrot, 12/31/2021