coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Abhishek Anand <aa755 AT pm.me>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] rewrite clears hypotheses in evar's context
- Date: Tue, 11 Oct 2022 03:03:26 +0000
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=aa755 AT pm.me; spf=Pass smtp.mailfrom=aa755 AT pm.me; spf=Pass smtp.helo=postmaster AT mail-4322.protonmail.ch
- Feedback-id: 39498114:user:proton
- Ironport-data: A9a23:k9aNDa/qLz06jLb8iUHWDrUDhXqTJUtcMsCJ2f8bNWPcYEJGY0x3x 2AeCz2FM6neNmX8LtB1bdm3pEoBvJOBxtdrGwU5+CxEQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHPykYAL9EngZbRd+Tys8gg5Ulec8g4p56fC0GArlV ena+qUzA3f4nW8pWo4ow/jb8kk25K2r4GpwUmEWPJingneOzxH5M7pEfcldH1OgKqFIE+izQ fr0zb3R1gs1KD9wYj8Nuu+TnnwiGtY+DyDW4pZlc/TKbix5m8AH+v1T2Mzwxqtgo27hc9hZk L2hvHErIOsjFvWkdO81C3G0H8ziVEFL0OevHJSxjSCc5xL8S3Lv2u0xMFsVGogYy/tOI2Bs2 +NNfVjhbjjb7w636LeyS+0p2p95do/zJoQDvXdlxDDdS/0mKXzBa/yauJkHhHFs3YYUR54yZ OJBAdZrRB3JPEASEk8STpcz9AutriOhL2QG8AjNzUYxy3X0wVFviOnECt3uQtGUe9gPn3qVu UuTqgwVBTlBaIzEl2vUmp62vcfEmjq+U4YPHpWj5/tyiRuSwHYSAVsYTzOGTeKRj0e/X5cDc BZOvDI0qrQ18kmiT927VB3QTGO4UgA0BOBoGu4j8F6x0Inz5gaoG1EmTxxvd4lz3CMpfgAC2 liMltLvIDVgtryJVH6Qnot4SxvsY0D5ykdcP0c5oRs5D8rL/N5q0k6eJjp3OP7s04Ctcd3l6 2nS9EADa6MvYdkj/IXTwLwqqzelp5yMElVvvEPPRGW56QV8bY+hIYeogbQ60RqiBNjJJrVil CJe8yR70AzoJc3c/MBqaLlddIxFH97fbFXhbadHRvHNDQiF9X+5Zpx36zpjPkpvOctsUWa3P hKP410Pv8YJYyHCgUpLj2SZVZ5CIU/IS46NaxwoRoMmjmVZLlTfoEmCm2bBjggBb3TAYYlkZ cfAL5f9ZZrrIbx9yyaxQa8U3tcWKtMWmwvuqWTA503/i9K2PSfNIZ9caQfmRr1nsMus/VuEm /4BbJDi40sED4XDjtz/rNd7waYidydnXPgbaqV/K4a+H+aRMDh4W6WMn+58ItANcmY8vr6gw 0xRk3RwkDLX7UAr4y3RApy6QOOxA8RMvjggMDYyPF2l/XEmbMz9pO0cbpY7N/1vvuBq0fc+H bFPdtSiE8Z/bG3N2w0cSp3h861kVhCg3jyVMwSfPTMQQp9HRi7ywOHCQDfBzic1IxCMhZMMm IH4jgL/argfdjtmF/fTOa6OzUvunH0zm9BSfkrvI/tMcn6x7LpRCjfQi8UvKJomMiTzxTq91 ieXDywHpOLLnZQHzdnRiY2ArKarC+FbHHcGL1LE7L2zCzbWzlCjzaBETuyMWzLXD0Hwx4mPe sRXyKvaHMAcvVMXrbd5Laln/Zg+6/TrubVe6AZuR1fPTlazD4JfMmu05tZOuoJN141ml1OPA GzXweZjOJKNJM/BO3wSLlB8bu28iNclqgOL5vExeEjH9Ct7+YScanprPj6Otn15DKB0O4Yb0 +seqJYoywiguCELbPeCrA5prlqpEFJRcp8apqk7AZDqgDUF0lttQ4LRIQ6o7YCta+djCFgLI DiVjpXsn753nhLnYVsiMX7nzOAGv4oEvUlKxWAdOmXTldvhrd001S137j4YYFl0zBJG8uQrI UltFRR/Cpuv9gdSpvpofj6TCSAYIzaGo2rd5Vctv0/IfXmCD2DiAjU0BreQwRo/7WlZQAl+w JiZ72TUCRDRY8D723oJa35P8vDMY4R4yVzfpZqBAc+AIpgdZAjliI+IYU4jiUPuIeE1tX39i dhaxsRCQoylCndIuIw+MZeQ6poIQhPdJGBif+BozJlUIU7iIgONyRq8AGHvXPMVPPHb016KO +o3LOJ1ahmO/iKvrDcaOK0yH4FJjMMZvOQlRLe6ClMF4p2+ryVouq3+7iLRpnEmaPQwnNcfK rH+TSOjEGuRjlQMhmXykchgEUi7aOkiewfT8r2U8uIINpRbq8BqUxg4/YWVtkWvEjlM3kyrr iKaQIGO1M1k64Bnv7W0I5V5Hw/udO/CDrWZwj68o/FlTI3pM/6Xkyg3t1O+HQBdHYVJauRNj b7X7eLGhhLUjo0XDVLctYKKTZRSxMOIW+FSDML7AV9akQaGW+7u+xEzwH+5G7MYjOJi4tSbe CXgZPuSbdI1X/Jv9E9RYQVaEDcfDP35UP6x72f15fGBEQMU3gH7Pcuqvy2hJ31ScigTfYbyE EnosvKp/cpVt5lIGARCPfx9HptkOxX2bMPKrTEqWeWwVQFEQ29uu4cOUTIl4DDPTyXfSpy8+ YjCWh/4cR2zvOfDzLm1dqRs6wYPAi8VbfYYJyogFxxe0lhWz1Lq6cwFNNMDB/m4VwTsgYrga milgHQKUE3AsPctTfk4yMzmGAKSbgDL1hEVORRxl36ph+yK6E9szVevGuqMI5u7R9c78NyaF A==
- Ironport-hdrordr: A9a23:jatqe67Es1GRSO7KZAPXwNHXdLJyesId70hD6qkRc203TiX8ra qTdZsgviMc9wxxZJhNo7y90cq7IU80l6Qa3WB5B97LYOCMggSVxe9ZgLff/w==
- Ironport-phdr: A9a23:6Bu/Pxc5V2Z8/hzHVVRTWLj7lGM+VNXLVj580XLHo4xHfqnrxZn+J kuXvawr0AWSG96Etrka0KL/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQF cVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHNbQhEnjSwbLFyI Rm5rAjcuNQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2U bJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5 KptVRTmijoINyQh/W/ZlMJ+jL9VrhGuqBNj2IPbep2ZOeBkc6/BYd8XR2xMVdtRWSxbBYO8a pMCAvYaMuZYron9vFsOogW9BQKxGO7vzCVHhnnr0qYn1OkuCxvJ0Q4gEt8Oq3nUtND1OL0XU e+r1aTFyyjIYPxK1znn8ofIbgwhru+WXbJ2acfd10khGQPEg1iRtYDpIjKY2voJvmaU7OdtV OKhhmo7pg1srTaiyNsgh5XHiI8XyV3J9St0zYk3KNGlSEB2Y9CqHZ1NvC+UMIt2R9ktQ2Buu Csixb0GuIK7fCgXyJs83RLQd/uHc42O7xn+V+iROS91iG9mdb+/nRq/81SsxvfzW8S6ylpGs DRJn9/RvX4XzRPT8NKISv5l80ehxzmP0wfT5/lBIU8ulKrbL4ctz7E+m5YNr0jPBDf2mF/xj K+KcUUk/O2o5P7mYrXivJOTK490hhn/MqQohMO/Hfw1PhUNUmWb4+ix1qHv8Vf2TbhElPE6j LfVvIjfJcsBp665BwFV0pwk6xa6Fzqpys4XkHsHIV9FYx+Hl43pN0vLIP/mFfu/hU+jny9xx //aJr3hHonNLn/bnbv8Zbp98VJTyBIvzdBD4JJZEq0OIPXqWkPoqNPYCgI5PBevzub8CNR90 5seVniVDq+YNqPSq16I6fg1L+mCfo9G8Ar6fvMi/rvliWIz0QsWerDs1p8KYli5GO5nKgOXe yy/rM0GFDIjtAo/V+znixWrVzdVaz7mVqtju2wTEIfgCIqVFdPlu6CIwCruRs4eXWtBEF3ZS R8AFq2BUvYIM2eJJ9N51ycDTf6nQpMg0hensEn7zaBmJ6za4H5Qrortgf5y4eCbjhQu7XpsF c3I2mjSEjxchmZOQjJllLtnrxlFw0yYmbN9n+QeENVS4/1TVQJvPJeDkrFSE9W0Xw+SNsyRR gOeS869SSo0Usp3w9IKZBNlHM6+ixnYwyewK7oclrjOWMduqOTExX/tIMB4wnfCkqIh57U/a u1IM2Duxqt29gyIQpXMj13cjKGyM6IVwC/K8m6Hi2uIpkBRFgBqA+3DWjgEa03aoM6chAuKR qKyCbkhLgpKyNKTYqpMZNrziFxaRfDlcN3AamO1km20CF6G3LSJJIbtfmwc2m3aBi1m20ga9 CnbaCAmA2GkriOWDTBjE07uf1K56fN3+zuwSk45yR3PblU0jurovEFNw6DHDalJjddm8G87p j55HUiwxYfTAtuE/E96eblEJMg6+BFB3H7YsAp0OtqhKbpjjxgQaVcS3Qum2hNpB4FHicVvo mktyV84IKvHjQ5pbzbe2J26afXHb3L/+hyicfuc01iBjYu+4qJJ7fly+DCB9Em5U0El9Xtgy dxc1XCRs47LAAQlWpX0Sk8r9hJ+qtk2ewEF7pjPnT1pOKiw6XrZ3s4xQfAi0lCmdsteN6WNE EnzFdcbDo6gMr5il1+sZxMCdOdckcx8d8qvKKbb8LaueuNt1D6rlmVI5olh31nErnohDLGQm cpehavClgKcHy/xllKgrtz6lchfaDceE3D+rEqsTI9da6tufJoaXGKnIsm53NJ71NbmX39V8 kLmBktTgZ/0P0XKKQCmm1cKhiF16TS9lCC1ziJ5iWQsp6ubh2nVxvj6MQEAIihNTXVjilHlJ c61icobVQ6mdVtM9lPt6EDkyqxcvKk6IXPURBICdiGpcjxKSq72s7fIMIZfrYgltylaSrH2a FnFF+PVux5c1i6pTA48jHgrMjqtvJv+hRlzjmmQeW1yoHTucsZ13R7D5dbYSK0Zzn8cSSJ/k zWSGkmkMozj44CPj5ma+LPbNSrpRthJfCLs14/FqCar+TggH0ikh/7q0tz/TVpjgXK9iIEsC X2O9FGmPsHqz/joaLI6OBYwQgOlrZI9QN0b8MN4hYlMiyFK29PKpTxbyiGrdo8HkaP4Z34QS TNZ9MXN7lKjwFdkMnWPwov4UjOWwoN3bt2+KAv6wwoF5ttRQOeR5b1Axm5up0ag6BnWeb57l ysczv0n7DgbhfsIsUwj1HfVDrcXFEhedSvi8nbAp8i5t7lSbX2zfKKY0UN/mZX9V+vY5BlGX 2r+fJIrHCs25cU3PF/X0XL1453pY5GJPY9V6UXSz0yG1bIdIYlU9LJCnSd9PGPhoXApg/U2i xBjx9DyvYSKLXls4LPsAhNcMW69bMcS9zfxyKdGy5/GgsbwRtM9QXNRBsiNL7rgCj8ZuPX5O hzbFTQ9rizeAr/DBUqE718gqXvTEpetPnXRJX8DzNwkSgPOQS4XyA0SQjg+mYY0Uw6ww8m0O k5wuW1Mzkb97B5BgLENVVG3QiLEqQGkZy1hAoCYNwZT5xpe6l39NMWf6qcvRHsCuIW7qxCKL GmSZgAOBmFDCSnmTxjze7Kp49fH6e2RAOGzeuDPbbu5outbT/6UxJir39gu73OWO86IJHUnE +wj1x8JQyViA8qA0WZqKWRfh2fXYsWcvhv55iBnspX17qHwQAy2rYqXV+kLYYgppEjw3fzFb bTYki99LXwwPnwk3XqOzbVNhTb6aglrfjipVOhb73SLVLjXhqhRChcab2V4NJkRh0rZ9hFIf 8vW2Iud6w==
- Ironport-sdr: 6344dd04_9ZvzcnsLYUesm1zyADq4uMg/q2KgjYt2YMW65J5LydAKKNr axpCB2ZiVShNB8i+EXeU43x5UuiO1O68fQ9FAhw==
As shown in the lemma test1 here (https://gist.github.com/aa755/1ebc84dc22108fecccfe1ceedb33066e),
rewriting in a hypothesis that existed when an evar was created results in the deletion of that hypothesis from the context of that evar.
More surprisingly, this happens even when the rewrite uses a definitional equation, as shown in the lemma test2 in the page linked above.
In this case, it seems trivial for Coq to not clear the hypothesis.
Even when the rewrite is with a non-definitional equality, can Coq not insert
eq_rect
at appropriate places to avoid dropping the hypothesis from the context of the evar?--
Abhishek Anand
- [Coq-Club] rewrite clears hypotheses in evar's context, Abhishek Anand, 10/11/2022
- Re: [Coq-Club] rewrite clears hypotheses in evar's context, Samuel Gruetter, 10/11/2022
Archive powered by MHonArc 2.6.19+.