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: Wendlasida Ouedraogo <ouedraogo.tertius 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 09:25:11 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ouedraogo.tertius AT gmail.com; spf=Pass smtp.mailfrom=ouedraogo.tertius AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi1-f173.google.com
Ironport-data: A9a23:JMiy/q7buJ/qDMATVVNfDQxRtCjDchMFZxGqfqrLsTDasY5as4F+v jYbDD/QOffeNzD0KohzYd+w/EhV7JKAzYNjG1c+/ig2Zn8b8sCt6faxfh6hZXvKRiHgZBs6t JtGMoGowOQcFCK0SsKFa+C5xZVE/fjUAOC6UoYoAwgpLSd8UiAtlBl/rOAwh49skLCRDhiE0 T/Ii5S31GSNhXgsaAr414rZ8Ek05KWq4WtE1rADTakjUGH2xyF94K03fvnZw0vQGuF8AuO8T uDf+7C1lkuxE8AFV7tJOp6iGqE7aua60Tqm0hK6aID+6vR2nRHe545gXBYqhei7vB3S9zx54 I0lWZVd0m7FNIWU8AgWe0Ew/y2TocSqUVIISJSymZX78qHIT5fj68x8EHA3NqYUweF2Wl5F5 OA+LDwwRSnW0opawJrjIgVtrsEqLc2uO4JG/385kmqfAvEhTpTOBa7N4Le03h9q3pEITauYP pRGL2MwN3wsYDUXUrsTIJUjkeuyj37wdHtEpUiJpLcsy2fWxQ11lrPqNbI5f/TUGZQMxBrE9 goq+Uy6MhI0LPW5+wa8816NmtD+zB+rRtw7QejQGvlC2QXPnAT/EiY+Xlyi5PK9l0SWQMNaM 0VS+yw0rKF0+lbDczXmdxixoXrBuR9FHtQJTLZ85waKxa7ZpQ2eAwDoUwKtdvQfptMHRDcB2 mSOnojWDi1zlrmZdFmko+L8QSyJBQAZKmoLZCkhRAQD4sX+rIxbsv4pZoYyeEJSpo2kcQwc0 wxmvwBl2OpO1Z9jO7GTuAGY02j19/AlWyZsvl2PNl9J+D+Vc2JMWmBFwV3S7PIFK4fAC1fY4 yNClM+Z4+QDS5qKkURhodnh/pn5tp5p0xWG2jaD+qXNERzzohZPmqgOuVlDyL9BaJpsRNMQS Ba7VfltzJFSJmC2SqR8fpi8Dc8npYC5S4W+C6GPNoEUOsQoHONiwM2ITR7Bt4wKuBh9+ZzTx b/GGSpRJSxKVPo7kmTeqxk1jeN3nUjSOl8/tbiil0j9uVZvTHGSTrgBPTOzghMRvcu5TPHu2 48HbaOikk0BOMWnO3W/2dBJcTgicyNgbbio8Jw/SwJ2ClA5cI3XI6SBn+1Jlk0Mt/g9q9okC VnkBx4FkAKv1CGXQehIA1g6AI7SsV9EhSpTFUQR0ZyAghDPuK7/svlNRIh9ZrQ96u1owNh9S vRPKY3KAe1CRn6Ds34RZIX05t4qPhm6pxO8Dwz8ahgGfrlkW1Po/P3gdVDR7yUgNHe8mvY/h LyC7TnlZ6Q/aT5sNvuLV8L3/WiN5SAcvMlQQ3r3JsJifRSw0YpydA30oPwFA+ANDhThwDGl+ R6cKkoar7OVoqse0trAtYabpaiHTsp8GUt7GTHAzLCUbCP1wEuq8bViYs2pIw+EDHjV/oemb sVrl8DMCuUNxgt2gtAtAoRVwrIbzPqxgb1jlyBPPmjBNnavAZNeeki259FF7PBx9+UIqDmNe xy9//dBMu+0I+LjKlkaITQlYsml1f05njrz7+w/EH7l5R1Yraa2bkFPAyai0CBtDqN5EIcA8 9cTvMQ77w+eiB1zPO2W0QFS1WCHdUIbX4sd65o1PY7MiygQ8G9kX6DyMCHNzau0W41+CXVye j6wr4jetotY3XvHIiYSF2CS/O9zhqYumRFtzX0ELWungtDu2/09hkVQ1R8VTQ1l6ApN/MwuG 2psNmxzfb6v+RUxjud9fmmcISNzLzzHxRWp0HoPtmnSb3fwZ1z3NGdnZNq8phEIwVxTbh1w3 e++yl+8dR3IYcuo/C85eXA9mszZVdYrqzHzwpG2Lf+kQas/TyHu2JK1RGwyrBDiP8M9qWvHq cRu/8dycafLDjERkYJqF7il0aksdz7cKFxgWf1B+IY7LVPYchy22hmMLBm/QdMSBvro9UTjN ddiCPgSXDuD1QGPjAshO4gyH5FOksUE2v8+a5LwBGtfs7Kgvjtj653R0S7lhV4UedZlkOdjC 4aIdzu9DXCa33hEv1D8vO9WH3eKO4gaVlfs2MSw1vsDLLMYkeRWaUpp+KCFj3aUFwpG/hyvo wLIYZHN/dFi0YhBm4jNEL1JIhedc+PIS+WD9T6sv+R0bd/gNdnEsyUXoALFOzt6EKQwWdMts 5iwq//ygV34uYgpX1Djm5WuE7dD4eOwVrF1NuP1NHxrojuQavTz4hcs+3GKFrIRqYlzvvKYf gqfbNe8UfU3WN0HnX1cVHV4IiYnUq/yav/tmDO5o/GyESMi6A3gLu32xU+xOCsfPmUNNoblA wD5h+e265oK5M5QDRsDHLd9D4U+PFbnXrA8esbssSWDSFOlmU6GpqCogC9IBesn0ZVYOJ2SD VP5qhnCmNCavajJyJRestU3sERIVzByhu4/ek9b8Nlz49x/4KjqMsxFWajqyLkN+sAx6H08T D7IZWomTy76WFyotD3itc/7UF736vMmY7/Ey/9Aw69QQyizDYKERrBm80+MJpuwliTLlImaF D3VxpE80tVdDH2kqSb/K8FXWdta+84=
Ironport-hdrordr: A9a23:UL9+SKhYX35f5ioviOx/eyX7v3BQXuMji2hC6mlwRA09TyX4rb HWoB1/73XJYVkqKRQdcLy7Scu9qDbnhP1ICOoqXItKPjOW3FdARbsKheDfKn/bexEWndQtsp uIHZIObuEYzmIXsS852mSF+hobr+VvOZrHudvj
Ironport-phdr: A9a23:D9muERZKXOVQun+YnOGKrun/LTG22oqcDmcuAnoPtbtCf+yZ8oj4O wSHvLMx1gGPBNmAoKsd2qL/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQF cVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHNYghEniexbLx8I Rm5sAndq80bipZ+J6gszRfEvmFGcPlMy2NyIlKTkRf85sOu85Nm7i9dpfEv+dNeXKvjZ6g3Q qBWAzogM2Au+c3krgLDQheV5nsdSWoZjBxFCBXY4R7gX5fxtiz6tvdh2CSfIMb7Q6w4VSik4 qx2ThLjlSUJOCMj8GzPhcNwgqBUrhKvqRJ83oDafp2aOeFkca/BZ94XX3ZNUtpTWiFHH4iyb 5EPD+0EPetAr4byuV0Ooga6BQa2H+PvyyJHiWXr1qMjzuQuDxzJ3BY6ENIJv3TUq8j+OaAVU eCo0qbH0C/DYOlR2Tfy74jEaAwhru+WXbJscMrR1FIvGhjKjlWVs4PlPjeV2v4RvGic6uptT OSigHMopA9tuDag3NssipXXiYIPzFDJ7Sp0zYU6KNO3VEN2b9CpHYVOui+UNIZ4TcMsT3x1t Cg1xLMLt5G1cicUxZk6wxPSdv2Kf5SW7h7+W+idPzN1iXNjdbmiiRiy9k2gxff9VsmyyFtKr yxFksPNtn8XzRDT5NKHRuNy/kegxTaP1x3T5fpeLU8okqrbLpgsyaMzmJoLqUnPADP6lUHsg KKVdkgo4PWk5uXlb7n8u5ORNYF5hwfjOao0gMO/G/43Mg0WUmib5+u80Lrj8FX8QLpQj/02l rDVsJfbJcgGv6K5DRJZ34Qt5hqlADem19MYnXYDLF1bYh6Ik4/pO1TWLPD5C/ewnUisnS91y /zaOrDtGJbAI3jZnLv8fLtw6VRQxBcxwN1R/55UD6sOIPP3Wk//rtzYCRo5PhSzw+b6Ftpyy 5keVniIAq+WN6Peq0OI6fw1I+mQZY8VpS39JuMq5/7rl3A5mFsdcbO10psQbXC0BvJmLF6Bb nr2ntgBCXsKvhY5TOHylVGOSSRTaGqqX6Ig+jE7D5qrApvERoC0mbCOwCO7HoBNaW1dEVCNE XLod52eVPsWaSKSJNVhkj0eWrS7RY8hz0LmiAivwL1+a+HQ5ycwtJT51dEz6feAuws18GlLA sKR12iWTm191kQVSjMs1adwpgQpzUqO3bJxhPNfU8Be/e9ITxwSOpvVzug8ANf3DFGSNuyVQ UqrF431SQo6Scg8lodmiydVHtyjikuGxC+2G/oOkKTNApUo86Xa1ny3JsBnyn+A2rNyx0I+T J5pMmurzrV66xCVH5TAxkKEmqqwfKMT22jR+X2fzHeVlE5dWQ90F67CWCNXfVPY+Ozw/ViKV LqyEfIiOwpFx9SFL/5Nd9Dll1xBS/ClJNnEf2OsgE+/AB+JwvWHa4+5M34F0nD7D04J2xsW4 W7ANQU6AXK5pHnCCTV1CV/1S0bl8O07r3LiC0FtkFrMYEpm2L64vBUSgJRwUts12bQJ8Gcko jRwRxOm2s7OTsGHv0xndbldZtU05BFG03jYvkpzJM7oKacqnVMYfwlt2iGmnxxqFoVNl9Qrp 3I23UJzL6yfylZIazKf29j5JLTWLmD4+B3nZbTR3xnS19Of+6FH7/pdyR2ruxykGlAr9Hpgl cVYyWed+47iAw8bUJa3WUEytlB7q7zcfigh9tbMz3Q/VMv8+jTG2t8vGK4k0kP6J4YZYP7CT VGtVZRFXJvLSqRigVWiYxMaMfoH8ac1O5jjbP6awOuwO/4mmju6jGNB6YQ700SW9iM6RPSbu vRNi/yewAaDUC/xyVm7tcWi04dZaD0IF22wzm74CZRNZ7BpVYkOAGaqZcaww58t4vylE24d7 1OlC14cjYWuZBeedVX60goWyUkNvX26ggO3yjV1l3ciqa/Vj0msi6zyMREAPGBMXmxri1zhd JO1g94tV0+tdwE1lRGh6C4W3oBjrb9kZynWSEZMJG3tKn16F7C3rvyEatJO75UhtWNWVv69a BaUUOy1rxwf2iLlV2xQoVJzPza3t5njlht1jySBIWxvrWfCUc51zBbbotfbQLZd0yEHSy9xl TTMTgLkbp/5oJPNyciF67/lH2u6M/8bOTHm14aBqDe26SVxDBuzkury0tzrHA4m0DPqgtxjV CHGthH5MeyJn+yxNeNqeFUtBUepsZIrXNEj1NJu29dJhiNJ4/fdtWAKmmryL9hBjKf3bX5WA CUO38aQ+w/9nktqMnOOwYv9EHSb2MpoIdegMQZ0kmow6d5HDKCM4flKhyxw9xC/sA/de/F6k TBb1fY09H8HmMkGvQMsymOWBbVYTiw6dWT80g+F6dyztvAdY3uifaK500V528ysFq2Dvxp0V 3Pwe5NkFih1pJYaUhqEwDj47Yfqf8PVZNQYu0iPkhvOuONSLYo4ivsAgSc0cXK4p3AuzPQ3y AB/xZzv9pbSMH1jpejqZ3wQfi2wfc4Y/SvhyLpTjtrDlZ76BY1vQ30KRMe6Fq/uSWNK8667a EDWV2dg4naDReiBQUnFsxwg9iyXVcjsbiDyRjFRzM0+FkfDYhUH2kZMGm19xMZxFxj2lpK/N h0lt3ZBvhig7UEUguNwa0ugCCGG+EHxO21yEN/GfH80pklD/xuHbpDYt7guWXkeptr48kSMM jDJPlwYSzhWBQrUQQikZODm5MGcobHHXaznfqeIOfPW7rUAMpXAjZO3jtk8p2fKZpjJZyMyS aV8gxULXGglSZ6AxXNSG2pOxniLN4nC9V+94nEl9Jnhtq6wCUS0v83XTOIDVLcnswa/haPJX wKJrAB+LzsQlpYFxHuTjaMawEZXkCZ2MT+kDbUHsyfJCqPWgK5eSRABOWt1M4NT4qQw0xMoW 4aTg87p1rN+kv8+CktUHV3nlMazYMUWIma7fFrZDUePPb6CKHXF2cbyKa+7TLRRiq1TuXjS8 X6DFFT/Oz2YizTzfxWmMOUJiyDCeRIH59r7fRFqBmzuCtnhb1zzMdN6iyE33axhhn7OMj15U 3A0eEdMo7uMqCJA168nSioRszw8c7bCwnnCvIy6Yt4MvPBmAzp5jbdf6XU+kP5O6T1cAedyg G3Up8JvpFevlq+OzCBmWVxAsGUu5srDsEN8NKHe7pQFV2zD+UdH6nidBw4DoNRiTMHiobxR1 8Pnm6f6KTME+NXRt5h5ZYCcOIecPXwtPAC8UibTFxcARCW3OHv3gkVclLSV9yTQoMFl8d7jn 50BTrIdX1swXKB/aAwtDJkJJ5F5WSkhmLiQgZsT5HawmxLWQd1TopHNUv/66RDHJzOQjL0Cb BwNk+uQxWU7M4T63wllawA/kt2VQAzfWtdCpiAnZQgx8h0lGJdWQWg62kajYQSosiZ7KA==
Ironport-sdr: 64f2e365_vzk/qMpqhh1sA4KRjrZNEL9aYLOsFEvWxEU69kpiDfv09Qf aiqc/1KosDc9MupuEe83jhD3/Pl//2Xl5cMv44w==

Hello,

I had a similar problems a couple of years ago (https://sympa.inria.fr/sympa/arc/coq-club/2021-08/msg00043.html) and Pierre Castéran gave me this solution (https://sympa.inria.fr/sympa/arc/coq-club/2021-08/msg00044.html) which solved my problem.

Regards,

Le sam. 2 sept. 2023 à 03:27, Agnishom Chattopadhyay <agnishom AT cmi.ac.in> a écrit :

Hi all;

I have a function I am trying to define whose well-foundedness is not obvious. I am trying to do it in two different ways: (1) using Program Fixpoint and (2) using Function. In both cases, I am using the fixannot {wf ...}

However,

(1) When I try Program Fixpoint, the function can be defined. But it is opaque to `simpl`. How do I get around this? I need to be able to prove things about this function.
(2) When I use Function, I am getting a strange error message. The error message is not helpful because it references some variable names which I have not used.

Here is the Coq code: https://gist.github.com/Agnishom/1150d29732a6c727396fb6c118dbf375

Any help with this would be appreciated. I originally posted this on StackExchange, but I am corssposting here because I think this would be better suited for a threaded discussion rather than a Q/A style one.

Thanks!

--Agnishom

[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