coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Frederic Mesnard <frederic.mesnard AT univ-reunion.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] Observing "simplification of proofs as evaluation of programs" with Coq?
Date: Wed, 27 Oct 2021 13:18:34 +0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=frederic.mesnard AT univ-reunion.fr; spf=Pass smtp.mailfrom=frederic.mesnard AT univ-reunion.fr; spf=None smtp.helo=postmaster AT mail-ua1-f48.google.com
Ironport-data: A9a23:4+lg+q3qEUFMBsYx8/bD5a1wkn2cJEfYwER7XOPLsXnJ1G9whWNRyzFLUTyHPayMMGLwKIgkO97lp0sHsZGAmtQSHQtv/xmBbVoa8JufXYzxwmTYZn7JcJWbFCqL1yivAzX5BJhcokT0+1H9bdANkVEmjfvRH+KmV7adUsxMbVYMpBkJ2UoLd9ER2dYAbeiRW2thiPuqyyHtEAfNNw1cbgr435m+RCZH55wejt+3UmsWPpintHeG/5Uc4Ql2yauZdxMUSaEMdgK2qnqq8V23wo/Z109F5tKNl7/6dggXS+eXM1TezHVRXKemj15JoSlaPqQTbqJNLxcKzW/TxZYtmL2htrToIestFqPWlegQSRhTVSRzJqtP4rPvPH6+r4mJwlDAcnzqhft0ZK0zFdJApL8tUQmi8tRBcGxXBvyZvMq9x6v+Qe1xjOw4PczzNcUevGthxHfXF54brTrrV/2fv5kHyG5l3oYWCayLP4xDOGs2eE+VO1sSLghCIYwat+KMqnnbUjR+lEixm6sS9zGLmVM1jqyF3MH9f9WLQYBIlx/dqD6WuWv+BR4eOZqUzj/tz55lvceX9QuTZW7YPOTQGj9WbFyvKqg7DRQXUR6mqKD8hBLuHd1YLEMQ92wlqq1aGImDJjXid0XQnZJGlkd0txls/ykS9QeM1O/O7hufB28CCDBbADDjnNFjXiQkjzdlgPuwbQGCc9Sppba167GVs3aoNDUTLGgEIyEeJefAy7EPv6lr5i/yoh1f/GJZQzE79fwcA9xHkcTmu4gusA==
Ironport-hdrordr: A9a23:N8vSJK/o+eC2yPsKVURuk+DbI+orL9Y04lQ7vn2ZKCYlFPBw+Pre/sjzuSWE6wr5HUtBpTniAse9qBHnhPtICOAqVN/IYOClggqVxepZnO/fKlPbakrDHy1muJuIsZIVNDQ9NzRHZA/BjzWFLw==
Ironport-phdr: A9a23:+8se+ROgWP+cQ5SB8gsl6nbLDRdPi9zP1u491JMrhvp0f7i5+Ny6ZQqDv60r1gORFtyCo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9AdgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/6u95HJfQlFiyaxbbxvIBmrsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KODE5/m/ZicJ+kbxVrw66qhNl34LZepuYOOZicq7fe94RWGpPXtxWVyxEGo6yb5EPAPQcMulGtYn9pkcBpga5CwayH+PvzCVHhmXr0qYn1OkhHxvG0xI9EN0QqnTUrcn6OL0XUe+r16nIyy/Mb+lL1jrm9YjIdBEhoe+VUbJqb8XR1E8vFwLCjlWWs4DlMSmV2/0LvmOG4OVuSfihhHQ7qwFtvDev3MEsh5HLi48R1l3K9Sd0zJspKdClVEJ2Y9CpHZtNuyyHM4Z7Xt8uTmBstSskzrALpZ62ciYUxZkmxBPSZeKKfomM7xzjUuuaPDR2hGp9db6hmxq/9VKsx+78W8WuzlpGsDRJnsPDu30O0RHY99KJReFn/ki73DaCzwDT5f9AIUAzjafbLoQuwr80lpYKrETMBDL6lFz4jKKZdUgo4Oeo6+PgYrXpop+TKZV4hR35MqQrgsC/AOI4PRYSX2WD5+iwyLnu8Vf6TbhKlPE6jLfVvI7AKckUpaO1GwpV3Zwi6xa7ATemytMYnXwfIVJLYhKIkZXmNE/UIPD5EfizmVGsnylwx/DAJLLhGIjCI2PekLfnfLZ99VdQyBAtwtBC4ZJUC7YBIPTpVk//rtzUFgU5PBCsw+b7FNV90ZsTVn6IAq+AKa/drVuI5v80LOSXf48UuDP9K+A/6PL0jH85n0Udfaiz0pcNZnC4BKcuH0LMan31x9wFDG0ivwwkTeWshkfRfyRUYiOcRa8w6ys6A8qDAJzFT5qhyOiPxiq3E4dXbSZDB0uKGG3kX5iCWulJci+PJM5mlHoKT+7yGMcayRiyuVqimPJcJe3O93hA3XoC/N185umWiBhrsDIoX4KS1GaCS2wylWQNFWdeNEVXvEp81BKZ3LV+gvteU9JJtashuugSKJjd0algBs30WwXHONmTGg/Ofw==

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