Skip to Content.
Sympa Menu

coq-club - [Coq-Club] I've completely formalized 3 key chapters from Rob's Type Theory and Formal Proof textbook

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] I've completely formalized 3 key chapters from Rob's Type Theory and Formal Proof textbook


Chronological Thread 
  • From: Iaroslav Baranov <kciray8 AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] I've completely formalized 3 key chapters from Rob's Type Theory and Formal Proof textbook
  • Date: Sun, 5 Jan 2025 05:09:24 +0300
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kciray8 AT gmail.com; spf=Pass smtp.mailfrom=kciray8 AT gmail.com; spf=None smtp.helo=postmaster AT mail-yb1-f175.google.com
  • Ironport-data: A9a23:yriphKz3rKcUn04XFBV6t+eawirEfRIJ4+MujC+fZmUNrF6WrkUEn GBLXGjTaP6Na2ugeYojPY2/9BwBvceAmtcxHAVr+VhgHilAwSbnLYTAfx2oZ0t+DeWaERk5t 51GAjXkBJppJpMJjk71atANlVEliefSAOCU5NfsYkhZXRVjRDoqlSVtkus4hp8AqdWiCmthg /uryyHkEAHjgmQc3l48sfrZ9Us25Kiq4lv0g3RnDRx1lA+G/5UqJMlHTU2BByOQapVZGOe8W 9HCwNmRlo8O10pF5nuNy94XQ2VSKlLgFVDmZkl+B8BOtiN/Shkaic7XAhazhXB/0F1ll/gpo DlEWAfZpQ0BZsUgk8xFO/VU/r0X0QSrN9YrLFDm2fF/wXEqfFPW3vFeJ3oLGLQS+78qC11jq tE0FBkSO0Xra+KemNpXS8Fpj8UnadjhZcYR4y49iz7eCvkiTNbIRKCiCd1whm9hwJATW6yHN oxANmcHgBfoO3WjPn8UA5Mklfb4rnb6ejxc7lmSoMLb5kCJlFUti+K2bIu9ltqiWppYhlfIl l3/0EPQJEgjGOOO1BSb/Sf57gPItXimAdpNRePQGuRRqFaU3ykYDAAcfUCqpOGwzE+4QdNWb UIOkhfCtoA3/U2vC8j3Bli2+SHZ+BEbXNVUHqsx7wTlJrfoDxixPHUAfhV6Vfkfvs5vGDYW+ wCks+/AGmk62FGKck61+rCRpDK0HCEaK24eeCMJJTfpBfGz8OnfaTqfHr5e/L6JszHjJd3nL 9m3QMUWgrwSiYsa3fz+8wmY3nSjoZ/GSgNz7QLSNo5E0u+bTN/4D2BLwQGEhRqlEGp/Zgfc1 JTjs5bFhN3i9bnXyESwrBwlRdlFHcqtPjzGmkJIFJI87Tmr8HPLVdkPu28mfRo1Y5lVIWGBj KrvVeV5tM870JyCPf8fXm5NI55ypUQdPY26BqCKMYAWCnSPXFPfoXk3PSZ8IFwBYGB3zPhnZ sbFGSpdJXkdDqtjwXK3QexbuYLHNQhvrV4/savTlkz9uZLHPCD9Ye5cbDOmMLplhIva+1692 4gEZ6O3J+B3CrGWjt//q9NLdQhiwLlSLcyelvG7gcbYeVY4Rjh7VKKJqV7jEqQ895loei7z1 inVcidlJJDX3BUr8C3TMis/OoD8F41yt2w6NiEKNFOlkSprK4W24atVM9N9cbA7/aYxhbR5X tsUSfWmW/5vczXg/yhCTJ/fqIc5Sg+nqzjTNAWYYR8+XaVaeSr3xvHecDHSqRY+VhiMiZNmo pmL9B/qfp4YdgEzUOfUcK2Oyn2yj1g8mcVzfU3CHfdLcm6x8oIwcy3Vpd00KvEqNh/s6Ga71 QGXIBFAvsjLgdY/3+fojJC+jbWCMrVBDGsDOELE/5OaCDL8wlOz5aNhDMOZYiH7Vk7v3aepO NVu0PD3NcMYkGZws4ZTF6hhyYQ87YDNo4B24xtFHnLZSUaCEZJlf2e72PdQup13xrN2vRW8X mSN8IJ4PZSLIMbUL04DFjE6b+is1eAmpReK1K4beH7F3S5Q+KaLdW5wPBPW0SxUE+ZTAbMfm OwkvJYb1hy7hh8UKe25tyFz9VmXD3k+Qq4i54A7Aojqt1IR8Wt8Q6fgUw343JLeTO93EBgOA iSVj6/8lbhj1hL8U34sJ0Psg8tZp7oz4S5v8nFTBm60iuLkh+A21iJ/6T4YbBpY5TQZ3vNRO lpEDVxUJ6KP9QhGnMJoBj2dGSxdNh+0oWrKll0DzjzfRWaVS12XfXEcOPmMzm8d4WlzbjhWx 5DG6WfHABLBXtD94Ts2YmFh88fcdN1W8hbQveyWBOKHFIkeTRu8pYH2fksOiR/sIf1ptX39v eMwodpBM/zqBxAfs4gQKte8141JbDumOWYbY/Vq3J1RLFHmYDvohAS/cRGgSPhsec7P31SzU fF1B8R1UB+76iaCgxYbCYMIIJ52hPQZ38UDSJy6OV85t6ajkRQxvKLy7iTegEoZc+dqm+s5K aLTcGumOU6Ujn12hWTMjZdlPkyVXNo6XzD/jduFqLgxK5E+se9XYR4T1JmwtC6rKwdJxU+fk z7CQK709NZc77pQsbHiKYh5PDXsG+jPDLyJ1CuRr+Vxacj+NJaSlgEN9XjiEQdkHZoQfNVVk 76ynsb99x7HtuxuUkTyuZqIJ49W7+qcActVNcPWKiFBvC2gAcXD3ToKy1qaG7dozuxPx5CAb BSqTeeNbvgpYsd56FwJTjlBAjAfJr/SbKy9lRiirv+JNAcR4TbHIPyj63XtS2NRLQ0MBLHTF S72vOSI9PlDjYERGiIBOe5qM6V4LHDnR6EiUd/77hucL2uwh2K9qqnQrgUh5R7LG0u7Pp7Du 7ydfSfHdTO2pK3s5/NaudYrvhQoUVBMsdNpdUcZo9NLmzS2CVAdFtskMLIEN4p1lxLj35Spd RDPa2ofUR/GZwpmSimlwtrfXVa4PNcsa+fJfmljuwvebiqtH4qPDYdw7ioqsT88ZjLny/rhM t0EvGH5Oh+q2JxyWOIP/bqBjPx6wu/BjGc9kawnfxce3z5FaVnL6JBgIOaJfSnOEsWIhU+SY GZsGj0CT0a8Rkr8V81nfha53f3fUCzHl10VgeWnmb4zeLl3CMVPzfT+P6f41bhrgAEiOusVX X2uL4eSyzn+55HQ0JfFf/omhKZ1DbSAGc3SwGoPg+ENt/nY11nL9P/uUcbCoA/ONeKf/57ge uGQ3kUD
  • Ironport-hdrordr: A9a23:kh+Jk6sNApz4BQLv8/fGm6xU7skDTNV00zEX/kB9WHVpm62j5q aTdZEgvyMc5wxhOk3I9erwW5VoIkm9yXcW2/h1AV7KZmCP01dAR7sSibcKrQeQfBHWx6py0e NPfcFFZ+EYzmIXsS852mSF+hobruVvOZrIudvj
  • Ironport-phdr: A9a23:EKlA3RxcrtsRoVjXCzLTwFBlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z xWZvK4yxwOTFazgqNt6yMPu8JrcEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzH cBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/9pPObwlSmTawb7F/I Bq5oAnPq8IbnZZsJqEtxxTGpXdFZ/5YyWR0K1yNgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7U LJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5 LplRRP0lCsKMSMy/WfKgcJyka1bugqsqBN/zYDaY4+bKeRwcb/GcNwAWWZMRNxcWzBdDo6+a YYEEuoPPfxfr4n4v1YArgGxBROrBOP0zj9HnGH21rAn3us7CwHJxgogH9UQsH/Jq9j1N7sdU eGvzKbSzTTObOhb2Tj46IfScxAhpeuAUq53ccrU0EQiER7OgVqMp4L/JTyVyvgNvHaB7+pmT e+jl3MqphxsrzWu28ohi5TFi4wUx13a9yh0w4g4KNmkRUB7fNOqEJtduiOVOoZqQs0vXn1lt Sg0xLMJupO2fycExZI6zBDRbPyHdpKH4hPlVOuJLjd4hW5leLKihxmp60Sv1ur8Vsyy3V1Xr SRFisHBum4R2xHX8MSKSftw8l2/1TqS0w3f8PxILEI0mKfdNpUs3LowlocIsUTfACD2glj4j K6Xd0o64uWk9+Lqaaj8qJCGLY97kAT+P7wumsOhBeQ4NRADX22B9uS90L3v5E34T65XgvEvn KnVrZLXKMQBqq62BA9V1Ykj6xKhADu8zNsYmnwHIEpEeBKBkYfpJ0nDLO7kAfq7mVihkzdmy +rYMrH8BpjBNGXPnbXhcLpl7k5T0gszzdRR55JODbEBJer+Wkztu9zZFB82KQy1zuX8BdVy0 4MRQ2OPAquDPKzOtl+I4/ojI++Xa4ANojbyN+Al5+LyjX8+gVIRYLGl3YELZ3CgAvRmP0KZb GLwjdcGCGcGpxYxTOj3iFKZSjNTfHazX6ck5j4hEo6mDIHDRpqsgLObxiu7EIdWNSh6DQWHF m6tfIGZUd8NbjiTK4lviG8qT7+kHq4ozxa1sAbkg5BuNOPS/TNQ4ZHo1cJ89r37mhQ79DgyB MOYhTLeB1pol38FEmdllJt0plZwnw/rOclQhvVZEYYW/PZVSkIgMpWayeVmCtf0UwaHf9GTS V/gTM/1SSopQIcXxNkDK114B83klgrKiimhAqUchuyjC5k986aa1H/0dI5m03iT7KA6lBE9R 9dXc2ivh6px7Q/WUo3Ckl+QhvaCeqEV3SqL/2CGniKVpE8Ndgl2XO3eWGwHIEvbqdOs/kTZU 7qnEqgqKCNEwM+Gb7pAM5jn1AobAvjkP9vabiS6nGLY6Q+g4LSKYcKqfmwc2H+YE00Yi0UJ+ n3AMwEiByCnqmaYDTp0FFupbVm+ue954Gi2SEM51WToJwVoyqa19xgJhPedV+Jb37QKvz0ko il1G1D11szfCt6JrQ5sNKtGZtZ17FBC3GPf/wtzW/7oZ6Nph0QXYlRfsEbn1hExAYJF0IAro H4s0AtuOPeAyloSPzic3J32JvjWMjyopEHpO/OQgAiPlo/Jp/RqirxwsVjosQC3G1B39nxm1 4MQyH6A/tDQCwFUV5vtU0Ex/hw8prfAYyB76ZmHsB8keaSyrDLG3MokQeU/zRP1NdRUMbmNB V/aHMgTBszoI+sv0QvMDFpMLKVJ+ag4MtnzPfiN2bSiLbZIkzevjGAB64d4mBHE5293TejG2 IwAyveT016cVjvyu1ymt9j+hYFOYTx68nOX8SH/H8YRY6RzedxOEmKyO4itwd44gZfxWnle/ VrlBlUc2cbvdwDAJ1D62ARR0wwQrxnF0WO7xD1umiB5hqWa1S3Khe/lcVILN3VKS29rkVr3a dLs3pZKAQ7yNllvzUT4rU/hj7BWvqF+M3XeTSIqN2DtImduX7Hx/ruObshT6Y855CBeUeCye 1efGfb2pxoX1T+mHnMLnmhqMWH3/M+gzloj1z/OSRQ75GDUcsxx2xrFsdnVRPoLmyEDWDE9k z7cQF61I9iu+9yQ0ZbFqOG3EWy7BfgxOWHmy52NsCyj6ChkGxq6yrqwkdz9GBlq+SD+3thuE y7PqVyvB+ujn7T/Ku9hckRyURX/4MtgE5AuuoQ1jZAUn3Mdg9/GtWpCmmD1P9JB3Kv4Z3dYX j8Hzene5w390VFiJHaElOebHj2Nh9FsbN6gbiYKyzowuopUXbyM4uUOzmNl50C1pgXLbb1hk ycBnLEwvWUCjbhs2kJlzz3BUOtPWxAJZWq2y0vOt5fk8O1WfDr9L+T2jhEl24n/VPfa5VgNE HfhJsV8Q2kptp85aBSUlyerj+OsMNjIMYBN6FvOz0aG37ATcNVrzrILnXY1Zji75CFjkr9hy 0QphMHyvZDbeToxuvvjX1gAcGWyPp12mHmljL4CzJ/Oj8b2QconSnNTG8GxBfOwTGBL6q+hb lfSVmV68jDCR/LeBVPNsh836SKSVcnxZzfPYyBGqLcqDBiFeB4F2V5SAWV8x89jUFjtnZ2pc V8ltGpIuBii8UoKkbgub16mAy/JrQOsIF/YUbC5KxxbpkFH7kbRa4mF6/5rWjtf9dunpRCML WqSY0JJC3sIUwqKHQKrOL7m/tTG/+WCY4j2Z/LTfbWDr/BfXPaU1Nqu1IVh5TOFKsSIODFrE fQ63kNJWX0xFd7enn0DTCkeliSFaMD+xl/04ipsssW26+jmQirq7IqLTqpYaJBhok/rx6iEM OGUiWByLjMZnpIAyHnUyaQOiV4fjyY9ElvlWb8EtCPLUOfRgvoNV09dO341bpIZqftjg1ooW 4aTkN7+279mg+RgDl5EUQakgcS1fYkQJGr7MlrbBUGNPbDAJDvRwsixb7nvLN8YxOhSqRC0v i6WVkH5OTHW3TriVgqmILFkgySSPRgYs4a4OEUIayCrXJf9Zxu3PcUixyUx2qExj2jWOHQ0N DF9dwZcpOTV43oH37NwHGtO6ncjJu6B0XX8jaGQOtMdtv1lBT5xnuRR7SEhyrdb2ypDQeR8h CrYqtMGS7SOneyGyz4hWx1L+G4jbGOjuExjPeDI/MAFVy+boVQC6mKfDxlMrNxgWIWHU094x d3Glaa1IzBHoYu8wA==
  • Ironport-sdr: 6779e9e1_O0VF0SCEzRhEooJn+My6tjwNJImaMpa1Zs4wSmuIfXwmddV jRadG9WPHbvStBtMtKLGst+U2rh/rfqHLJ6GSAQ==

Chapter 11 (Flag-style natural deduction in λD) - NaturalDeduction.v

Chapter 12 (Mathematics in λD: a first attempt) - MathematicsFirstAttempt.v

Chapter 13 (Sets and subsets) - SetsAndSubsets.v

I've turned off Coq Standard Library (-noinit option) and everything is developed from scratch and no inductive types are used. I developed a new Coq dialect which is as close to the textbook as possible.

I'm happy to say that the modern version of Coq (2024) is 100% compatible with the original Calculus of Constructions and λD extension. I bet chapters from 2 to 10 is also possible to formalize, so you can keep it in mind if you would like to learn type theory deeper.

I would like to get some code review and suggestions/corrections. Any feedback is good. https://github.com/kciray8/the-great-formalization-project/pull/2/files

Keep in mind though that I decided to save a bit of time by allowing coq automatically name things for me (H0, H1, H2 etc) and haven't done any code refactoring for readability yet.


--

Iaroslav Baranov

kciray8 AT gmail.com



  • [Coq-Club] I've completely formalized 3 key chapters from Rob's Type Theory and Formal Proof textbook, Iaroslav Baranov, 01/05/2025

Archive powered by MHonArc 2.6.19+.

Top of Page