coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Qed opacity and Coq standard library

From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
To: coq-club AT inria.fr, Jerome Hugues <jhugues AT andrew.cmu.edu>
Subject: Re: [Coq-Club] Qed opacity and Coq standard library
Date: Wed, 21 Apr 2021 15:58:07 +0200
Ironport-hdrordr: A9a23:GERjFa0sEkcBhSqxGIR4QQqjBTlyeYIsi2QD101hICF9WMbwrbHMoN0w0xjohDENHEw6kdebN6WaBV/a/5h54Y4eVI3SJDXOkm2uMY1k8M/e0yTtcheOj9J1+IVBV+xFCNP2BUVnlsqS2mKFOvsp3dXvys+VrMjEyXMFd29XQoFmqzx0EwOKVnBxLTM2YKYRMZqH+45uvDCgeWsaB/7LeEUteujYupnqufvdEGE7Ljsm8hTLtDWz9dfBYmml9zIfSS4K/bA57WPemRf47anLiYDK9jb523XI55pb3PvNo+EzZvCkrsgQJnHShh2zZIJnMofy2gwdmfqi4lomnN7Hr34bTr9OwkjcdG20vhfhsjOIuFxCh0PK8lOWjWDupsb0XlsBeq58rLlUax7Ir3cn1esc7Itww2mbu5BLZCmw+xjV2t6gbXFXv3vxiWY+l6opg2ZHV4wFZPtqsZUH509OCv47bVHHwbFiPO5yDNzNoNZ6GGnqG0zxjy1AwMGMQn92JRuPWE4E0/blrwR+rTRWz1Y42MdapXsL9Is8R55Yjt60T5hApfVhTtI2cak4P+sKQdK2BmvRBTrAPXmfO06PLtB0B1v977D2/ZQo76WRdJsEwIBaouW6bHpo8VQdP27PJKS1reh2ziw=

Hi,

On 20/04/2021 15:48, Jerome Hugues wrote:
> Is there some suggested readings on this topic?

I am afraid I don't have anything specific to propose you to read on
this, but I believe that the recent introduction of the sort of strict
proposition SProp in the Coq type theory could relieve some of the
problems arising from Qed-terminated proofs.

It's still quite hard to use due to buggy tactics / pretyper, and it
will never help you for termination proofs either, but it might be worth
having a look at it.

PMP

Attachment: OpenPGP_signature
Description: OpenPGP digital signature

[Coq-Club] Qed opacity and Coq standard library, Jerome Hugues, 04/20/2021
- Re: [Coq-Club] Qed opacity and Coq standard library, Jean-Christophe Léchenet, 04/21/2021
  - Re: [Coq-Club] Qed opacity and Coq standard library, Jerome Hugues, 04/21/2021
    - Re: [Coq-Club] Qed opacity and Coq standard library, Fabian Kunze, 04/23/2021
- Re: [Coq-Club] Qed opacity and Coq standard library, Pierre-Marie Pédrot, 04/21/2021
- Re: [Coq-Club] Qed opacity and Coq standard library, Xavier Leroy, 04/21/2021
  - Re: [Coq-Club] Qed opacity and Coq standard library, Jerome Hugues, 04/23/2021
    - Re: [Coq-Club] Qed opacity and Coq standard library, Pierre Courtieu, 04/23/2021