coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Observing "simplification of proofs as evaluation of programs" with Coq?

From: Dominik Kirst <kirst AT cs.uni-saarland.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Observing "simplification of proofs as evaluation of programs" with Coq?
Date: Wed, 27 Oct 2021 11:29:42 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=kirst AT cs.uni-saarland.de; spf=Pass smtp.mailfrom=kirst AT cs.uni-saarland.de; spf=None smtp.helo=postmaster AT triton.rz.uni-saarland.de
Ironport-hdrordr: A9a23:CsG1wauvSA8POoYOTDg9eLgr7skDQ9V00zEX/kB9WHVpm62j5riTdZEgviMc5wx/ZJhRo7q90da7MBXhHPJOjLX5RI3SOTUO21HJEGgB1/qB/9S6IVybygc1784JT0EZMrzN5DNB4foSjjPXLz4Cq+P3l5xBx4/lvhRQpKpRGthd0zs=
Ironport-phdr: A9a23:2/qZKB8KuBw4o/9uWeG8ngc9DxPPW53KNwIYoqAql6hJOvz6uci4ZAqOvL4w0xfgZsby07p8ke3YsqTtCyQrwK2qlzQ8SqFKTAIPks4MngYtU4avAEz/K+P2PWRhRJwRHFBq8GumPkdLBc3we0PdomGo7T4VBx7zKRd5Kv76F4LMk8i7zeS/94DcbwhIhje2fK9/IgixoQjNrMcdnJFsKrw2yhvHo3tIf/pZyGZ1Ll+NnBjy+9m98od7/ytfp/wu+chAUb7nf6sjVrxXEC4mM2Eu68L1sxTIUBaC6WEdUmUSlRpIHhTF4RTnVZr/rif2quxw0zScMMbrT747RC6i4r9rRhD0hykIOCM3/m/ZisJujq1VoxWvqgdjw47NZYGZKPp+cr/Dcd4cWGFPXtxRVytEAo6kYYUPCO8BPeder4n8pFsFsB6wBQi2BOP01j9Dm3j73a470+Q7CgHGwBctEM4VsHjOsdX1MqYSXfmuzKbS1zrDdfdW1i376IfVaBwuvO+DUKt2fMHMxkYhCxnLgU+MqYz5ITyVzOINvnCb4udhSO+ilW8qpQ9+rDWsyckglI3Eip8Wx17E9Ch3zpg5KMO3RUB0ZdOoDZRdui6HO4Z0Xs8uX3xktiY6xLAEv5OwYSsEyIw/yhLCZfGKfJKE7xbiWeqLIzp0nmxpdbKnixqv/0WtxffwW8213VpQsyZIkdjBumoQ2xHR7MWMV+Fz8V272TmV0gDe8uFELl4wlarcM5Mh3qQwlpsPsUTEGC/6gl/2ja6MekU5/Oio6v3rYq78qZCGLY90jhvxMqIzlcClHOs3LBACX2md+euiyL3u5VD1TbtFg/EslqTUsYrWKMYBqqKnAwJZyoMj5Ay+Dzei3tQYh34HLFdddRKEjojpIUrOIOzjAPijmFSgiiprx/bHPrH4GZXCNGLMkK3lfbln7U5T1RA/ws1B6J5MELEOPOrzWlPttNzfFhI2Lwu0w//+BNph0oMeRHmAD7SCMKLStF+I/vggL/ONZI8Tojb9KuIq6+TgjX8jyhchevyi2oJSY3SlFNxnJV+YaDzimIQvC2AP6yY5Se3siV7Kcj9JfGr6C6E9/ConIIm9S5rFR8W2ibWb2C69EttaazYVWRi3DX70etDcCL83YyWIL5o5+tThfbO6DZIn1FS1vQbgz7NhIqzY939A3XoM/NNuofDVlFQp/DVuC82b3yeBQjMt9ovpbyMs3bx4pwpn2BGe16k9mPVRD9ha4f8PXgpobfbh

Hi Fred,

you can prove the proposition True either directly with its constructor I, or
by first proving True -> True with the identity function and then applying it
to I. The latter program (fun x => x) I evaluates to I, which represents the
most simplified proof of True without any intermediate steps. I guess this is
the correspondence Philip Wadler is referring to.

Best wishes,
Dominik

> On 27. Oct 2021, at 11:18, Frederic Mesnard
> <frederic.mesnard AT univ-reunion.fr> wrote:
>
> Hi all,
>
> I am reading the CACM paper "Propositions as Types" written by Philip
> Wadler.
> With Coq, I can easily observe "propositions as types" and "proofs as
> programs".
> Can I also observe "simplification of proofs as evaluation of programs"
> within Coq?
> Where can I find examples?
>
> Thanks in advance!
> Fred

[Coq-Club] Observing "simplification of proofs as evaluation of programs" with Coq?, Frederic Mesnard, 10/27/2021
- Re: [Coq-Club] Observing "simplification of proofs as evaluation of programs" with Coq?, Dominik Kirst, 10/27/2021
- Re: [Coq-Club] Observing "simplification of proofs as evaluation of programs" with Coq?, Jean-Francois Monin, 10/27/2021