coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: kirang <kirang AT comp.nus.edu.sg>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Forcing computation through opaque terms
- Date: Sun, 29 May 2022 05:53:41 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kirang AT comp.nus.edu.sg; spf=Pass smtp.mailfrom=kirang AT comp.nus.edu.sg; spf=None smtp.helo=postmaster AT mailgw0.comp.nus.edu.sg
- Ironport-data: A9a23:Gw7nG6OUtmylEePvrR1zkcFynXyQoLVcMsEvi/4bfWQNrUolgjVTz zROC2iGbPrfZzDwfd5wOo60/RgH6pLSx4RqT3M5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8kk/vgqoPUUIYoAAgoLeNfYHpn2EsLd9IR2NYy24DkWVLV4 LsenuWGULOb824sWo4rw/nbwP9flKyaVOQw4zTSzdgS1LPvvyF94KA3fcldHFOkKmVgJdNWc s6YpF2PEsw1yD92Yj+tuu6TnkTn2dc+NyDW4pZdc/DKbhSvOkXe345jXMfwZ3u7hB22os1hl /hMmKeaQDYZBrL0wsYNSwthRnQW0a1uoNcrIFC6uM2XwFKeNXDrxu0oClwte4AU56BsDgmi9 9RBc29LN0vZwbLqhujjIgVvrpxLwM3DP4IFs3dv5TreCO5gR43YBajG+JlD01/cg+gVTaqGP ZNHMVKDajzNTABRIncuDagake2qiXPuU2Zl8XCa8P9fD2/7ll0vj+e0a7I5YOeiTsJM202cu 2ju5HX8GhhcNdqFyDPD/GjEuwPUtXOnHdhKUra/8+YshkCIgGEfFVsNWjNXvMVVlGaBZs9Pd GEV1xEEpJkCzFOTFPvtRw+B9SvsUgEnZ/JcFOgz6Qeow6XS4hqECmVsctKnQId73CPRbWByv mJlj+8FFhQ26+XEGBpx4p/N9WjtZ3NNRYMXTXZcJTbp9eUPt6kIoXojpP5YEai6h8XyAzyYL 9ui9XJWuln+pZ5Xkv/ju1vAhirqoIXSCAM5+0PMUQpJDz+Vhqb4OeRECnCCs56sybp1qHHa5 RDofODFsIgz4WmlznDlfQn0NOjBCwy5GDPdm0VzOJIq6i6g/XWuFagJvmwlexkzbJZVJG6yC KM2he+3zMQNVJdNRfMuC79d9+xwpUQdPYq4C6uKBjawSsIrLmdrAx2ClWbKjj6yzxF3+U3OE ZGSbcerC38eQblhzSS7Xfwcza5jwS523mLVSpnjyA6quYdyl1bJIYrpxGCmN7hjhIvd+V292 48GZ6OilkUOOMWjM3K/2dNCcjgicyNhbbio8JM/SwJ2Clc8cI3XI6WPkepJlk0Mt/k9q9okC VnmBxEIkAGh3SefQehIA1g6AI7SsV9EhSpTFUQR0ZyAghDPuK6js/UScYUZZ74i+LAxxPJ4V aBYKc6HB+wJTCncvTkRcN/mo9U6JhisgAuPOQujYSQ+L8I5GFSZqoe8c1u97jQKAwq2qdA68 u+p2Q7sSJYeQxhvUZTNY/W1wlLt5XUQwbogX0bBLtRJVl/r9Yxmd374gvMtepxeIhLG3n2cy h3QDBsF4/LC+tdn/N7MjKGCjoGoD+ouQhMFRzmLte67bHCI8HCizIlMVPezUQrcDG6kqr+/Y eh1zu3nNKxVlVlHhINwDrJ3wP9s/NDovbJbklxpEXiXPVSmDrRsfiuP0cVV7PYfw7ZYvQSpA gSE/dxCf7OUI4XoHENXPwV8NraP0vQdmz/z6/UpIRWmvXAvrOrfCUgCbQORjCF9LaduNNJ3y Ogsj8ca9gijh0d4Kd2BlC1VqzyBIyBSSakhrZ1GUobnhhBxkwMSPdmGUmn955SXLdNRKQ8nL iLSn6Wb3+ZQwU/LcnwSE3nR3LoB3MtW6EASlFJSdU6Untflh+Ms2EwD+Ds6eQ1Z0xFb3r8hI WNsLUB0ef2D8joAaBKvhIxw99ytxSF1+3AdD3MMnWzdQFbwEGfKKXV7P/uWuk0V7iRHcVC3O V1eJHnNCV7XkAPZh0PemnKJb9ToStlpsAvfg4aqE9nDBJZSjf/NnPq1fWRRw/f4KZpZuaAEz NWGOM57bqjjcygNuOs2B5Tczrt4pNVo4oBdaakJwZ7l1l0wtN1/NfZi5qxxlg5wyyT2zHKF
- Ironport-hdrordr: A9a23:vhgFsaw+UvkdsZYEQTfoKrPwIr1zdoMgy1knxilNoHtuA7Wlfq GV7ZImPHDP6Qr5NEtBpTniAse9qBHnhPtICOAqVN/IMWWIhILCFvAB0WKN+UyCJ8SzzJ876U 8xG5IObOEY0mIRsfrH
- Ironport-phdr: A9a23:A/zbzxRhtZhenOlRLkpWNELHodpsoryVAWYlg6HPa5pwe6iut67vI FbYra00ygOTBsOLsbkU16L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQF cVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHNbQhEnjmwba19I Bi1ogjaq9Ubj5ZlJqst0BXCv2FGe/5RxWNmJFKTmwjz68Kt95N98Cpepuws+ddYXar1Y6o3Q 7pYDC87M28u/83kqQPDTQqU6XQCVGgdjwdFDBLE7BH+WZfxrzf6u+9g0ySUIcH6UbY5Uimk4 qx2ShHnlT0HOiY2/2/ZisJ+kr9VrhGuphNx34Hab5qYNOZ8c6PfYd8WWXBMUthXWidcAo28d YwPD+8ZMOZbron9vUEBrR2xBQKxA+7vyT5IhmXs0q083OQsCh3J3AslH9IWqnjUqsj1NLwIX e+r0abI0C/Pb+hZ2Trk7oXDbx8ur+2WU71qbcrR1VcgFxnDjliIqoHoIzyb2+sPvmWV8+ZsS +KihWEppQxsojWix9ogh4fUio8ayl7J6yF0zZg1KNGmS0N2f8OpHptUui+aKoZ7RsUvSHxrt iYi0rAKpJC2cSoQxJg6yRPTdeaLfouH7x75SuqdPTF1j29/dr2lnRa9602gx/X8Vsaq1FZKq TJIktzWuXAM0xzT5caGRudn8ki93jaP0hjT5vtCIUApjqrXMYAuzaMtlpYJqkTDETf6mETwj KCIakUp4vWk5urlb7n8u5OROZF4hhv9P6khgMCzH/g0PhALX2eB+OS80LPj/Vf+QLVPlvA2k ajZsIrAKsQdqa60GBNa0oEm6xanFTum1skYnWIdIF1bZR2HkpLlO0rBIPzgC/ewmEyjkC13y PDeIr3hHpLNI2DenLv5Z7Zy91ZcyBYvzdBY/59bFrYBIOvqVkDtsNzYEwQ2Phevw+fnDdV9z pkRVXiOAq+fKqPSsEWH6vghI+mWN8cpv2P2LOFg7Przh1c4n0UcdO+nx8g5cne9S/dnOUyfb jK4gdYbGGEFlgE5SfSsjkCZFzNfejCpUPRvtXkAFIu6ANKbFciWi7ub0XLjdnU3TmVPC1TWV Gzta53BQfAHLiSbPs5mlDUAE7mnUY4okx+050fh07QyCO3S92UDsI77ksBv7rjQlAs78zNcB MOYyyeLUnoyk28VASQ5j+hkuUIo8l6YyuBjhuBAU9la5vdHSAA/YJ3d1eV8BPj5XQfZONGUU xCrTsjgGj5iBskpzYooZEBwU86nkgiF3yeuBOoNkKeXAZUv7q/G9334JsJy1C6A364klx8gX 9AJOGG7wLVwn+TKL6jOlUjR16OjdKBGmTXI6H/G122F+kdRTA93V6zBG3EZfErf69rjtAvES Pe1BLIrPxEkq4bKI7ZWatDvkVRNRevycNXYbWWrnm6sBBGOjrqSZYvucm8Z0W3TEk8B2wwU+ H+HM0A5CELD6yrdDSZnE13HaETp6a94tWj9Q0MpiRqFLgVg27ez5h8JlKmEUfpAu9BM8Cwlq jhyABO8x4ePUIXG/lE7OvUAJ4llszIlnSrDugdwP4KtNfVnj18aKUFsul/2kg9wAcNGmNQrq 3UjyExzL7iZ2RVPbWD9v9i4N7vJJ2315B3qZbTR3wSU09eM86EAwP8/rk2luhyyUEcu7jN83 JMGthnUroWPFwcUXZ/rBww09gJzob7yaS44/8XSyGYqPKWp9CTNkYFMZqNt2lOreNFRN7mBH Qn5HpgBBsSgH+ctnkCgchMOOO06GLccB8q9bLPG3aeqOLwlhze6lSFd54s71EuQ9i16Q+qO3 pAfwvje0BHVHzv7iV6gtIjwl+UmLXkRH3C2zyfMD4lUfut0YJ1NBGuzZda4jtlznJ/iXXdE+ UXrXghZnpbyI1zCMxqnhUVZzgwPrGaimDekwjAR8XlhtaeZ0CHUgqzjeBcBJm9XVTxnhFboL 5KzioNSV0ypYg410Rq9sB+hmO4C//45fzWVGx8bGkq+Z3tvWaaxqLeYNstG6Zdy9D5STPz5e 1eRDLj0vxod1SrnWWpY3jEyMT+w6fCb11R3jnyQKHFroT/XY8Z1kF3c5cbVQ/F51T0DXG9+l CKRC1ShecKmt4bx9d+LoqWlWmStW4cGOyrq14qGuwOw4mhyRxuihLa+lsChCgdwgkqZn5F6E C7Pqhj7eIzi0a+3ZPlmckdfD1j588NmG4t6n9h4lNQK1HMdnJnQ4WsfnDK5L4BAwaynJiloJ 3ZD05vP7QPiwkEmMn+Z29ezSCCG2sU4L9yqKmpe2zphvZkRV+HNt+YCzXcz+wLh6lmLBJo11 jYFlal3syFc2rpT/lpxiHzFWPdJRwFZJXC+zk/XqYnl9uMGPCDzKP/rji8c1ZigFO3Q+1oDH i+iINFyQWkqtoIkahrNyCGhs9q7PoCLN5RD6lvOylCb1Y03YNo4xKpWwHM/YCT2ung9jegml lpj0Yz8p4fPIjc9oOfgWkQePTrwf4UV5yqrgKpD2N2ZuuLnVpwzAjIQQMKuRvWtCHQUqO+hO gqTViYz4n7JSeaaR1fZ40BjtzTJDovtOn2KYmIWqLcqDBDPdBAa2llSVzI/htg/CxvsycD8N lx2riYY4lqywvdV4sRvMRS3EmLWpQPyLywxVIDaNh1dqAdL+0bSN8WaqON1BSBRuJO7/kSLL SSAagJEAHtsOATMDk3/PrSo+djL8vSJTuu4IfzUZLySqOtYH/6WzJOr24Fi8n6CLMKKdnVlC vQ63AJEUxUbU4zBnC4TTiUMiy/XR8uSpROz5XUxpce66LLtRRmp6IeSTaBdcJ1u9x2wnaafJ ruQiSJ+elM6ntsHwX7FzqRa3UZH0noxMWD2S/JQ6WiXFPG1+OcfFRMQZiJtOdEd6qs92lMII svHkpbv0bU+iPcpClBDXFinm8ezZMVMLXvuUTGPTEuNKrmCIiXGhs/tZqbpA75RluxSuDW7v jODVUn+JXKOmySvTB/lYoQuxGmLeQdTvo2waEMnEW/4UNfvcQG2KvdyhDwyzqJswHjNMHZaN yVnNU5Bs/uL4mkL55c3U3wE5X1jI+6eni+f5OSNMZcav8xgBSFsnv5b6nA3o1OwxCpDQeQzn jbJ6NNivhe9nbvXotKIeBFJry4Ngp+Q+0huJOPC+csZMZ4l1BcE7GGfFExMrNxgEpvpprsWx 9TS0rn8em8qzg==
- Ironport-sdr: ZBpkPjUzossVmBa0dkmYCR+3F1gIWcImdUsTRVv31fUA/NQPjlmsoI8y2CM0x5cbIc2pVWk0lg NQOD0vpi+vioOMCgfj9SBjra1rP4TbjOSSgih557N1PzALePlHMTny+nnBCXK/LujQMQSDGfMZ lfL67kzzto/qiP72rXvrVgcW71nEsvu2Bk5E2iVJB4Ew2tdoG4zzG9bM3zH/UBwAlZ7VNRpat6 bHxlkIB4SPzrxgzXmoPmDNwFd2emEs1JEAi1Qp6BtaTvgYJVSJ2nc7lIwVprYMEFZmtZPXkWuD WEkaRT34aeb0lqxyaFn6G0H5
Heyo Coq-club!
I was wondering if there is a way to force computation over opaque terms, for the purposes of debugging/meta-analysis of proof scripts.
I understand why Coq doesn't do this by default, and guess it would probably interact in unfavourable ways with proof irrelevance.
My aim is not to use this computation as part of a proof, but rather purely for debugging/meta-analysis - much like how the `Print` command can display the proof terms associated with lemmas, even if they are actually opaque.
Is it possible, using the Coq api if necassary, to perform computation ignoring opaqueness of terms? Think something like a `PrintReduced` command that reduces its argument as much as possible (until it reaches constructors, existential variables or axioms - things for which the definition doesn't exist at all)?
Is this possible while reusing Coq's existing evaluation mechanisms? or is this something that would require a much larger architectural shift?
Thanks,
Kiran.
- [Coq-Club] Forcing computation through opaque terms, kirang, 05/29/2022
Archive powered by MHonArc 2.6.19+.