coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] unification ignores local evar let bindings
- Date: Mon, 2 Oct 2023 14:59:15 -0400
- 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-wr1-f52.google.com
- Ironport-data: A9a23:hVfvBaP6A4WLuuzvrR3RksFynXyQoLVcMsEvi/4bfWQNrUom12QGn DAXXGGHOvzfN2CgL91+O4vn9k4G75CDyIBkHXM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8mk/vgqoPUUIbsIjp2SRJvVBAvgBdin/9RqoNziLBVOSvU0 T/Ji5OZYATNNwJcaDpOsPvb8Ek35pwehRtB1rAATaAT1LPhvyJNZH4vDfnZB2f1RIBSAtm7S 47rpF1u1j6xE78FU7tJo56jGqE4aua60Tum1hK6b5Ofbi1q/UTe5EqU2M00Mi+7gx3R9zx4J U4kWZaYEW/FNYWU8AgRvoUx/4iT8sSq9ZeeSUVTv/B/wGWddXng4vplU30xZ9Qao+l8O3NEq OMXfWVlghCr34pawZq+Q+how9s5dYzlYdlZtXZnwjXUS/0hRPgvQY2QvY4ejGp23JoXW6uED yYaQWIHgBDoahdPO0wXBZF4leGhgHW5cjxEp3qaoKM25y7YywkZPL3FaYCEIoPTH50K9qqej mXf0kHVOiEkD9mGmTrG73n2pe/kvwquDer+E5X9rJaGmma7zWsKTRYSSFGTuui8kkf4WtRFK kVS9DBGkEQp3EmiT924QAfh5XDZ5FgTXN1fF+B84waIokbJ3zuk6qE/ZmYpQLQbWAUeGVTGD 3fYxIu7Ni8lq7CPV3OW+5GdqD74a2BfLnYPaWVABUEJ6sXq6tN7xB/ebMdRIIjshP3MGBb03 2+rqgo6jO4tlsIl7fiw0m3GpDOOnaL3aDAJyD/ZZU+byz9oRZWEYtWo4GfL7PwbI4e+SEKAj Uc+mMOfzb4vCMiNnROSXOlWPaGN2MfcFTyBh1Q1Tp8r2AmwyiTyYaFR/zBMC0N7OekUeTLSQ RHyuCEAwLRxLXeVfatMTIbpMPsTzI/kDsbAesHPS9hzPqhKaw6M+R9xaX6q32zClFYmlYc9M 8y5dfmAIGk7C6M96haLXMYYjKEWwx4hyVPpRZzUywqt1ZycbiW3TZYHKF6/UfAr3piboQn68 8dtCOXS8k9xCNbBWyjw9ZIfCXsoLnJhXJD/lJFxR965ewFjHDksNu/VzbYfYLdapqVylNmZ2 lGmW0Rd9kjzum2fFyWOdUJYSe3OWbRRkCsFGBICbHeS9VotW4KN1JskVoAWeOAn/dNzzPQvQ Pgifd6BM8t1ST/G2mo8aJXhnbNmbzCuoxyEBAu+QT0FZ5U7bRf4ytzlWQrO9Sc1ESu8s/Ulk YCgzg/2RZkiRRxoKcTrNNaD6kyXhmdEvs5fRG7KLct3VGS21bN1OgrjivMTCOMdGyXpnze1+ V6fPkYFmLPrvYQwzujsuYmFiIWMSM5VAUtQGjjg34acbCX10DKq/t5dbbyuYzvYaWLT/Zeib 8Vzy9XXEqUOvHROgrpGP4db94AMzPqxmOYC1SVhJmvBUHqzALA5InWm49hGhpcQ+pBn4zmJS mC90fgEH4XRI870Mk8jFCx8ZMS56PwksD3z7/M0HUbE2BFK7Ie3CXt1AR3dpxFefZ1UMZwky 9gPoMQ5yRKyoTt0P8ekjhJ7zXWtLHsBYf9+tpglH5La0Fs361BdYK7zDj39z4GPZu5tbGgrA G6wr4jTi4tMwnHtdyIIKkHM+u5GlLIytwtv3nZbA3i0wv/+me4Q8DhK1DYGXiB5705g7bpoG 25JM0ZVG/2/zw1wjpIeY1H2ShBzOhKJ32fQlX4bn3L9ZGu1XDXvKGYdB768zHoB+TgBQgkBr aCq80e7YzPEZ8qr4zATX3RioPndTdBc0A3OtcSkPsadFakBfjvXrf6yVFUMtifYL5s9tG/fq clu2dRAW6nxGCoTgq88UoekjOVaDFjOIWFZWvhu8Z8YBWyWKnn4xTGKLFv3Yc9XYeDD9UijE cF1O8ZTTFKE2T2TqiwAT7s5S1OucCXFOPJZEl8qGYIHj1dbhj9gsZaV6TKnwWF2GZNhlsEyL o6XfDWHeoBVab24hEeVxPSo+ELhCTXHWOE49O+w+eQNUZkEtYmAtGksh6CssSz93BRPpnqpU cCqW0MS5+NnwIVo2YDrF82vwulyxczbDIy1zex4jziCgR4j/ysDW8P5Z2QL5zhrAIY=
- Ironport-hdrordr: A9a23:JPRUvqoC3oQzp5X5zB7orE4aV5omeYIsimQD101hICG9E/bo8P xG+c5w6faaskdzZJhNo7C90cq7IE80l6QFg7X5VI3KNGLbUQCTXeRfBOXZslnd8u7FmtK1F5 0MT0GzMrLN5JFB4/rH3A==
- Ironport-phdr: A9a23:4QyHQhdjGthw0af1hiFtCe4HlGM+nNvLVj580XJGo7dHc6D5uo/nI FSa//JmylnAQYTc7ftAzevQqaHpH2Iast6aqH5XVptKWlcejNkO2RQ6CZuMA036N/7nbGozG s1EWBlk/m20GUdQEcf6IVbVpy769iYcTy32LhE9PeHpAsjXhsWz2fq1/sjaaQVJnzqwYvV7K hywoUPQt9UZqYRnI6c1jBDOpygAYPxYkEVvI1/bhBPg/oGw8ZpkpjxXoO4k/tVcXL/Seq05S flHFm1jPT1vosLsshbHQE2E4X50vnw+tB1ODkCF6Rj7Ws20qS7mrq9n3yLcO8TqTLcyUDDk7 qFxSRauhj1Vfzg+uHrajMB9lsc56FqougB/zojIYYqUKOs2f6XTeskfTHZAWcAZXjJIA4e1Z Y8CR+QbOuMQo474rloI5RywYGvkTOrlyj5ThnL1m6Q82uItVwDHwAMIENcHsXCSp9Lwde8TX e2z0KjU3GDbdfoFvFW1oIPMcx0nvbSNRecqKZuXmRRpTVmcyAjK+umHd3uP2+8AsnaW9b9lX OOr0Ss8rh1p5yKozYEqg5XIgYQczhbF8z94ycA7P47dKgYzbNi6HZ9XryzfOZFxR5ZoSmtou T06x75AsJiyeiRMyZU7yDbQbvWGd86D5RepB4PzaX9owWlofr6ynUP4+EKgy/b8W8ry2VBDq CYDk9jQuVgC0hXS7o6MTf43rSLDkX6fkgvU7O9DO0U9k6HWfoUgzrAHnZ0WqU3fHyXylS0al Yeuf14/sqit4uXjOPD9o4OEcpVzgUf4O7gvncq2BaI5NBIPVi6V47b02Lrm9Ez/CLJE659+2 qDTsJHBJckY4Ke/CglZlIci9xmXADKv0dBeln4CZF5IYxOIiYH1NkqGeqipS6fixQ72yXE2n bjPJdiDSt3VI2LGkav9cLo18ENaxAcpjJhe659SFrAdMaf2U071usbfC0xxOAi1zuD7TdRlg 9lGCCTfX+nDavqU7AXbg4Bna/OBb4IUpjvnfv0s5vq0yGQ8hUdYZ66im50edHG/GP1iZUSfe 3vlxNkbQgJo9kIzSvLnjFqaXHtdfXG3Cug17DE6E4KrDsHKQImrjPqA3Tu0NpJTb2FCTFuLF D27EufME+dJcy+ULsJ7x3YNX7igUI8s1lensgb8x/xmL/bb0iIdvJPnktNy4qeA8HN6vSwxB MOb3WaXSmhylW5dXD460pd0pkllw0uC26x10LRIUMZe7PRTXkImJIbRmqZkXsvqVFuLLbLrA B62B8+rCjYrQpctzs8SNgxjTs66gEmL3jL2UeRI0eXaXNpurv2ahz+re4580yqUivVn1QJ9B JIRbSv+wfcukmqbT4/RzxfHyeDzLf5ahGiVsz3bhWuW4BMGDkgqDfSDDShZPgyM9Zz4/h+QE OXoUOhha1obj5bFc/svCJWhjE0aFqi/fo2EPiTp3T/3XEjAx6vQPtOyKyNEg3qbWA5c1FpKt XeeaVpnWXzn+jOCSmQoTRW2PSaOuaF/sC/pFBdliVHXKRQ7h/ztvUdKzf2EF6FJh+xC5Xdn8 mQuWg76hoOeCsLc9VA4IuMGOoJ7uw0BjSWA5mkfdtS2JqRmzDbyaixRuEXjn1VyA4REy40xq W8yiRB1IuSe2U9AcDWR2dbxPKfWIy/85kLnbamewVzY3NuMn8VHoP0lt1Xuuh2oHUs+4j1m1 ddSyX6V+pTNCkIbT5vwVk898xUyqavdZ2Ex4Ibd1HskNqfR0HeKw9UyGO4s0QqtZf9aOaKAU RDoSogUWpLoJ+stlFykKBkDOaEa9aI5Od+na+rT2KOvO7UF/nruhmBG7YZhl0OUonAkG6iYg tBfmajeg1HUMlW0xE2suc32h41eMDQbH27ljDPhGJYUfKp5O4ACFWapJcSzgNR4nZ/kHXBCp zvBTxsL3tGkfR2KYhnzxwpVgA4eq3ymgiu1zHp9lTgvouye3TDB6+vnfRsDfGVMQSMx6DWka ZjxlN0cUEWyOkIxkwC54E/h26VBjKF2Lm2WXl0ROiardSdtVay/srfEaMlKosBN020fQKG3Z laUTaT4qh0R3nb4HmdQ8zs8cimjppTzmxESYIO1KX9yqD/GY5g1y0qFotPbQvFV03wNQywq0 VE/43CzOtCo+ZOfkJKR6ohWuEquU5RSdW/gyobS7UOG
- Ironport-sdr: 651b1330_5orQoaH9tOhZ5vnnTGTXHD3TqCd6NKH20+MwgFlvmaCP0Z1 aVtwOn17oqm7t3OhO1zumt8Ofc3YMr/iUR3TyAw==
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.
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.
Proof using.
set (y:=1%nat).
unfold y.
exists y.
reflexivity.
Qed.
Is there a workaround for this?
-- Abhishek
http://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+.