coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jerome Hugues <jhugues AT andrew.cmu.edu>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] Qed opacity and Coq standard library
- Date: Tue, 20 Apr 2021 13:48:30 +0000
- Accept-language: en-US
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jhugues AT andrew.cmu.edu; spf=Pass smtp.mailfrom=jhugues AT andrew.cmu.edu; spf=None smtp.helo=postmaster AT relay-exchange.andrew.cmu.edu
- Ironport-hdrordr: A9a23:2Ui4Z6spwjhyNmJGVY2scPVR7skCtYQji2hD6mlwRA09T+Wxncqjhele8BfyhioYVn1Io6HmBICraxrnmqJdy48XILukQU3CsGynMIlt4eLZslvdMgf58fNQ0rolTrN3D8f+AUM/ocHx5gS5FNhI+qjwzImDg+DCw3BxCTx7cq0I1XYPNi+3GlB7LTM2ZqYRO4Gb4qN8ygaIWXNSVcijA2lAYu6rnayuqLvDQTorQyEq8xOPizTA0s+yLzG90g0FWz1ChZcOmFK18TDR3amov/GlxhK07Qa6hP5rseDsxddZCMuHhtJ9EESIti+TeI9jV7ee1QpanMiT6U0nmNSJgxAsM9Ub0RPsV1y1uhfk1k3c1i8v4RbZqGOwvH2Lm6DEbQN/L/AEqZNScxPf5UZllsp7yrhzxG6ct4BaF1fpgDn9z8KgbWApqmOE5V4Z1cIDhX1WVoUTLJVLq5YExVhYFJcbEDi/wJw7Ec1jBsDV4/ZNdTqhHjXkl1gq5ObpcmU4Hx+ATERHkNeSySJuh3x8z1EV3og2gmoAzpQgUJNJjt60dphApfVrdIs7fKh9DOAOTY+cEWrWWyvWPGaTO1j8UIosERv22sbKyYRwwNvvVI0DzZM0lpiEekhfr3QKYE7rCdeDxtlw2DWlehT6YR3djuVlo7RpsLz1Q7TmdQeZTko1qtCtp/UEDteeZu26P4hOBeT/EHDnFolI1TDvQpU6EwhYbOQl/vIAH36eqMPCLYPn8sbBduzIHaHgFTY/Vnm6CnwfXCLrLMEF9EqiXXX/hwXcSm6FQD2jwbtAVIzhu8QDwokEMYNB9iIPj06i39qGLT1ZvrZzeEdlOrvonrm8uXK98Q/znjxUEysYKnwQzKTrUntMqwNPGVjza6w7oNmaeXpfxj+APR9wT8TfFQRbp1hx5KKvJ5Gc3iw5EbucQzmnpkpWgEjPY4YXm6WF68ugUIg/FIweQ6B0FR/GDVhtggBhpH1YZAJBTV+aFTXzkqKsiZwSCojkBoVBqTbuBfQRhWPUtE2aq81qbGAcRSSWSsKSgRwjXX5InVV36bYYm6ecgj6hJms0nfQgPDR3GT6qKYMDKD7ASJRfm7jtdg01Z3yNnyamhxY6fXev31kOh0T6RBfkMs3jMx54gDR1w6zq+FR7eiG2ZERrcE13toV7CCDvpmtz6+mWfaC+ulHhIGcq86U4CnXocDESKgRhy5SczxiOgguPEn0g29EIMvHCCq8gN5XewGmkJoHNtaxuJY4YwL9VcPTV9sMbW+OWfAGYaBniDfky5gCTrnE5fCZurn0plu7pxQ3l4GC00GVXO4ucHH1WA5UgZ/2M5WntQPiFlL9ji8gugOe2OmLtLt6KoJunIQJrG1f2myqbXusooZdbseYZr71oBaTWVjPOyTVC1BU6J8HkiVMGTM1AkfH8E74qW/ZXVzNS/1IvmtjKBlAsqBbKDug3ekxoiWTaMdOP67/BsqEuHUWFuQv1NTCkgmFg1saAexHG+a8RCqo2L2gTQlM78m5e8OSLcJCVFB+nbPhZ/F2xMma0dbhUTKTtI8RRkj9Kp/Wz28OHfSvx3w7d+QZhKqVV6mC9XIeZGwSXA9NF9NS8JHWBiqan+9SIkT/yUDe3An5oxrFtRAg1VIBjgiNnpJAr2iKyI5aH234Noh9723VbsXLDnqKh+3zWGElaNxaxuOQvYRBjdl6Sg8zD8fuRyXT65xlI0ZTOD11oZd1VF8MOQoWfFVYwFeEg+Jiy/6QuhSxfZgwJFGBUskG048pvwaq51PLOW+frFHfvPhYb9SRYA5Nv9xZb0l1oYoyw64mwbR4QEfNNC/wj5ppOmDYssVTr6UYABi8dwzAAx8XJIxj/JHJ3GbL1kYaeumlnmIGSr1lvrm5XgFWplRWVvEX0hd+8vxMP3h7ghx4iraWWXz0qhilF8gZh3Kx6K3KIFWrhW2mMPl+yzKwmPxReeBIS4vRuiACGI7gAl5i4wWYhpTMnAjIoy7XuEmrEUz2dGdD5MTjCLqXAPPdiJ/JKfmYTJX+/MxrJ3okqRhXTYdF7y1GinGwNCaXmANLWXCuNSJ0WuKoeNKznT9TA2YPA1g1F+2oTqIy+g3qfh/5u5d6aIAk5sd9VSdkUBi66uCNjlt2UVkbTOoJS5iffpWno8z5ZK98b2B59+zhrmQ4AXCezQ8quTURgriMcw5DnRCcE2d+MIOwlzFvpsBqkoj3KLwiaP0mnRq0V738o/AjHRpjGv1LSQcuPCzlCvPe2Eam4kiLm1wjV49WZ5QOuzC9Q7Q==
- Ironport-phdr: A9a23:J9Bysx38kz2a8GWXsmDO4wMyDhhPgJ3EezUN459isYplN5qZl7zcNUDSrc9gkEXOFd2Cra4d2qyM6/2rAjNIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfLd/IA+ooQnNtsQajoVvJ6QswRbVv3VEfPhby3l1LlyJhRb84cmw/J9n8ytOvv8q6tBNX6bncakmVLJUFDspPXw7683trhnDUBCA5mAAXWUMkxpHGBbK4RfnVZrsqCT6t+592C6HPc3qSL0/RDqv47t3RBLulSwKMSMy/mPKhcxqlK9VoAyvqQFjw4DaY4+VNeZxcazGcNwAWWZBW9xcWzBdDo6+aYYEEuoPPfxfr4n4v1YAqQWxBROrBOPq1DBDm3343bA10+Q8Dw7GxxErEtUMsHTUsdX1O7oSXv6uzKTT1zrDae5Z2S3j54nGaBwuvfSMXa9qfcXP1EYvChrIg1ONooPqIz2bzP4Cs3SH7+V+T+KvjXYqpx1trjWtxskglIvEi58Rx13Z6Sl0xIk4K9OlRUJlY9OpEZteui+aOYZ4Qc4vQWJltSg7x7AatpO2YSwHxpQmyhPZdveJfY+I4hf5W+aQJzd1nHdleLOjhxqo70ev1/D8W8+p21hJtipIisTAum4O2hDJ9MSLUOZx8luh1DqVygzf9O9JLVgpmabFKJMt2KA8moAcvEjdBCP7l136gLKIekgn4OSk9f7rbqjmq5KeLYN5iQPzP6IzkcKlG+s4KBIBX22D9OS8yrLj+Ur5Ta1QjvIolqnWqpDbKd0Fqa+2HwBV0pws6xCwDzi4ytgXh38HI09feB2ZgYnlIU3BIPXlDfulnVujjSpry+jHPr3nHJrNMmDOnKr/cbt+8UJQ1hA/wc1D659UEL0NPez/V0HpuNzdFBA5Mgi0w+j9CNV604MTQWCPAq+EMKPdrF+H+PkvLvKWa48TpTn9MeYq5vD0gXAlnF8dYLOl0oUKZ3ClBvhmOVmWYWLwgtcdFmcHphYxTOvziFGbTTFTY2uyULkn6zEgCIOmCJ/DSZq3jLyA2ie7BJxWaXpcBlCCC3e7P7mDDr0HbzvXKct8mBQFU6KgQskvz1vm4AT90v9sKvfe0iwer5PqktZvsb79jxY3oB55FcOY3imtUm5pk3hAEz02wa9irFdVw1GPy6VnxfddCJpe6+4fAVRyDoLV0+EvU4O6YQnGZNrcED6OcpCdGTg0C+kJ7ZoLakd5Fc+li3jr1iymGbIK0beOGdo5/r+OhhDZF4NG03/DkZIZoRw+WMInHWSgirRy6E7YApOPnkmExf7CXZRZ5zbE8SK49UTLvExcV2ZYS6jBVGFaa1vdrd3/6U6ERrmiE7k4dABE1IiPJrYYMrXU
Hi,
At some point in my project, I use Defined rather than Qed to have transparent proofs and use the Compute mechanisms to evaluate some statements. This works nicely for my own theorems, but I am stuck when this involves theorems provided by the Coq standard library, NoDup_dec in my case, but ultimately this might extend to more situations.
One quick and dirty work-around is to copy/paste the code, change Qed into Defined and voila! But this is not satisfactory.
I could find some blog posts like this one https://plv.csail.mit.edu/blog/computing-with-opaque-proofs.html by Clément Pit-Claudel on this topic, but again it seems this imposes some rework.
I understand Qed and Defined are different for a reason, I am just curious whether there is a systematic way to change Qed into Defined on a case by case basis, or if we are forced to this type of modifications.
Is there some suggested readings on this topic?
Thanks |
- [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, Jerome Hugues, 04/21/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
- Re: [Coq-Club] Qed opacity and Coq standard library, Jerome Hugues, 04/23/2021
- Re: [Coq-Club] Qed opacity and Coq standard library, Jean-Christophe Léchenet, 04/21/2021
Archive powered by MHonArc 2.6.19+.