coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Courtieu <pierre.courtieu AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] unification ignores local evar let bindings
- Date: Mon, 9 Oct 2023 07:50:30 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-pg1-f179.google.com
- Ironport-data: A9a23:bX5J36+K8e8ASSk0SZ7BDrUD8HuTJUtcMsCJ2f8bNWPcYEJGY0x3y 2YfCmDTPqyPYmqgLdh+OYvj/UxTv5LTy4AxT1FtrS1EQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHPymYAL9EngZbRd+Tys8gg5Ulec8g4p56fC0GArlV ena+qUzA3f7nWYvWo4ow/jb8kg25Kyi4GlwUmEWPJingneOzxH5M7pEfcldH1OgKqFIE+izQ fr0zb3R1gs1KD9wYj8Nuu+TnnwiGtY+DyDW4pZlc/TKbix5m8AH+v1T2Mzwxqtgo27hc9hZk L2hvHErIOsjFvWkdO81C3G0H8ziVEHvFXCuzXWX6KSuI0P6n3TExq5RL09sB5Yjodl7E0phx PgaKD8fR0XW7w626OrTpuhEg80iKIzzM9patCg/nHfWCvEpRZ2FSKLPjTNa9G1o14YeQLCEP pdfMGU+BPjDS0Un1lM/EJMzhv2lwHL4bidEqV+IjaUy6mnXigd21dABNfKMIYTTHJsOzh7wS mTuvGfZKypAM+SllyOX4lnwjd/quBunYddHfFG/3rsw6LGJ/UQYDwRTXl+mq9Gim0umUpReL VYV82wgt8APGFeDS9D8W1igryfBsEdDCpxfFOo17AzLwa3Ri+qEOlU5ovd6QIROnKcLqfYCj zdlRvu4XmA9g67fUn+H6LafoBW7PCVffydIZjYJQUFBq5PvqZ06xECHBNtyMr+HvvusExHJw heOsHcfgZcXhpU1zKmVxw3MrA+tgZnrdTQLwDvrcFir1S5DX779VbeUsQDayd1iMLemSkKwu SlYusqGs8ELI5K/tA2MZ+QvGruWye6PG2DeiwQ3Hr0K1Teky1i8d69+vRB8I0ZINJ4fWDnLO UX8hyJY1KVxDlCLM5BlQtuWINs46ITdDvLZb+DwQvsSR4luZSmF0TpLZ0XN71vykUMpr74zC a2bfemoE3weL6ZtlxiyeMswzp4pwTIY10rIZJWm0Smi76WSVESVRZgBLlGKSOIzt4GAgQfN9 udgJ9m48ApeXML+cxvo39Yqd35SFkcCBLfyt8BzXcyAKFA/GGgeVtng8Yl4cIlhx6lohuPE+ 0+mYXBhyX39uyzjCR6LYXVder/QTc5BjXYkDxcNY3es+VYeOLiK0olOVqEKbYEG9fNix8FaV /MqWduNKdURRyXl+wYyV4jcrotjfiuFnQilZjWXchUjTZxNHCvyp9nuJFrp/gYzExvt5Ncfo qKh5CzfU5EsVwRvN+eISfONnnean2kRp/J2ZGTMeuJsQUTL9JN4DgDAldo1Hp08EgrCzT6ky AqmOxcUiu3TqYsT8tOSp6S7g6q2Mul5RGx2InL66OuoCCzk4WaT+49Mf+KWdzT7Vmmv2qGDZ /1Q/s7sIs88g1dGnIptIYlFlZtkyYPUmIZb6QB4EFHgTVehUOpgK0bb+/h/jPRGw7sBtDamX k6KxMJhBoyIH8HbQXoxPwsua9qR2c4Ewgfy6esHG2SkxStV0ofeb2BsEUiitChvIoFxErsZ+ sY6mctP6wWAmhsgadmHqSZP9lWzFH8LUoR5l5QWHL7UjhEPz3dca6f9EQ7z2omEMP9XA3kpI xiVpavMvKtdzUz8aEgOFWDB8O5epJYWsjVI8QMmC3GWvOHa39kb8QZ08zslaih0lDB8zPNVK GxnE2ZXNJe+1W5kq+YbVl/9BjwbIgOS/3LA7mcglUrbahKNfXPMJmhsAtS91hkV3EwEdwcK4 YzC7njuVAvrW8TD3iESf0pBgN67RPxT8jzyouyWL/6nLbIbPwW82rSPYFAWoSTJGcky3U3Lh dd79dZKNJHUC3QinL0ZOaK7i5IgERyKHTkXC7UptqYEBnrVdzyOyCCDYRL5MN9EI/vRt1S0E YpyL8ZITA6zzzuKsitdP6MXPrtoh7Q80bLuoF8wybIu6NNzbwaFsa48MgD7jW4vBs1hyIMzc 9yAMT2FFWOUiD1fnGqlQAyo/IanSYFsWeE+9LndHCY1+1Yrv+RlcEV02byx15lQGBUy5Aqa5 WsveIePp9GPCu1Qc0/EHaBKBgHyItT2PAhNHMZfrPwWBe7y3QzyW8/5Z7Up08m6/VfcZjivq YmwjQ==
- Ironport-hdrordr: A9a23:aO0Z+KvG7wouSOAWFax7F86d7skDT9V00zEX/kB9WHVpm62j5r mTdZEgvyMc5wxhPU3I9erwWpVoBEmslqKdgrNxAV7BZniDhILAFugLhrcKgQeBJ8SUzJ876U 4PSdkZNDQyNzRHZATBjTVQ3+xO/DBPys6Vuds=
- Ironport-phdr: A9a23:WzMaeh+Bn4FvDP9uWZy2ngc9DxPPW53KNwIYoqAql6hJOvz6uci4b AqCv7401AaBHd2Cra4e1ayO6+GocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wE ZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmjmwbalyI Rmoogndq9UajZZ/Iao11hfFv2FEdutIyW5pP16fgwrw6sKt95N/7ipcvO4s+dRdWqvgZaQ4S rJYDDUiM28r4cDgqAfOQwiS6HYCS2saihVHDRTL4xH8RZfxrzD1tvFh1ymAPM35Vq47VDK/5 Kp2UhDoiSMHNzkk8GHLj8F7kaxWrA69qxF53oXZZpyeOvhjcaPHZd4VSmRBUcRRWSJPAY2yc pUBAPYaMOlCs4XwvUEDoQeiCQSuAu7k1z9GhmXx3a0/y+kvCwDG0xI6H9IUrnvfscv4NKAPU eCv0KnIzCvMb+5L0jr68IjIcw4uoeuWXb1ua8be1U4vFx7fjlWMqIzqIS6V2/8Cs2ie9eVgV Oavh3Q7pAF2pzii38EhgZTGiYwJ0F7L7zl5wJorKt2iTk52ed+pHptQuSyGM4Z7Qt4uTmBnt is+17ELpZC2cScKxpk5xxPRa/KKfYiH7x/iUOucLzd1iXZ5dL+9hRu/9VStx+z6W8Kp3lhKq S9FncPNtnALzxHc9s+HSuF7/ki/3TaP0xrf5f9ZLkApk6fQNp0vwqYom5YNrUjOGjX6lUb2g aOMaEko5+il5/76brjkopKRMZJ/hBvkPaQ0gMO/BPw1MggQUGif/uSxzLjj8lf4QLVOl/E2i qbZvI3DKcQVu6K0AQtY3pws6xa4CDem39AYkmcdIF1ZfxKHipDlO1DIIP/mEfeym0qgnCtvy vzcPbDsAo/BImbenLrhZ7px9kxRxQ4rwdBa/Z1UC7UBIPzpWk/2sdzVFgc5Mw2qzOb9EtVyy JkSVn6IAq+EKqPSrV6I6fwyI+SXa48VvSzyK/kh5/L0kXA5nlodcbGv3ZQMcH+4BOhpI12FY XrwhdcMCXoGshIkTOP2kF2CTSJTZ3GqUq0g4TE7EZuqApvHRoCwm7OMxzy7H51TZmBeEF+AC 3bod4OeW/cNci2eOMFhkiZXHYSmHoQmzFSlsBLw47thNOvdvCMC5rz5090g3+zejws/vRdzE t6B0myQBzVsn24SXTJw16diu1B8x0qr3q1xgvgeHttWsaAaGjwmPILRmrQpQ+v5XRjMK4/ho DeOR9ynBWt0Vdct25oUZE07Hdy+jxfF1i7sArkPlrXNCoZnurnE0S3XIMBwg23DyLFnl0MvF 9NOOHe8i+h08BXJG4/Ejm2Wkq+rceIX2yuevHybwz+2tVpDGBV1Tb2DWHkeYkXMqtGs/kLPV aWjT78gLxFdyMOfAqRPY9zty15BQaSrI8zQNkS2nWr4HhOU3vWMYY7tLn0axznYAVMYnho7+ H+HMU0mCX7krTuBXXphElXgZ06q+u57wJ+iZmkzyQzCL0ho1r7vvwUQmeTZUfQYmLQNpCYmr TxwWle7xdPfTdSa9UJne+1HbNUx7U0ityqRvhFhPpGmM6Fph0IPOwVxsUT00hxrC4JG2cE0p XIuxQB2JOqWylREPz+f2JnxPPXQJAyQtFi3aqPMwFyY29GL4LsO5ekQpFDqvQXvHU0nsj1m3 9RTz3qA98DSFgNBNPC5Gk0z9hV8u/Tbenxnv9KShSAqa/Dp9GadioFMZqNt0BurctZBPbnRE QbzF5dfHM2yMKkwnFPvaBsYPedU/apyPsW8dvLA1rT4WYQo1D+gk2lD55hwl0yW8C8pAPbJ0 owfzreT2RadSzbxkX+ut8n2ncZPYjRYTQ/dgWD0QZVcYKF/Z9NBEWajOde6gN55moTxWnNF3 FGmDlICnsSufFDBCj61lR0V3kMRr3u9nCK+xDEhiDAloJ2U2ynWyvjjfh4KUoJSbFFrlkykY Y29jtRAGVOtcxBsjhyuo0Dz26lcoq17aWjVW0ZBOSbsfSluVa65t7zKZMAqittgqSRaSv6xJ 1udV6ThohYH+yzmFmpagjs8cnmmt474kBpzlG+GZCwr/TyJJIcqnEqZvYONDfdKu1hODDF1k zzWGkSxM5Gy8NOYmo2C+uGyWmS9V4FCJCzizIeOriy+tggISVW0m/G+nMGiEBBvi3eqkYk3E 3+R8VClPdi4ssbyefhqdURpGlLmvs9zG4Uk15A1mIlVw38RwJOc4XsAl273d9Rdw6P3KnQXF ltpi5bY5hbo3Ep7IzeH3YX8Az+Fw8Z7fdT8aWQLwD484t1iB6Kd7bgClixw6Andz0qZcb1mk zERxOF7omYbjvsTtUwmyTiHHrEfAGFXOCXtk1KD6NX0/8A1LC6/NLO30kR5h9WoCrqP9xpdV HjOcZAnBSZs7897PQGEwDjp54rjYtWVccMLu0jejULbl+YMYsFU9LJClW99NGn6p3Fg1+Mrk Ukkw8ShpIbeY2R1oPDiX1gBZ2WzPZ9MvGmq1/oWn97Kjd7zWM86QXNSAsOuFbXxQVdw/bzmL 1rcTmN68y/BX+KZRUjFsA9nty6dTc7tbS3GYilBi40lHkHVJVQD0l9OGmxm2MdoTEbyg5WxF SUxrjEJugyn9l0VkL8ub1+nFT6B7AawNmVtEMjZdUUJqFEEvwCPaISf9r4hRn4DuMTw8ErVb DTcPlotbylBW1TYVQq7b//+uJ+ZqbjeXq3ncLPPeenc87UAEarYg8v+iM0+uG/dfsSXYis4V qN9gBESGysjXZyewmRqKWRfgSvJa4TzSA6U3Cpxo4j/9f3qXFiq/o6TE/5INt4p/RmqgKCFP urWhSBjKD8e2IlejXnPgKMS2lIfkUQMP3GkDKgAuCjRTanRhr4fDhgVbDl2PddJ6KR01xdEO MrSgNf4nrBiift9B1BAXF3n0sanAK5Ca3m6L0/CDV2XOa6uIDTKx4Tvbvr5R+QP3aNbsBq/v TvdGEjmf3yCmzTvSxGzILRMgSWcb3k88Mm2dhdgD3SmTcqzMEXqdo8qy2dvnPtt2SKZUAxUe SJxeE5MsLCKuCZRg/ElXndE8mIgN+6P3SCQ8+jfLJ8S9/ptGCV90exAsxFYg/NY6j9JQPttl W7ctNlr9hu+k+SV0DchWx1TsCpKiZ+jskBrOKGf/Z5FEyWhnlpF/SCLBhIGqsEwQMXooLxVw 8PTmbjbLT5D95fM8pJZCZGLeYSIN30uNRevEznRRlhgL3bjJSTUgEpTl+uX/3ueo80hq5Tir 5EJT6dSSF0/Ev5y4qtNE9kLIZMxVTQhw+fzZC8g4HO/qFzJS5wfsMmYB7SdBvLgLDvfhr5BN UNgKVbQIoEaN4m90EtnOAESoQ==
- Ironport-sdr: 652394bc_f4hK8bkVJ/HYK0FDo+fqYj6Ry01rH2jr+iySzfv8DdAHEWu sqaQHqfGeAe5r3OuMzi1SpgHcYr4BF+AL4ZYv3A==
The ereflexivity and other « e » variants of tactic have been made for this: these are tactics allowed to create *and instantiate* evars. Others can’t afaik.
Best regards
Pierre
Le lun. 2 oct. 2023 à 21:00, Abhishek Anand <abhishek.anand.iitg AT gmail.com> a écrit :
Lemma unifyIssue: exists x:nat, x=1%nat.
Proof using.
evar (y:nat). (* context now yas y:=?y*)
exists y.
Fail reflexivity.
Fail unify y 1.
subst y.
reflexivity.
Qed.Lemma unifyNoIssue: exists x:nat, x=1%nat.
Proof using.
set (y:=1%nat).
unfold y.
exists y.
reflexivity.
Qed.Is there a workaround for this?-- Abhishekhttp://www.cs.cornell.edu/~aa755/
- [Coq-Club] unification ignores local evar let bindings, Abhishek Anand, 10/02/2023
- Re: [Coq-Club] unification ignores local evar let bindings, Pierre Courtieu, 10/09/2023
Archive powered by MHonArc 2.6.19+.