coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Non obvious recursion (Issue with Function + Can't unfold Program Fixpoint)

From: Jim Fehrle <jim.fehrle AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Non obvious recursion (Issue with Function + Can't unfold Program Fixpoint)
Date: Sat, 2 Sep 2023 12:12:18 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jim.fehrle AT gmail.com; spf=Pass smtp.mailfrom=jim.fehrle AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf1-f50.google.com
Ironport-data: A9a23:sTC9NKyYF9apfQkp3Sx6t+dawyrEfRIJ4+MujC+fZmUNrF6WrkVSy 2QYDDjVPP7YZjHwf4pwa4Tk/E0AsMLdzIc2GgU6q1hgHilAwSbnLYTAfx2oZ0t+DeWaERk5t 51GAjXkBJppJpMJjk71atANlVEliefSAOCU5NfsYkhZXRVjRDoqlSVtkus4hp8AqdWiCmthg /uryyHkEAHjg2Qc3l48sfrZ80s+5K6q4lv0g3RnDRx1lA+G/5UqJMlHTU2BByOQapVZGOe8W 9HCwNmRlo8O10pF5nuNy94XQ2VSKlLgFVDmZkl+B8BOtiN/Shkaic7XAhazhXB/0F1ll/gpo DlEWAfZpQ0BZsUgk8xFO/VU/r0X0QSrN9YrLFDm2fF/wXEqfFPF6elNJ1ARPLQRufluCHBX3 M4nKB0CO0Xra+KemNpXS8Fpj8Unac3lZcYR5ykmwjbeAvIrB5vERs0m5/cChGZ21p0IRKiBI ZdBAdZsREyojxlnOFYSTpwznP2si1HwdjRZrBSeoq9fD237lVYtiOO2bIeNEjCMbdxvmh/Eg Vrrw3/wLgw/DNO742e1+1v504cjmgu+Aur+DoaQ/flzxVaX22Y7EwwTTVL9oP+ji0f4Vcg3F qAP0i8nrKx38ELyC9egB1u3p3mLuhNaUN1VewEn1DywJmPvy17xLgA5ovRpMbTKbednHmR45 UzDhN7zGz1kvZucTH/XpP/eriq/NWJRZSUObDMNB1lNqdTygpABvjSWRPZaEYmxkoLUHxP0y Gu0tyQQvegYovMK8KSZxmr5pQyQiKLHdSMLwznGf3mE61p5bbG1Zobz5ln86+1BHbmjTVKAn SYlnpGe5d8REZuipTypf9RUOZr04fzfYTvWrmNyLsNw6xWs5H+RUoRC6x5uJEpSE5gleB24R GTxqA9u9JtoE3/yVpBOYqW1ENYP4Zn7MNbYCsDvcdtFZ6ZueD+9/C1BYVCa20bvmhMOlZ4TF Ii6c8H2K1onEoVikSSLQtkC3Y8RxiwRwX3ZQbb5xU+F1ZucfHukdqcXAmCRb+wW7LK2nyuNy oxxb/C18hR4VPHyRgL18oRJdFADEiUdNKDM8sdScraOHxpiFGQfEMTu+LIGebI0u4ROl+zNw GOxZV8A9nr7mk/8CFurblJNVerReKhR/FwHOR4iB1KK40QYQJ2O6f4ffqQnfLN8++1Ey+V1f sY/eM6BI6puTzjbygsZdr34ipJoTzWwpAe0JyH+SiMOT51hYA3o+9HfYQrk8hcVPBe3rccTp 76B1BvRZJg+GyBOKdnwU+326X+cpl0fl/BWc2qSB+JMaWP+9IROAA7gvM8des0jB03K+WqH6 lywHxwdm9jon6Y019vs3oWvsIajFrpFLHpwRmX0w+6/CnjHwzCF34RFbeeveALdXkPS/IGJR 71c79P4Ac09sGd6iahOOJc18vtm/PrqnaFQ8Sp8FnaSb1iLNKJpEkPb4eZx7J9y1p1rkirof HLX4dRLG6S7COW8Gn4rGQcVROCi1/YVpzrs0coIMHjKvC9awb7WfnhRbj+tiTNcJoRbKIkK4 /ksk+9I5h2diigFCMenjCdVxT7VLnU/TLgW7MAGIY70izgEzkNJTozcBxTXvrCOSYRoGWs7L gCEgJHtg+xn+XPDVH4oBF7x0vF4l71XnDx3lHo5OEWutv/eo/0GzDl90G8QcFxO7xNl1+lTB DBaB3dtL//TwwYy1dlxYW+8PipgWjiL8VPV4HkUnjT7S0KIaDT8HFclM7zQwHFDonNuRRkFz rS2022/bC3Levv21S4MWUJIjfzvYNhy1w/akvCcAMW3MMgmUAXhn5ORSzIEmzn/DeM1oX/3l +1g0eJzSK/8bCAu+vxxT8HQ0LkLUxmLKVBTWfwrrutDAWjYfyr0wjSUbVy4fsRWPfHR7EukE IpUK9lSUwilnjO7xtzB6XXg/5cv9BLo2DYDRl8vDWsPsr/aqjQw9ZyNrm7xg2gkR9gomsE4Q m8Um/RuDUTI7Ua4WUeUxCWHBoZ8SdYBbQz4muuy9Y3l0rod5fp0fxhaPqSc5h2o3cgOw/5Ql AzGbq7SiedlzOyAWmcq/rprX22JFD84aAhEHM1ffTiDgRMj/Poibz8ol2Q=
Ironport-hdrordr: A9a23:UGE9V61VvaBeuOi/Cn2JgQqjBIskLtp133Aq2lEZdPU1SL3gqy nKpp4mPHDP+VMssR0b6LK90ey7MBDhHP1OgLX5X43SODUO0VHAROpfBMnZowEIcBeOkdK1u5 0QFZSWy+edMbG5t6vHCcWDfOrICePozJyV
Ironport-phdr: A9a23:VJQW4xYgLnUN/BmIG+ZhpJv/LTFi2oqcDmcuAnoPtbtCf+yZ8oj4O wSHvLMx1gGPBNmHoKsf1qL/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQF cVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHNYghEniexbLx9I Rm5sAncuMkbipZ+J6gszRfEvmFGcPlMy2NyIlKTkRf85sOu85Nm7i9dpfEv+dNeXKvjZ6g3Q qBWAzogM2Au+c3krgLDQheV5nsdSWoZjBxFCBXY4R7gX5fxtiz6tvdh2CSfIMb7Q6w4VSik4 qx2ThLjlSUJOCMj8GzPhcNwgqBUrhKvqRJ83oDafp2aOeFkca/BZ94XX3ZNUtpTWiFHH4iyb 5EPD+0EPetAq4f9pl4Opga+CwayBOPv0DtIiWHr1qA90eQhEATG0BYuH90QsHTUttH1O7kJX OC6yanH1zTDb/dM1Tjh74jIdwksrPeRVr1/bcTf01MgFx/ZjlqOs4zlOSuY2/gOvmWF6+dtW uOihmolpg1tvDWhyMMhhpXVi48R1lzJ9Ct0zYcrKNCmVEJ2ZdqpHZlfui+UKoZ4Td4vTn90t Cs817YIuoa7cTAUxJg7wxPTcf+KfoiS7h7+VeucIy10iXJ5dL+5mh2861KvyvfmWcmxyFtKr jRKkt3Ltn0V0hzc8MmHSv9k8kel1zaDyhnf6u9ELEwoj6bbJJkhwrk/lpoXr0vPBDP5mELzj KOOd0Uk/Pan6/j/b7n4upORM5V4hwL+P6g0h8CyAOY1PhIOUmSH4ei80afs/Uz9QLVElP02l azZvYjYJcQao661GQFV3Zgj6xalCzepzs8VnXYCLF1feRKHi5LlNE3JIPD9Ffu/hU+jny9xx //aJr3hHonNLn/bnbv8Zbp98VJTyBIvzdBD4JJZEq0OIPXqWkPoqNPYCgI5PBevzub8CNR90 5seVniVDq+YNqPSq16I6fg1L+mCfo9G8Ar6fvMi/rvliWIzsV4bZ6igm5UNO16iGfEzAUScK VThgs0FHC9evAs7CuLniEeGXBZcYn+zW+Q34TRtW9HuNpvKWo342O/J5yy8BJADPgiua3iJG HbsLcCfXusULTiVKYlnmyAFUr6oT8kg0wuvvUn00ekvNfLarwsfs5+rz91p/6vLjxhn9z1xS cqQ03uJQkl7m2oJQ3k926Us6VdlxAK72LNjy+ddCcQV4vpIVgkgMpuJze1/Td7/WhjFc/+GT V+nRpOtBjRiBskpzYooZEBwU86nkgiF3yeuBOoNkKeXAZUv7q/G9334JsI4z3ifkad81x8pR cxAMWDgjal6n+TKL6jOlUjR16OjdKBGmTXI6H/G122F+kdRTA93V6zBG3EZfErf69rjtAvES Pe1BLIrPxEkq4bKI7ZWatDvkVRNRevycNXYbWWrnm6sBBGOjrqSZYvucm8Z0W3TEk8B2wwU+ H+HM0A5CELD6yrcDTkoG1/veUfh2eZ7oXK/CEQzykDCbkFs0aa05g9AneaVGLsY2rMJvjtkq i0hRg7smYKLTYPe+Ew8JPY5A5t1+lpM2GPHuhYoO5WhK/onnVsCa0FtuEio0RxrC4JGmMxsr XUwzQM0J7jLtTEJPz6ew530PaXab2fo+xX6IazX3xfQ3daM/qon5/ExqlGltwasXBlHkT0vw 5xO3n2Q64+fRggTVNT/X0Yt8xVSqLTTYy177ITRny4JU+H8onrJ3NQnA/EgwxCrcoJEMa+KI wT1FtUTG8mkLOFCd0GBVhsfJ6gS8ac1O5njbP6awOuxO+0mmju6jGNB6YQ700SW9iM6RPSal 5oCxviZ2EOAWVKexB+js8Wxl41EfzUfNmW6wCngQoVWY+V+cJ0KBmGnP8Csjo8m1ti9BjgBq gHlWgtO0dThYReIal3hwQBcsCZf6Weqnye11X08kj0kqLaewD2bxu3jcBQdPWsYDGJmjFrqP c21l4VABBnuP1VvzUX6oxuilM057OxlImLeQFlFZX3zJmBmCO6rs6aaJtRI49UuuDlWV+K1Z RabTKT8ql0UyXCGfSMWyTYlejWtopi8kQZ9jTfXLnd26nTUedt0yD/Q4dXdQbha2T9MF0waw XHHQ0OxOdWk54DelZbG9O6zV3ilW7VcdCDqycWLsy7xtggISVWv2vu0nNPgCw0z1yT2gsJrW Sv/pxH5eoD31q6+PLEvbgxyCVT78cY/BpBmn956msQLwXZDzMbwnzJPgSLpPN5cw667cHcdW WtB3YvO+Aa8kEx7ciDSmsSgBy3bmJc+IYH9OD9e2zphvZ4WTv3Pt/odw3Mz+h3h/GezKbB8h mtPl6VosSZAxblP4E13lm2cGuxAQxceZ3C90UTQqYj59v0fZX7zI+fqkhMi24nwVvfa5VgMP RSxMpY6QX0vsoMmag+KiDurrdi6MNjIMYBK7k3SykifybgTcNVrz7ILnXY1YD2m+yR0l6hjy 0QphM/f3sDPKn0xrvjhU1gIa3usPZNVona00u5fhprEhdnxWMgxXGxaBt2wCqv5WDMK6aa9b ljISmZt7CzBX+KYRF76ig8uuXvLF9rD22i/An4fwJ0iQRCcIBYamwUIRHAgmZV/EAm2xcvne UM/5zYL51e+pAEeguRvfwLyVGvSvmLKIn89VYSfIRxK7wpD+1adMMqQ6fh2Fj1Z+ZvppRKEK 2iSbQBFRW8TXUnMC1fmN7iord7OlorQTvK5NOfLaK6SpPZ2Uv6Jwder3NIj8WvUcMqIOXZmA rsw3U8CFXF1FsLFmikeHiwakyWeCqzT7By4+yBxsoW+6KGxAFOptdbJUuUNd4g3qHXUye+ZO uWdhTh0M2Nd35IInzrTzaQHmUQVgGdofiWsFrIJsWjMSrjRk+lZFU1+CWs7Oc1W4qY7xgQIN 9Tcj4a/1L99yPA4C01BWHTun8ioYYoBJGT3ZzalTA6bca+LIzHG2ZS9eaSnVbhZl/lZrTW1s DefVkvtZ3GNymGvWBeoPuVByiqcOVYN3eP1OgYoAm/lQtX8bxS9O9Iiljw6z4o/gXbSPHIdO zxxG6uohrKV5CJcxP54Hj4ZhpKEBeyNmiLc6+eBb5hL6b1kBSN7k+8c63M/meM9BM5sS/l8m S+Updlr8QjOrw==
Ironport-sdr: 64f38928_iIBLlCrFdKRYU3eeLir8vj93IuN4WKJSWdusyydf+Ghrsvq cG6G1swrgGJG9SKOERvfCDuRZykdfsQr2+tCVgA==

IIUC, rather than maintaining Qed/Defined versions of each proof in the standard library, wouldn't it be better/simpler if the Transparent command could change existing proofs to be transparent?

[Coq-Club] Non obvious recursion (Issue with Function + Can't unfold Program Fixpoint), Agnishom Chattopadhyay, 09/02/2023
- Re: [Coq-Club] Non obvious recursion (Issue with Function + Can't unfold Program Fixpoint), Wendlasida Ouedraogo, 09/02/2023
- Re: [Coq-Club] Non obvious recursion (Issue with Function + Can't unfold Program Fixpoint), mukesh tiwari, 09/02/2023
- Re: [Coq-Club] Non obvious recursion (Issue with Function + Can't unfold Program Fixpoint), Castéran Pierre, 09/02/2023
  - Re: [Coq-Club] Non obvious recursion (Issue with Function + Can't unfold Program Fixpoint), mukesh tiwari, 09/02/2023
    - Re: [Coq-Club] Non obvious recursion (Issue with Function + Can't unfold Program Fixpoint), Dominique Larchey-Wendling, 09/02/2023
      - Re: [Coq-Club] Non obvious recursion (Issue with Function + Can't unfold Program Fixpoint), mukesh tiwari, 09/02/2023
        
        Re: [Coq-Club] Non obvious recursion (Issue with Function + Can't unfold Program Fixpoint), mukesh tiwari, 09/02/2023
        
        Re: [Coq-Club] Non obvious recursion (Issue with Function + Can't unfold Program Fixpoint), Jim Fehrle, 09/02/2023
        
        Re: [Coq-Club] Non obvious recursion (Issue with Function + Can't unfold Program Fixpoint), Agnishom Chattopadhyay, 09/03/2023
        
        Re: [Coq-Club] Non obvious recursion (Issue with Function + Can't unfold Program Fixpoint), Meven Lennon-Bertrand, 09/04/2023