coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Formal Way to Express Provability in Coq
- Date: Fri, 6 Oct 2023 17:11:04 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mukeshtiwari.iiitm AT gmail.com; spf=Pass smtp.mailfrom=mukeshtiwari.iiitm AT gmail.com; spf=None smtp.helo=postmaster AT mail-yb1-f181.google.com
- Ironport-data: A9a23:5y7zVqmIEDYNhdqbA4iOOTTo5gz9I0RdPkR7XQ2eYbSJt1+Wr1Gzt xIaD2GHaPiNZTD2etlwOYi+p0tQsMDXz4VlSgU4/yw9HltH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvymTrSs1hlZHWdMUD0mhQ9oh9k3i4tphcnRKw6Ws LsemeWGULOe82Ayajl8B56r8ks1562q4G1A5zTSWNgS1LPgvylNZH4gDfrpR5fIatE8NvK3Q e/F0Ia48gvxl/v6Io7Nfh7TKyXmc5aKVeS8oiI+t5uK3nCukhcPPpMTb5LwX6v4ZwKhxLidw P0V3XC5pJxA0qfkwIzxWDEAe81y0DEvFBYq7hFTvOTKp3AqfUcAzN18N29tN5UK1NpyKlNJy tUUBTQpTECc0rfeLLKTEoGAh+wmJcjveZIV4zRulGGAS/khRp/HTuPB4towMDUY3JgfW6aDI ZBAOHw2PE2ojx5nYj/7DLo7geSlnXnjciJRslPTpKs2/237wwl40byrO93QEjCPbZwPzxfD+ DOWpgwVBDlKasG71mGo2U6yubXShSX1ZIQLEoano6sCbFq7gzZ75ActfVC8uLyyjlO0c8lOL lQdvCsot6k7skKxJuQRRDW9qX+A+w8WAp9eSr1jrg6KzaXQ7kCSAW1soiN9VeHKffQeHVQCv mJlVfuwX1SDaZXEEi7PxaTetj6oJykeIEkLYCJOH0NP4MDurMt3xljDR8pqWvz9xNDkOyDC8 xbTpggHhpIXkZEq0Ye/9gv5mD6CnMXCYTM0wQT1ZVibyD1FSrSrXbH11miD3818dN6YanKjo Ek7n9Ov6bFSLJOVyw2IbuY/PJCowPenNjfjr0ZlNMQj/W71+lqIX4NZ0BdhLmhHb+cGfj7IZ hfImAVzvZV8AlqjXZVVUamQVfs47PHHPsv3c9zpdfxyW4hVWC7b2TBxdGiS8nvIkkNxoZogO JyeT9mgPUwaBYtj0jCyYeUXip0v+QwT2kLRQoLd3T288L/DekOQd6gJAGGOYs898qmAhgffq PRbFsmSziRgQP/MWTbW/aETPGI1AyACX76ukPNud8mHPgZCM0MiAaWIwboeJqpUr54MneLMp nyASktUzWTkvkL+KCKIVCFHSKjuVpNBv34ELXQSHVK36UMCP6erzokiLqUSQ5d21dZe3cZVT uYEcfquGv5gaCrK0BVDYIjfrL5NTgWKhwWPNRWLeDIUJsNRRSHVyN3JIi7UqS8EVHuxv+QDv oz6hx/6QIUCdStmHs35ePKi9HLvnHk/ycZZfVrEHclXQ2roqLNVEi3WiuQlBu09MjDB+2eq7 BmXChImuuX9mY85393Xj6SirY3yMe9BMmdFPmvct5CaCDL7+ze9/Ip+T+q4RzDRe2fq8qGEZ +8O7fXdMuUCrWlaobhHDLdn4qIv1eTB/4YA4FxfI0zKSFC3BpdLAHqMh5BPv5IQ4I5pg1K9X 0bX9+RKPbmMBtjeL2cQAwgbP8CjzvAfnwfA4csleHva4DBFx5vZcEFwESTVtgljAupUCq0Hz 90lmvYq0C2kqx9zMt+5niFerGuNCXobUpQYjJIRAa61qw8n1mB9ZYf4Dwno6qqucPRJCFEhe RWPtZrBhpNd50vMSGUyHn7zxthghYwClRRJ7V0aLXGLp4bhqtoo+iZOqBIbYx9wzBpV985SY E1QKFxTN6GC2xxKlfpzdTmgNC8ZDSLI53Gr7UUCkVPoanWBV0vPCTYYEvmM9kVIyFBsVGFX0 5/AwVm0TAuwWt/62xYzfktXq/bDa9hV3S+akeCFG/W1JbULUQDHsISPO1VR8wDGBPkvjnLpv eNppeZ8SZPqPB4q/pEUNdOo6qQyejulekpyGP1vxfZcVyWUMjS/wiOHJE2Na9tAba6Cu1OxD 8t1YNlDTVKi3SKJtSoWHrMIP6QypvMy+d4eYfn+EAbqaVdEQuZB6/o8NxQShVPHh/1rmMc5b 5LbLneMSzzJw3RTnGDJoY9PPW/QjRzoouHj9LjdzQnLP8trXCJQnYUa3b69vnHTOwxil/5Rl B2WfLfYloSO1qw197YB0cx/68GcJtb6VeDO+we22ziLgRUjLu+W3z4oRpLb08i68FfftxmbV VhAjTIv4H74gQ==
- Ironport-hdrordr: A9a23:+is6t6qJQ5ZtpXkX9Yh4C94aV5omeYIsimQD101hICG9E/bo8P xG+c5w6faaskdzZJhNo7C90cq7IE80l6QFg7X5VI3KNGLbUQCTXeRfBOXZslnd8u7FmtK1F5 0MT0GzMrLN5JFB4/rH3A==
- Ironport-phdr: A9a23:KY87zx3K1HFfL6BUsmDOHQ4yDhhOgF0UFjAc5pdvsb9SaKPrp82kY BaPo6kzxw6VFcWDsrQY0bSQ6/ihEUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7F skRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCS+bL9oI xi7rArdu80ZjIB/Lqo91gbFrmFHduhIxG5kP06fkwr56syt4JNt7iNctu47+cVdS6v6ZaM4T bJZDDQiLW844dDguAfAQwWS+HYSS30anRVUDQfL6hH6RYrxvTDhtuVhwimaPNb5Qq4yVD+/8 qpkUh7oiCMANz4k7GHaj9F7gaxHrB69oRF03ojZa5yXOvVjZKPQZdwVS2pPUMhSSiJPHJ+zY pAVAOYdJ+tVtZXxq0cMoBa4GAKiBPnvyjhNhnLu2K06zuchHh/d3AwgAtkOrHXUrdvvO6cIU OC+0a7FzTDeb/NVxzj984jIcgwgofCCR71wa8vRxVMuFwPEj1WQtYnlMiia1uQIqWeb7u5gW fizhG4grgF8uz6izdojhYfVnIwa0EzE9Tlnz4YvI921UFJ3bNGqHZdMtiyWKZZ7T8w/T2x1v Cs0xaAKtJy1ciUFyJkqxh3SZ+GDfoWL4h/uV+ifLzl6iXxrfL+ymRi8/Eymx+bhVce0yE5Ho jRZntTIrHwA1Bze5tKZRvdg+kqtwyuD2gPO5uxCPEs6j7DUK4Q7zb41jpcTsVrMHivxmEjui a+ZbEQk+uyx5+Xnebrqu4aQN4Fphgz9L6gigMO/AeM/MggBW2iU5/6w26Hk/U38WLlKj/s2n bfFsJ3CO8gXuqq0DxVW34sj8RqzESqq3dACkXUaL19JZQqLj43zNFHPJPD4A+2/g1OpkDpzw vDGI77hDYvWLnjDjLfhfLh85FRGyAoy19xf5pNUCrAdIPL2QULxu9nYAQU4Mwyw2eroFNJ91 oYGVWKJGaCWKLnSvkOQ5uIzP+mMY5cYtCvlJ/g/+/HulWM5mUMafaSxwZQXb2m4Eu16LEWdf HrjmcwMEXwKvwo7VOzlkkeOUT9VZ3aoXqIz/Cs3CIy8DdSLeof4i7uYmSy/A5d+Z2ZcC1nKH 227WZ+DXqIJdSGfOc8pjj0bXKKgA9skyBKjrw/myqVuNOuS+ywZqZfL29185umVnhY3o28nR /+B2n2AGjkn1lgDQCU7ifgXSS1Vz16C1fI9mPlEDZlJ4PgPVA4mNJnaxug8CtboWwuHcM3aA E2+TICABjc8Bsk038dIe1x0TtC/jR3Y3zarHLYPlvqKBZ0o94rT2nHwI4B2zHOVnLI5gQweS 9BUfXajmrY58gHSA4DTlEDMkrupeL8cwC/S/X2Ci2uPvV1deAF1WKTBG3sYYxietsz3s2XFS bLmErE7Kk1BxMqFf7NNccHshE5aSe3LPd3fZyegkT71C0/Yn/WDa43lf2hb1yLYYKQduyYU+ 3vOdQ03ByP75nnbECQrD1XkJUXl7eh5rnq/CE4y1QCDKUN7hfKz/VYOiPqQRul2vPpMsTo9q zhyAFe23s7HQ9uGqQ17eaxAYNQ7qF5Z3GPdvgZ5M9SuNadnzlIZdg12uQvp2XAVQs1FjMsnt 3M2zRV7M6Pe0VJAazaw0pX5O7mRIW73vViuZ6PQxlDCwYOO4K5cjZZw417nvQyvCg8j6yA9i 4gTgybavMybSlNCCMGUMA5/7RVxqrDEbzNo4orV0ScpKqyoqnrY3NlvAuI5yxGmdtMZMaWeF Qa0HddJYqrmYOEshVWtaQoJee5I86thdca7dPad2LKqI+96nXSnjGVb5ahy10uN82x3TeuCj PNni7mImxCKUTvxlgLrt930lJtEeTANF3C+jynlBZJUTqJ3dIcPT2ypJofko7c2z46oUHle+ lm5AloA08L8YhueYWv22ghI3FgWq3iq8ceh5wR9iCph7q+W3SiUhv/naAJCIGlAAm9rkVbrJ 4GwydEcRkmhKQYzxlOp4kPzxq4To6oaTSGbRFpLcjP2M2B9W7Gx8LuDYtJKwJwtuCRTFu+7Z BiWR6X8rB0Tzy74VzEGlXZrKnfw48S/xkwjwGuGSRQ75GLUY8Rx2QvS6JTHSPhd0yBHDCh0h D/LB0Statyg/NGajZDG4YXcHyqqUpxedzWuzJvV7nPqoz03R0fmzrbqyoS0dGpymTX23NRrS yjS+RP1Y42xkr+/LfoiZE5jQln198t9HIh61Io2npAZn3YA1fD3tTIKl3n+NdJD1Ofwdn0IE HQO3t3Y+wj52VJqNHPPxoP4SnC1zc5oZt38aWQTkHFYjYgCGOKP4bpIkDEg6F+lrg/KYeR8g T4HyL0v6X8GhskGvQMsymOWBbVYTiw6dWT80h+P6d65tqBeYm2iJKOx2ERJltekFLieowtYV SWxatI4ECR39Mk6LEPU3Si59NT/YNeJJ4F21FXcg1LaguNSMp50ivcamX8tJzfmpXN8g+8j0 U41gNfj7dDBcTkyuvr+WEIQNyWpNZ1PvGu21uAHwJ7Qh8f2T/ADUn0KRMe6E6zuSWpI86yhb 0HUSHU9sivJR+SZR1POrhc+6SqIScjjNmnLdiZDi4w+AkDMfgoHx1lEOVdy1p8hSlL1mIq4K ho/vnZJoQem4hpUlrAxb0m5CziA4lfuMnBuEdCeNEYEt14ZoR6EbYrGqLo0Rn89nNXprRTRe DbDNkIYUCdQABzCXxe6YfGv/YWSqbHGQLfuaaKfO/PW7rUPH/aQmcD1i9UgpW3dcJ7VeCElV qxeuAILS3l9H46xdywnbSsRmmqNaseaoE354ShrtoWl9/+tXgvz5IyJAr8UMNN1+hnwj73Rf +iXzD10LzpVzPZujTfB1aQf0VgOiipvayjlELIOsjTIRb7RnakfBgASaid6Ps9Fp6wm2QwFN cneg9Lznrl265x9Q09CTkDkk9q1aNYiJmi8MBbWDh/OOu3WfHvExMb4Za76QrpVza1VuxC2p TeHAhrjMzCExFyLH1ikNeBBij3ePQQL4tnsNEYwTzK6HZS/OkToVb0/xSc7yrA1mH7QYGsVM DwmNlhIsqXV9yRTxPN2B21G6HNha+iCgSeQqefCefN0+bNmBDp5k+VC7TE00bxQuWtBWf94g yvOr8FnuVDgk+iO1j9PXx9HqzINj4WO9xYHW+2R5txbVHDI8QhYp32XEAgPrsB5B8fHvqlRz p3envu2Jm4SqpTb+swTA8WSI8WCeilEU1KhCHvfCw0LSiSuPGfUihlGkf2cwXaSq4Aztpnmn JdmolpzW1k8F/dcAUNgToRqyHhfUTYtkLrdh8kNtyPWRPj5QcxbutXWXKvXD6y/cXCWir5LY xZOyrT9f9x7Cw==
- Ironport-sdr: 652031ac_Ubz7O+iBZNiSP5U/3/plCY5jRpmRTKaoqvpVgafTFRIK+28 n1G7wKvyhp8dy+7Aadg0tvZknRnhBBjx1dmbXqA==
Hi everyone,
This question is just out of curiosity. I understand that Peirce's law is not provable in Coq (constructive logic)
(I tried it in Coq and reached a point where it was impossible to construct an element of type Q from the context).
I am wondering if there is a formal way to say what is and what is not provable in Coq.
Best,
Mukesh Require Import List Utf8. Import Notations. Lemma peirce_law : ∀ (P Q : Prop), ((P -> Q) -> P) -> P. Proof. refine (λ P Q f, f (λ p, _ )). (* There is no way I can construct an element of Q from the given context: P, Q: Prop f: (P → Q) → P p: P *)
- [Coq-Club] Formal Way to Express Provability in Coq, mukesh tiwari, 10/06/2023
- Re: [Coq-Club] Formal Way to Express Provability in Coq, Meven Lennon-Bertrand, 10/06/2023
- Re: [Coq-Club] Formal Way to Express Provability in Coq, Li-yao Xia, 10/06/2023
Archive powered by MHonArc 2.6.19+.