Skip to Content.
Sympa Menu

coq-club - [Coq-Club] rename bound variable

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] rename bound variable


Chronological Thread 
  • From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] rename bound variable
  • Date: Sun, 9 Feb 2025 20:10:07 -0500
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f45.google.com
  • Ironport-data: A9a23:b5U9kqBfBBXIBRVW/4Pnw5YqxClBgxIJ4kV8jS/XYbTApGxz0TEHz GAZUG6PO/2PYDH1f9x2PIm+pBxVvsPXnNdmOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yM6j8lkf5KkYMbcICd9WAR4fykojBNnioYRj5Vh6TSDK1rlV eja/YuGYzdJ5xYuajhJs/jb+Us11BjPkGpwUmIWNagjUGD2zCF94KI3fcmZM3b+S49IKe+2L 86rIGaRows1Vz90Yj+Uuu6Tnn8iGtY+DiDS4pZiYJVOtzAZzsAEPgnXA9JHAatfo23hc9mcU 7yhv7ToIesiFvWkdOjwz3C0usyxVEFL0OavHJSxjSCc51zoNCrG7qxtNUURY6EC5P5TDjBgz NVNfVjhbjjb7w636LeyS+0pi8h6ace3YcUQvXZvyTyfBvEjKXzBa/+StJkIgXFq3pAIQau2i 8kxMVKDaDzJaR1OIVcaC9Q3mu6uij/+ciFXgF2QrKszpWPUyWSd1ZC3aIWOJYbSHZ89ckCwn XzA2mj8E0AhN9mRxya131iAt7DpknauMG4VPOblr6Y10QP7KnYoIBYRTB6wpeSzolWvXspWb U0S4Csn66YonHFHVfH4Vhy85XOI51sSB4cWHOo95wWAjKHT5m51G1ToUBZQRpt3nuJvRgUu8 QGlhc3xITM+noS8HCf1GqivkRu+Pi0cLGknbCACTBcY79SLnG3VpkKRJjqEOP7l5uAZCQ3NL ya2QD/Sboj/YOYO3qS/uF3L2nei+sWPQQky6QHaGGmi62uVhbJJhaT5tzA3Dt4Zc+51q2VtW lBax6ByC8hQUPmweNSlGrllIV1Qz6/t3MfgqVBuBYI90D+m5mSue4tdiBknexw4a5xZKGeyO h6N0e+02HO1FCv1BUOQS9LhY/nGMYC5RLwJq9iNPooROschKGdrAgk1PhLLgD6FfLcQfVEXY srCKZn9Ux72+Ixoyz25Q+pV0LkggEgDKZD7FPjGI+Cc+ePGPha9EO9bWHPXN7xRxP3e/G39r Y0EX+PUkEo3bQELSnOGmWLlBQtSdSBjbX03wuQLHtO+zv1OQT17V6OIme1/KuSIXc19z4/1w 510YWcAoHKXuJENAVzihqlLMeu0AcRMvjggMDYyPF2l/XEmbMz9pO0cbpY7N/1vvuBq0fc+H bFPdtSiE8Z/bG3N2w0cSp3h861kVhCg3jyVMwSfPTMQQp9HRi7ywOHCQDfBzic1IxSSidofu JyljwPSfooCTV9tDeHQc/Oe8Gmytnk8xsN3BkvBHcZPSnrV4KxVGnTXtaIxKZtdLx/s+yarj VeKIBYHpNvip50+38nJiJul8aaoMbpaNWhLE1bL6Y2ZMXHhwVOi5otbQsOkTCv7Vmjk3ImDP MJ7l+rdNt8Dl3Z067tMKa5hl/8C1oG+to1kwRRBN1SVSVaSU5dLAGSMhOtLvY1zno5pgxO8A B+zy4MLKIeyGZ3XFXAKL1AYdcWF7/YfnwfS4dkTIEnX4CxW/qKNYX5NPiuj2TBsE79oDLwLm esRmtYaywiauCoYNtyriiN19WPVClciV64hlI8RAa61qw4N52xBX6fhCX7N0MnSU+lPD0gkG S/Lpazgg78H+FHOXUBuHlfw3M1cp680hjZ08HE4KW60x+X13s0M4EUJ8BAcbBhk8RFc4uciZ klpLxJUIIuNzRdJhe9CfWamJC9ZDjbE+Eark1otv0/aRnmOSWbiAjAcO+GM3UZB6ENaXGFR0 4+5wVbfcwTBXZ/OzAprfmV6udnPcMdXyjTSvOyGQ+GUAIgcYxf+p62lOFoztBrsBP0uiH39p eVF+Ph6bYv5P3Uyp5IXJpa717MCbgKtP01HHO9c+Z0WEVHmeD2d3SaEL2azcJhvI93I6UqJN Nx8FPlQVhiR1De8kR5DPPQie4RLpf8O4MYOXpjJJmRc6ruWkWdPgaLqryP7gDcmfsVqncMDM bjuTjOlEFGLpH5qimTI/dhlOG25XIE+XzfC/tuJqccHK5FSl9tXUxAW8qC1tHCrIgdY70qqn AfcVZT3kc1m66pRxrXJLIsSJj+aC93JUMawzDuSqPVLNNPGDtfPvVgaq37hJAVnAoESUNVWy 5WIvMLG40femLMQTWriuoKgEpNR7p6YR9tnMcPQLVhbkxCdWcTq3QAxxmCgJbFNk/Jf/sOCR TbkTOeVavguRI576FBOTipRATIxKv7SVbjxgzG5o9CnKAkv4SaeIPyJrXbWPHxmLAkWMJjAO yrIkveJ5PUDia9TBRUBVspUM7UhLHDNAaIZJsDM7x+GBWyVg3SHiLvotTwkzRrpUnCkMsLL0 ajpdyjEViaZmf/3lYlCkolIoBcoIm53grAwcmIj6tdGsW2GI1BcH9sNE6ctK89yqTPz5qHad TuWTWoFCAfBZxpmXyj4wuzeWla4OrRTFPb/fzAnxhbBIWP+ToaNG6Bo+Spc8m97MGmrhv2uL dYFvGb8JF6ty5VuXvwe/eG/nfwh/P7B23YU4gropqQe2frF7WkijxSN3TahVBAr1+nInUTPY GU5HCVKHBz9Rkn2HsJtPXVSHXn1ed8pIyoANU+yLBT34u13D9GsDNXwPujy1vsIa8FiyHsmW ybsX2XUi4yJ8iV7hEbq0u7FRYd7DPuKGo6xK6qLqcj+WU2vwjxPAv7uVhbjgC3vFMCz3r8de vSRD6ACOXm4
  • Ironport-hdrordr: A9a23:YK6xl68xkuv6ScBqLoJuk+D1I+orL9Y04lQ7vn2ZKCYlC/Bw8v rFoB11726XtN98YgBCpTniAsm9qBHnhPpICOAqVN/IYOCMghrOEGgN1/qF/xTQXwP7ssFQ3b p9aKRlYeeAaGRSvILV5E2XHb8br+VvM5rFuQ4d9RpQpM1RBZ2IJj0ZNjqm
  • Ironport-phdr: A9a23:o3SelBRU1QENSPMlOLxNo8ivodpsouCWAWYlg6HPa5pwe6iut67vI FbYra00ygOSB8ODs7kf1bSG++C4ACpcus/H6ChDOLV3FDY7yuwu3DYcSPafDkP6KPO4JwcbJ +9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9FYHdldm42P6v8JPPfQpImCC9YbRvJ xmqsAndrMYbjIV8Jqor1hfFvnREdupXyG5pJl+YghLw6tut8JJ5/Cldte8t+9RcXanmeqgzU KBVAikhP20p68LnsgXOQxGI6nUATGsdjwBGAxLC7BH0X5fxtjX1u+9g0ySEPsP4UK45Vy264 6hkVBHnhiEHNyUk8G7Mkcx/kLhboBO6qBNhxYPffZyYO+B/fqPZetMaWHZBU8NMXCFPHo+wc 40CBPcHMO1FrYfyukEOoAOxCgesCu3hySJGiGHq0qAhyestDRvL0RY8E94SsnnZqsj+OqcIU eCyyanF1SnOYOhW2Tf884jIcg4uofKRVr9sd8re008vGB7YhViXs4PqJDOV1uUWs2ib8eVgV vijhHQhqw5rpDig290giojIhoIJxVDJ7ip5wIMvKt25TE53e8KrEJxVtyyDMYZ9X8wtTX1yt ikg1r0GpYC0fDIMyJk/2RPRa+KKfpWH7xzsSeudPzl1iGxmdb+jiRu88Vasx+L4W8S2zVpHr DdIn9nMuH0P1BHe6NSLRuVj8kqi2juC2Qbe4fxKL0AzkKrUMZ8hwrgom5UPtkTDBCn2l1vyj K+SbEkr5PWn6/nhb777pZGcL5d5hh/iPqkqgMCyAuQ1PhIQU2SH+umwzrLu8E3/Tb5XkPA2l rTZsIvGJcsFvK63Hg5V04c95BunEzur1skTk2MdI1JfYh2HipDkO1HQL/D8Cveym1Gsny1qx /DCJ7HuHIjCImXanLfvcrtw61RQyAU0zdBY6JJUDq8OLOjvVU/2sdzUFh45MwqqzOb7ENhxy J8SVGaVDqKaMK7eq0GE6v4sLuWWa4IYuC7xK/0/6P7viX85l0Udfa6s3ZYPcn+3BfRmI0SCY XrsnNgBEn0GsRA4TOPwjl2NTCRfZ3ezX6Ig6TE2E42mDYLZSYCshLyNxju0HppTZmxeDFCDC m/nd5+YVPcUdCKSPshhnyQZWbS5UY8uyQmutBPmy7pgNufb5ioYtYv62Ndp4+3TiAo9+CdvD 8Wd1mGNV3t7knkJRz8wxqB/oFZyxk2N0ahi0LRkEolY4OoMWQMnP9aIxOtjTtv2Rwjpf9GTS V/gTM/wUh8rSddk6tUOYl19FtbqpxbK2SbiV7Yfl72QBJE3tKva1n79Ycd813nu26wojl1gS cxKYz71zpVj/hTeUtaa236SkLynIPx0NE/l8W6CyTDLp0RESEtqVq6DW3kDZ0zQpNC/50XYT rboB650ehBZx5ukLa1HIsbskU0AXO3qbd3UY2Oqm2qzQx+Oz7WAKovrZ2o10yDUCUxCmAcWr j6dLQZrPi66uCrFCSB2U1fmYkfi6+57/XqxTk4vzwyJKURn3ry5vB8UmfO0RPYa37ZCsyAk+ H1vBFjo+dXQBpKbohZ5OqVRZdRo+FBcyWfQrBBwJLSlJqFmw1MSKkF54x6o2BJwBYFN18Mtq RvG1SJULqSVmBNEfjKch9XrP6HPb3P191apYrLX3VfX1JCX/L0O4bI2sQerugbhDUck/3h9t rsdm3KB+pXHChYTWpPtQw428RZ9vbTTfig64cvdy3RtNaC+tjKK1cguAaMpzROpftEXN63hd ke6GscaBtOuJe9skl6gaB5CPeFO+4Y7Osqnc72N36vqdOdskTS6jHhWtZhn2xHplWI0QerJ0 pAZhvCAi1HfBnGs0RH76pCxxd0XAFNaVnCywiXlGoNLM6h7fIJRTHyrP9Xy3NJ1wZjkR39f8 lenQVIAws6gPxSIPDmflUVd01oapXu/lG621TtxxnsgpKqexyzDwKLrchMBNihKRXVtpVjpK ImwydsdWQL7Cmph3Avg/kv8y6VB8e52JWnSWkdFfG7/KWhkXu2xt6aNS8FK4ZIs9y5QVa7vB DLSAq64qBwc3ST5GmJYzz1ubDCmtKLymBligX6cJnJ+xJbAUfl53gyXpNnVRPoLmyEDWDE9k z7cQF61I9iu+9yQ0ZbFqOG3EWy7BNVfdizizIXIsyXehyUiCBe/nuuzl96hGA4z1yO91th2W g3HqR/9Zs/g0KHyPe98f0ZuDUPx8IIgQtA4wtZ23slAnyRHzpyOmBhP2X/+K9Baxb7zYDIWS DgHzsSUqAnp1Ut/L26YkofwV3GT2MxkNJGxZmIb3D547tgfUv/FquwZ23Et8hzk8FG0A7A1h DoWxPow5WRPhugIvFBo1SCBGvUIGkIeOyXwlhOO5tT4raNNZW/pf6LjsSg21d2nEryGpRlRH XjjfZJ3VyZ67sRkMF/PlnT144foPtjRcd07uRidkhOGhO9QYsFU9LJClW98NGTxsGdwgecxj R113Zy5+oGBImNhuqO4HhFwOTj8ZsdV8Tbox/U7/I7ez8WkGZNvHS8OVZ3jQKezET4cgv/gM h6HDDw2rnrIUaqaBwKU711q6m7eC53+fW/CP2EXlJ8xIXvVbFwamg0fWy8224I0Bhz/jtK0a 193v3gQ/gKq8UYKk7MwcUOjDSGH4130IjYsFMrBcFwMtVoEvhmNd5TZt7MWfWkQ/4X9/lLTb DXDPUIQSzlOABTMBki/bOfwo4Ocoq7IXqzmaKGWKbSW9b4BDbHRmdT2g9Egp3HVZqDtdjFjF 6FphRYFBCokXZyfw3JWFWQWj36fNpbL4k7jpWsn6Jj4qq2jWRqzt9LQUP0LYIkpo1buxv7dU ozYzCdhdWQCjsJKlSKOkeJPmgZV0n4mdiHxQ+5Z62iQHOSJy/URV1lCOmtyLJcatftimFMWa IiA0JWtkecp65x9Q0FMUVir8i2wTeoNJWz1dFbOBULRca+DOSWO2cb8J6W1VbxXiuxQ8Ry2o zeSVUH5bHyFkHHyWhajPPsp7mnTNQFCuIy7bhdmCHTyBNPgZBqhNdZrjDowibQqj3LOPGQYP HByaURI5rGX6CpZhL14FQkjpjJ9KvKYni+C8+TCApMfsP8uDygt0uwGvTI1zLxa6CwCT/tw2 WPTotNov1C6g7yPxz5gA38s4n5AgIOGu1knOL2MrMERHyaZukhVvSPMVkdvxZMtENDktqFOx 8KakavyLG0H6NfI5Y4GAMOSLsubMX0nOB6vGTjODQJDQyT4UAOXz0FbjvyW8WWY65YgrZ250 pMESr5AVFE2UPocA0JpWt0DPJhfUTYtkLrdh8kNrynbzlGZVIBBs5bLW+jHS+3oMyqchKJYa gEgxLr5KcEeOtS+1RA/LFZ9m4vOFgzbWtUH8UgDJkck5U5K9nZ5VGg63UnoPxis7HEkHvmxh hcqiwF6bIzFGx/j5l42IhzBoy5iySHZfP3qhDmQdHj6K6LiBem+6gLxvkk1d573GkN7MVD0k ktjOzPJAblWiuk4HV0=
  • Ironport-sdr: 67a95215_lKuom9nMHddKJPw/hPg8O2GmPHKqK6AV7XKAiYRhXCJ+0ns 6iuB4EDsZdNEWZ/QbVI8u+LrcDhdgdp1lXG6FhQ==

Is there a way to rename a bound variable? 
For example, when proving the goal exists n:nat, n=1, can I ask Coq to rename n to nn?
I guess it can be done in Ltac2 by creating an alpha equal constr with the desired name and asserting it. I am wondering whether someone has already written something to achieve this.

Thanks,



Archive powered by MHonArc 2.6.19+.

Top of Page