coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Talia Ringer <tringer AT cs.washington.edu>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] New proof repair tutorial just dropped
- Date: Tue, 8 Mar 2022 01:43:39 -0600
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tringer AT cs.washington.edu; spf=Pass smtp.mailfrom=tringer AT cs.washington.edu; spf=None smtp.helo=postmaster AT mx6.cs.washington.edu
- Ironport-data: A9a23:uvKg1qLTt9GoflxMFE+RHJMlxSXFcZb7ZxGr2PjKsXjdYENSg2QBx zFMWWrVb/zfamH2ed12aIngpEgBupDcy9RqHAEd+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t 63yTvGacajYm1eF/k/F3oDJ9CU6jefRLlbFILas1hpZHGeIcw98z0M78wIFqtQw24LhWFvS4 YiaT/D3YTdJ5RYkagr41IrY8HuDjNyq0N/PlgFWiVhj5TcyplFNZH4tDfnZw0jQHuG4KtWHq 9Prl9lVyI92EyAFUbtJmp6jGqEDryW70QKm0hK6UID66vROS7BbPqsTbJIhhUlrZzqhroFNz dd1ibGLdyQbAKiUwe4PVDtTOnQrVUFG0OevzXmXtNzNiUbdNWTl2PVvCk4qOote9+pqaY1M3 aVCeHZXNkDF273wnevTpupE3qzPKOH3JoIZtXx65TrCS+kvWpDCRarW4tke0Tst7ixLNayCN pBFNWA3BPjGSzZTMV5JC8IXpszrtEuhVjR3mlerrrVitgA/yyQsiea9boG9lsaxbc5ShwOTo n/M13/oBwkTct2Z0zuMtHy27tIjhgv+SNxUH6b+6fdxgFyVyXAUDlsbWUbTTeSFZlCWaoNjL k4sxgcVk4sAyknzF9PvWD+ziSvR1vIDYOZ4H+o/4QCL76Pb5QeFG2QJJgJ8hMwaWNweGWN0i QTS9z/9LXk26ufOFSjAnluBhW7aBMQDEYMVicbopyM+7tD/vIU+5v4kZoczSfbu5jEZ9MGZ/ txnhC0u2fMYlogU3r67/FbInzWq4JXFU2bZBzk7vEr+sGuVh6b8OeREDGQ3Ct4Zd+6koqGp5 iRspiRnxLlm4FHkvHXlrB8xNL+o/e2ZFzbXnERiGZIsnxz0pSL9I98PsGkhfxkwWirhRdMPS BON0e+2zMIIVEZGkYcrC25MI59ykPa+SbwJqNiJMYEmjmdNmP+voXgwNRDLt4wcuFUqkL8yI 4yabdfkCnhSFq18zDuwSPsa19cWKtMWmAvuqWTA503/i9K2PSfFIYrpxnPRNrhhhE5FyS2Lm +ti2zyil00PALegM3OMreb+7zkidBAGOHw/kOQPHsbrH+asMDhJ5yb5zexzdop7sb5Sk+uUr HixVlUBlwj0njvYIB6Ka3ZsdLTpG5tzsCtjbyArOF+p3VklYJqusf1BLsRpJeF/+bwx1+NwQ tkEZ96EU6ZGRTnw8jgAaYXw8d55fxOxiAPSZyeoOWBtf5NpSwHT1MXjew/jqHsHAiat7JRsq KbmyQrAQZsFSBhlCoDbZO/2lwG9un0UmeRTWUrUI4QJJhyzrtAycyGo1605OcABLxnH1wC27 QfODEdKv/TJrq807MLN1PKNoIqeGudjGlZXQjvA5rGsOCiGpmeuzNMSUOuMejyBBmr49L/4P LdQ36+6O+ZBg19Rs4t6HKpsy+Qz68a2/+1WyQFtHXPqaVW3C+46fCDZg5EX7qAdlKVEvQaWW 16U/ocIM7u+OPT6HQNDPwEidOmCi60Zw2GA8fQvLUzmzyZr577bA15KNhyBhXAPNrdzK495k +4ttNRMsl66mkRsOc3AkSlP92WKIWAHVeMquoxDWN3njQ8iy1djZ53AC3KsvsjQNY0UakR6c CWJgKfihqhHwhSQeXQEFU/S0LcPnp8Joh1LkgMPfgzbhtrfi/Yr9xRN6jBrHB9NxxBK3u8b1 rKH7KGpyXFiPguEhfSvm0ipC18HDwbf5UXqy1oPm3HeSQ+lWnGlwKjR/wqS1Bhxzo6eVmEzE HKkJKLNWi2sY8jq3io0VlJirbruQcEZGsjqhpW8B8rcd3UlSWONv0JtDFbkbzPsGoUujVbHp O9l4OF2L6D3KEb8ZkH955ayjdwtdfxPGICOrTyNMk/E8aEwtQxeAQSzFn0=
- Ironport-hdrordr: A9a23:MGsORak1dNBW47VprDjtR5sUFsjpDfKC3DAbv31ZSRFFG/Fwz/ re5cgz/QT/iTYPVHxlsc3oAtjBfZquz+8M3WBxB8bfYOCIghrOEGhd1/qX/9SNIVycygayvZ 0QMpSXJrXLfBJHZOzBkUKF+05K+qjIzEiQ7d2ugEuEp2lRGuxdBn5Ce0qm+y5NNXZ77PgCZf yhD5F81k3QD0j/B/7TbhJuMoStybyqqHuBW290O/cJ0njGsdrC0s+LL/Hs5GZ7b9o5+8ZGzY GqqX2a2k392MvLtCM16QXonuZrcZDau6B+7YS3+7Iow5/X+3eVjI8KYcz2gBkF5OaorF4wmt jNvBtIBbU615r+RBDJnSfQ
- Ironport-phdr: A9a23:c0sFnhS4ENrWVJ2QKNCcbbeIFNpson2WAWYlg6HPa5pwe6iut67vI FbYra00ygOTB8OCsq8P0rKJ+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpV O5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxtWiDanfL9+M RW7oQrMusUKg4ZpN7o8xAbOrnZUYepd2HlmJUiUnxby58ew+IBs/iFNsP8/9MBOTLv3cb0gQ bNXEDopPWY15Nb2tRbYVguA+mEcUmQNnRVWBQXO8Qz3UY3wsiv+sep9xTWaMMjrRr06RTiu8 6FmQwLuhSwaNTA27XvXh9R/g6xbrhyvpAFxzZDIb4yOLvVyYrnQcMkGSWZdXMtcUTFKDIOmb 4sICuoMJfhWoJP5p1sPtxS1GBWiBOLpyj9HmHD2x7Ax3uM9EQHc3QwgGd0Ov2rOrNjuKKgSS vq5zafSwjXYb/NW2DH96IfUchAmp/GAR6x/ftfMyUQ2EQ7Ok1qfp5D/MTyPyuQNr3aU7/BmV e+3i2AqqAF8rzmry8swhITEmIEYx1PE+ylk3Is4Jd22RkF1b9OnEJZduCGXOYt5TM4hQ29kp SI3xqAYtJO4YiQHypIqzAPRZfyAdoiH+BPjVOCJLDd3hXJlZLK/hwup/kS61uL8Ucy03VBXp SRGitnBrm0B2wLQ58SdVPdx4kSs1SyA2g3R8O1JIV04mbLFJ5I9xrM8jJkevETZEiPrmUj7j bWae0og9+Wu9u/peK/ppoWGOI9xkgz+Mrohmsi4AekgNwgPUGmW9f6g273450H4Tq9FjuY2k qnYtpDaKtgbpqm/AwNPzIks9gu/Ay+n0NQeg3YHMEpIdA+Zg4XqIV3CPuz0APSlj1mjkjpn3 fDLMqD5DpXINHfDkbPhfbhn605bzQo+1cxf54hVCrEHL/L8RFXxucfEAR8iKQC1zfzoCM591 oMfX2KPDbOZMKTUsVOS+O0gPvSMaJcTuDnmM/cl/eLhjWclmV8BeqmkxYYbZGiiHvt6O0WZf WbsgtAZHGgWuQo+VfXmh0GGUT5OfHm/RLk85zE+CIK+F4jPXIGtgLqb3Ce6BJJafG5GCkrfW UvvIo6DQrIHbD+YCs5niD0NE7a7GKE70hT7iAb+yrMvFOvS9SAC/cb/ztlz6ODJvRopsyN9F MSc1W6RSGcyk28VEWxllJtjqFBwnw/QmZNzhOZVQIQ7D5JhVw47McSZ1OlmE5XoXQmHeN6VS VGgS9HgADcrT9t3zcVdK11lFYCEiRbOlzGvH6dTj6aCUYAu86TT0mLZLN071H/d1KgngEUhR I1COXD1zrVn+V3rDpXS216ci77scK0d2CDX82LW0XCPuk5VSiZ7SuPaVGsfZ03ZsdP/oE7OU uzmEqwpZy1Gz8PKMa5WcpvpgFFBEe/kI8jbanmtln2YAAbWgLiXKpXjYGUc2irBD05CngwOl ZqfHS45ACrp42fXDTg0UEnqf1up6+517nWyUk4zyQiOKUxnzbu8vBAP17SaTLsI07QItT1Ey X08FUuh39/QF9uLphZwNKRab9Qn5V5b1GXf/wVjN52kJqpmixYQaQNy90/p0hx2DM1Hn61I5 Ds21gt0Jq+C+FhaMSyRxpDxPLLLLW+08RyyKubX1lzYzNeK6/IX8v1rzjer9AqtF0ck7zBmy 4wMiSvavM2aSlZNF8+oASNVv1BgqrrXYzcw/dbR3Hxoa+yvtyPansguD60jwwqheNFWNOWFE hXzGosUHZvLSqRill63YxYDJO0X+rQzOpbsa+GH3qGmJs5rh3S5hH9H4YZyzkWKsSdwV6Sbu vRNi+HdxQaBWzrm2R29qMHxlo1eTToJWHW20ijlAoFNYas0cIoWQzTLQYX/1pB1gJjjXGRd/ VioCgYd2cOnThGVakT0wQxa0Ul/TWWPoSKj1HQ0ljgoqvDaxynS26H4cxFBPGdXRW5khFOqI I6ujtlcUlL6JwQukRKk4w79yc057OxjNWjVTkpSVyPtaX5rSauxsLWeZMgJ5Z81+SlaS+WzZ 1mGR6W1+kFKlXm7Ty0Cm3ZmLnmjofCb11RihXiYLWpvoXaRYsx2yRrFpZTdSfNXwjsaVXx9g DjTCEK7Oorh9tGVmpHf9+GmAjv7BtsJKXmtkdzG6XLogA8iSQeylP2yhND9RA0z0CuhksJvS T2NthH3JI/iy6W9N+tjOEhuHl71rcRgSeQc2sM9go8d3X8Ci9Cb530CxC3vK9Rd1q/kRHEWA yEC2N7U5gf530slI36UjdGcND3V0o56at+2b3lDkD4n7sZFBb2856cCgiJuolu+oh7WZ75wk ipXmp5MoDYKxuoOvgQq1CCUBLsfSFJZMSLbnBON99mira9TaTXnYf2q2UF5h9zkEKCar1QWR iPiYpl7V3wVjI03IBfW3Xb08I2hZNTAcYdZqEiPixmZx+EHM5ctjv0XmWxsIiTgojsox/Ne7 1Qm3Inm7tLfdiM3pvr/W0EHcGSpOYRIoHnslfoMxJ7Lmdr1RtM4RGhNBce2CqnydVBa/fX/a 1TXSm16+yrdQ+aFW1XFsgA99TrOC8z5bivHYiNBnZM6AkTafxYXgRhIDmxgzthjTlDsnZy4N h8+vG50hBawqwMQmLs0b1+mDj2Z/13uM21kD8LCZBtOslMbux+TaJDEqLgoQ2cBpM3m9lHoS CTTZhwUXzhWAQreWgilZOPxo4GHqbTQB/LifaKROvPU9LQYDqnYg8v3gsw9pVPufo2OJiUwU ax9ixMFBy0jXZ6C3G5VAy0Py3CUNZ7d/k/svHcu8obhrbOwAmeNrcOOE+cAaI8/vUru0eHdb 6jJ33w+cmwQ14tQlyaSmP5FhA5U1XkoKmXqSu5l12aFTaTbnrJbAkwscDt9csRP6K04009GP suTi9X+0qN0g6wuE1kDTUbmhsyiec0NJSe6KU/DA0GIcr+BIFipi4n2Z6i4VLFd3utYrAW+p C3dHVXuJTSOkjDoU1auNqlNiiqfIRBT6oagbhxqFG7vSdvnbluwN9lpjDpwx7Ao4xGCfXgVN Tw2G69UhpuX6y4QwvB2Gmgbq2FgMfHBgSGSqe/RNpcRt/JvRCVyjeNTpnogmfNT62lfSfp5l TG3zJYmqky6kuSJ1jtsUQZf4jdNioWRuEx+OKLfvpBeUHfA9RgJ4C2eERMP79diD9TuvehXx L2t3OrrLyxe9tvP4cYGL83EdoSMKzw+OAHpGTjbEAwDCzOnKCCXhkBQlu2T6mzArpU+rcuJ+ tJGQbtaWVopU/ICXx0/TJpYeMcxAmxizOfI6axArWCzpxTQWshA65XOV/bIRO7qNC7cl75PI R0B3bL/K40XcIz9wU1rLFdgz+GoUwLdW85Apip5Y0o6ukJIpTJiVGw11E//Qgi2pmAaDv61m BEqjQ04bOgwvmSJgR9/Nh/RqS08nVNk083imiyUeSXtIb2YWJEITSHv8Vc4KZP6RQlpagv0k EB5fmShJfoZn/5rcmZljxXZsJ1EFKtHTKFKVxQXwOmee/Qi1Vk0QsqPzlQB+uLeCZpkmxctd 9iho28SgmqLifY+PurPLbFJz15fmqWI+CKky7JpqOf/D0MdriWZY2gXsVcIN78pOy2uuOFg9 F7a8wY=
- Ironport-sdr: Es/Wv74PsHuL1LjHwqNkbPOYM652vj6CzkGKeks3dTcXhp8ucsOXUDs+sALU0BE7DOYIDDQsYt OeCoQ3d9E90HoNGcYT/PYy5w5MQC/HREuAgV5BQq/Yj76/C7usDCc200vzWSy7JWwHCIXAp9Xr zPiIwpDWpW5rqI28jGUqRGJmMfaMj32FO9GdirIK0x4blhTiqJ6mmVMc1EujYurwkAreQZcyz8 Ibh3ucuAJUX70R7n3gJAgqAYZFALp2vRSTeOV/m3OxjeQNhkIA1iWkl0sRU4IYGgQ9aFv14h6/ RKHrnEYvckZwpsWhCG48qaPJ
I decided to implement a tutorial teaching people how to implement proof repair, so basically a simplified version of my thesis work exercises pulled out that I hope can be completed in like an hour or two. Check it out if interested:
I'd love feedback. Also if anyone wants to get this in Coq's CI I'd appreciate it, but I'm too drained to spend more time on this for now.
Talia
- [Coq-Club] New proof repair tutorial just dropped, Talia Ringer, 03/08/2022
Archive powered by MHonArc 2.6.19+.