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: Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Non obvious recursion (Issue with Function + Can't unfold Program Fixpoint)
Date: Sun, 3 Sep 2023 10:54:47 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=agnishom AT cmi.ac.in; spf=Pass smtp.mailfrom=agnishom AT cmi.ac.in; spf=None smtp.helo=postmaster AT mail.cmi.ac.in
Ironport-data: A9a23:odRwxKIeNyKMOks3FE+RWJMlxSXFcZb7ZxGr2PjKsXjdYENSgjcPz DRNXT+HPfaINjf8KYp+b4yx/UJSsZeHzodhT1cd+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t 63yTvGacajYm1eF/k/F3oDJ9CU6j+fSLlbFILasEjhrQgN5QzsWhxtmmuoo6qZlmtHR7zml4 LsemOWBfgf/s9JIGjhMsfnb+Us05K2aVA4w5zTSW9gb5DcyqFFOVPrzFYnpR1PkT49dGPKNR uqr5NlVKUuEl/uFIorNfofTKiXmcJaKVeS9oiY+t5yZv/R3jndaPpDXmxYrQRw/Zz2hx7idw TjW3HC6YV9B0qbkwIzxX/TEes3X0GIvFLLveBCCXcKvI0Lua1jy3ftOUlMME9dI2OR1LWBq3 84BAWVYBvyDr7reLLOTT+BtgoIoKcitNYhZu3cIITPxVKx9B86YBf+SvpkChW1YasNmRZ4yY +IQZjxudxTHZjVEP1ZRAZl4neHAanzXKmcE8A3F+fJti4TV5DZIj+bmLIX/Ro2XRZVkpkyTj F33w3usV3n2M/Tak1Jp6EmEjejW2Cj/RYg6D6y97vcsgVuJx2VVBgd+aLegifywi0r4UNdeb UUfvCsoxUQvyHGWohDGd0XQiBa5UtQ0ALK8ysVqtl/f+bme+AuDGGkPQxhIbdFs5od8RiUn2 hXN15nlDCBm+u/dA3+M1KamnRXrMwgsLEgGeXAlSykB6ILdu40dtE/EYetiN6+XtefLPw/M7 QqElwUAookCrNUq0vy79G/Xgjj3qZnuSBU01zrtXWmkz11YYdelbrO39GmBtO5kKaibalyFo VkFhMmsw+QcBr6dlCG2YbssHZP4w92nITHjkVpUMJ15zAuU+lmnZpJ1zAhlAUVUbvY/Zj7iZ XHMtTNr5JN8OGWgaYl1admTD/sG4LfBF9O/cNzpdftLP4ZMcTGY8BFUZUK/237nlG4um/odP baZacOdMmYIO594zTaZR/Yv7pFz/3oQnVjsfJHcywir9ZG8Z3TPELcMDwaoX9ADtaiBpF3Yz sZbO8600C5gaezZYBeG1a4ILFsPE2o3OoCulexTady4A1RHHEMPNqbv5I0PKq1fsYZbrOPqx k2Ge1R5zQP/jELXKA/RZXFEbqjubKlFrnk6HHINOHC00kN+Ybe+sb8VdrosXLwd7Oc45+VFf /oEXMShA/p0VTXM/QoGX6T9tIBPcBeKhxqEGiiYPAgEYJ9rQjLW9u/efgfA8DcECgy1v5Acp 4KM+xz6Q51ZYShfF+fTNeySym2usUgnmO5dW1XCJv9Rch7O9KloMynAse8lEfoTKBnsxiqo6 CjOOE02/dLymo4S9MXFoYumrI3zSut3IRd8LlnhtL2zMXHXw3qnzYp+S923RDH6Vl2l3IW5Z O5Q8ePwD+1fonZOrLhHMuhKyYAQ2oLRgoF0nypYGEfFVVCJMo9bA2Kn2JBPv5Jdx7UCtgqRX FmOy+ZgOr6IGZ3EFXgNLTF4btWSiOkemxjJzPEPOE6hzjRGzLmGdkRzPhe3ly1WKoVuAr4l2 esMvM036RS1rxgXbua9kSFf8lqTIkw6U6kIso8QBKnpgFEJzm5uTIP9CCisxr2ycPRJb1cXJ wGLiJr4h7hzwlTId1wxHyPv2ctfnZE/hwBY/mQdJlimmsv3udFv5Ud/qQ8IdwVyyglL98lRO WIxbk18GviozgdS3cNGWzihJhFFCBin4XfO8loullOIf3nwAyaJZCc4NP2W9U8Uz3NEc3IJt PuEwWLiSnDxcNu3wiI2XlV/puf+ScBqsDfPg92jA9/PCqxSjeAJWUNyTTFgR9rb7cINaInvo OBr+KB7bKy9PCVWoqtT50x2E1gPYEjsGYCAaagJEGA18aX0czSznzGFbUG3Ei+ID+Kf6le2U qSCOeoWPylTF0+yQvQzDqsNZbZ/2v8vjDbHlnUHOkZe24aiQvFVXF48O8QwaKLHgzmjrCrlF r7sSg==
Ironport-hdrordr: A9a23:BpdwUqBEzV9PkfHlHemI55DYdb4zR+YMi2TDtnoBMiC9Hfbo8/ xG8M5rsCMczQxhOk3I+urhBEDjewK7yXcd2+B4Vt3OMDUO+lHYT72KhrGSugEIdReOjtK1Fp 0OT4FOTPP1BVh+yeDg4Ae5FN4khP2K6rqhi+ub71oFd3AMV0it1WlE48+gc3FLeA==
Ironport-phdr: A9a23:rOBXXhNurOiyO7l5fAsl6nZYBhdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDv6sr1QOXFtSGo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9A dgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/6z9pHJfglFizuwbbx2I Ri2sA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S 6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5 KlpVRDokj8KODE38G7VisJ+gqFVrg+/qRNj2IPbep2ZOeBkc6/BYd8XR2xMVdtRWSxbBYO8a pMCAvYOPeZeron9vFsOrRy7BQKxGu7vyiVHhmPq3a09y+QuCxzJ3AwgHt0UsHXfsdL4O70dU eCzzanI1jXDb/RT2Trm9IfIdxEhreuWUr1sa8bRyE8vGhrDg16NpoPrIymb2f4Rs2iH8eVgT +SvhnYnpQxsvjSj2sghh43Uio8VxV3J6SF0zJg1KNO3VUJ1b9CpHZ9QuiyEN4Z4QsMvTWF2t Ssk1LAKpJ+2cSkExZkkwRPUdv+Jc5CQ7x7+SuqcLy10iXNrdb6lmRq+7UatxvfiWsWpzlpGt jRJnsXIu3wX1BHe6tKLRuVg8kqgwzqC2ADe5+dZKk4uj6XbMYQuwrsom5oTr0vDGij2lV3zj KCMd0Uk/vKk5PjiYrXnvJOTLZN7hhv/MqQogsC/AOI4PRYSX2WD5OiwyrPu8Vf4TbhElPE6j LXVvZ7AKcgFu6K1HRdZ0oM55Ba+Czem3s4YnX4CLF9dYh2HgI7pO1DVIPD4Cve/hk+hnytux /DHJLHuGInCImLCkLfnZbp97VVTxxIpzd9D/5JUFq0BIPXrV0PsrNDYFAM2MxSow+b7D9Vwz p8RWWWWAqOALKzStUKI6fk0LumXZI4VvS79JOI/6/7vi385g14dcrOz0ZsZcnDrVshhdk6ee D/nhsoLOWYMpAs3CuLw23OYVjsGTnm0Xrk84TRzI4KvEZvEXomhgK2IzW/vF5JQZ3tGDVWkG nLpMYyPHfYKPnHBavR9myAJAODyA7Qq0guj4VeSI9tPK+PV/nddrpf/zJ1v4OaVkxgu9DtyB sDb0meXTmgykHlbDyQu0vVZpkpwgkyGzbA+m+ZRQNVc4fJSUgA/HZXZzqpzAJbzXFGJZc+HH W6vWc7uGjQtVpQ0yt4KbVx6HoCrgRbCxCqtBpcekr3NDZdy86SPl2PpKZNbzHDLnLIkk0FgQ sZLMji+gbVj8gHIG4PTu0CQlqLsfqEdmifGsmaFpYaXlGdfVgM4EaDMXHRFI1DTscy8/ETJC bmnFbUgNAJFj8+EMKpDLNPz3x1AQ7/4NdLSbnjU+S/4DAuUxr6KcIvhenkMlCTbBk8elgkP/ HGAfQEgDyalqmjaAXRgD1XqK0/r9OB/rju8QCpWh0mDYEtgzLqy/zYegP3aQvhV37RF8CYtp jNoHUqsisrMAonIrA5gcaNAJNIltQ4djiSH7EonZsfmdfk41Tt8O0xtskjj1gt6ENBFmMku9 jYxyRZqbLif2xVHfi+Z2pb5PvvWLHPz9Vahcf2zuBmW3dCI96MI8Pl9pU/kuVTjH0Uk8m5n1 Nx92H6doJzBSgsUG8GUMA5/511hqrfWbzNorYrb03x3Ma6xmjTH2pQgD60kzFzzN8caO6SCG gjoFsQcDMX7M+0mlW+iaRccNfxT/qo5Vy+/X8OPw7XjfONpnTb8yH9C/Jg4yEWHsSx1Vu/P2 Z8BhfCexAqOETnm3h+ttcX+mIYMYj93fCL3wCfiBZVRYahadoMKT26lZcyxjtlznJ/iXXdE+ UXrXgldnpHyP0DKNBqnhFcY3F9fuXG9nCqk0zF49lNh5rGS2iDD2aWqdRYKPHJKWHg3iF7tJ YauiNVJFEOsbgUviF6k/ROjnfMd+v85dTGIBx0RJXuTTSkqSKa7u7ucbtQa7ZoptX8SS+Gge RWATbW7pRIG0iTlFm8YxTYhdjjstI+q+n4ywG+bMnt3q2LUPM9qwhKKrtXTQ/9K3j0DbCJ9i H/eDR69OZP6mLfc34eGqe24W2+7A9dafi/q1oOHsQOw4GwsCBb5nvb5yZX3VAM91yH8zdxjU y7F+Q39bofc3KO/Ket7f0NsCQyZiYIyCsRkn4A3np1VxWkCi8Df4y8ciWmqe4YTyefkYXEKX zJO39PF/F2vxhh4NnzQj4fpHmOUxs8rDzWjSkUR3C91r8VDCaPOqadBgTMwuF2z6wTYffl6m D4Zj/oo8n8Txe8T6kIryW2GD7YeEFM9X2SkngmU7924sKRcZXq+Obm22k1kmNm9DbaE6ghCU Xf9c50mEGd+9MJ6eF7L1XTy7MnjdryyJZoLsQaIlh7bk+VPAJc4l/5Mji9mf2v2+3wjiqY6g RFowZCmrd2HJmFqr8fbSlZTMjz4Yd9W+ym41PwF2JjNmdr3RdM7Q29YOfmgBeilGz8Tq/n9Y gOHETlm72yeBaKaBwiUrkFvs3PIFZmvcXCRPngQi9t4F3z/bARShh4ZWDIik9s3DAevkYbof 0F4/TAW43bzrxoKw+kuNh+1AQK97E+4Lyw5TpSSNk8c9gZZ+0LcKtCT9Mp2FiBcuJakrUqEI SqaYU4baANBElzBDFflML604NDG+OXNHeuyIczFZrCWoPBfXfOFrXpO+o5v/jLKPcCOeHBpS fw9iBIrtZVREMHY3TwEDS0RxXqlhyGzrxK9vCR86MG5oq2DZQ==
Ironport-sdr: 64f4ac64_WW8DianPFKLPz88C8k0OGHlco1hP8ivC9Ja7TPSdWjIuDuU vYzDlIXfWuWxvD2BLgdEHKOX+ObJiKeQHTN7x1A==

Thanks for all the suggestions, everyone. The Equations version seems to be working. I think I might go with that one. Is there any downside to using Equations that is non-obvious? (One possible complication is that an additional plugin needs to be installed.)

If I understand correctly, the situation is as follows:

(1) Program Fixpoint does not reduce because the associated proof-terms are opaque.

(2) Function results in an error because of some unknown reason.

--Agnishom

On Sat, Sep 2, 2023 at 2:13 PM Jim Fehrle <jim.fehrle AT gmail.com> wrote:

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