coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[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: [Coq-Club] Non obvious recursion (Issue with Function + Can't unfold Program Fixpoint)
Date: Fri, 1 Sep 2023 20:26:16 -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:zUhS+6OTGLvX//HvrR0gkcFynXyQoLVcMsEvi/4bfWQNrUoihTQCy TYaCmyOPqzfZmX3fYt/Otjk8hhV6JWDztRkSnM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8mk/vgqoPUUIbsIjp2SRJvVBAvgBdin/9RqoNziLBVOSvU0 T/Ji5OZYAXNNwJcaDpOsPrS8Eo34JwehRtB1rAATaAT1LPhvyJNZH4vDfnZB2f1RIBSAtm7S 47rpF1u1j6xE78FU7tJo56jGqE4aua60Tum1hK6b5Ofbi1q/UTe5EqU2M00Mi+7gx3R9zx4J U4kWZaYEW/FNYWU8AgRvoUx/4iT8sSq9ZeeSUVTv/B/wGXbS3jA/spRVH05PJU65f4tKkZe0 uAXfWVlghCr34pawZq+Q+howM8mLY/iN8UevBmMzxmAV61gH8uFGf2Ro4UBhl/chegWdRraT 8MWbzt0bBPFSxZKOxEeA9Q/mo9Eg1GmKWYJ+AjK+/JfD2773VxV8JnCM4vse8GWHc5WxF6+n F7o4DGsav0dHJnFodafyVqngfaKlifmUqoJBbig/7hrhkeSzyodEnUruUCTpPC4jgi1XtMZI kdS+yxGQbUOyXFHh+LVB3WQyENodDZFMzaJO71ntFO+2eDP7hyHB2MJaDdEZZZ0/IU1XDEmn BvB1d/gGTUl4vXfRGO/54Wki2q4GREUCmseOg4Cbw8OuOf4rK8J0xngc9dEEYyOtOPTJw3e+ T6xgRIFt+0htvJTj6Sf1nLbsg2ovanMH1IU5B2If2eL7TFZRY+CZq6q42fY8Md/CZuQcQWAm FMmmMGuyv8EIr/QtS6KQcQLRKqI4dTcOhLioFdfJbsT3BXzxCf7ZqFWwjV1BHkxA/Y+YTWzP XPi41JA1qFcLF6BTPFRYbvoL+8I0KK5N9Duds6MX+p0epIrKTO2pnB/V3WxgVLovlMny5wkG JGhds2pM3YWJIJnwBeyRMYfybUb/T8/90yCWaHEywmb7pTGaE63UbslNH68XtI95o6AoyTX9 I9RDNvV6hN9VOalXDLb37ROJn83LF86J6vMleppSsC5LDBbRV4RU83q/et5eqhOvbhkqePTz 3TsBm5a0AXegFPEGyWra1diSrHlYpVinE0eICUTYVeM8FogaLaJ860wWcYWf74m1eo71t9yb aAPVPuhC8R1aAbs2moiNMHmjYpAcB+Lu1q/DxC9amJiQ686Fh37xND0WyDOqg8MN3OTnukjq eSC0gj7f8Iydz56BpyLVMP1nkKDhllDqudcRECSH8Jyfn/r+41UKyDcqP87DsUPCBfbzAuhy AekLkYElNbJvrMK3oHFtYKco6etNtlOLE5QMm3YzLSxbCfh7jWCx61EW722Zjzzbj7/15ijQ uR39MvCFsM7smxEiKdCNop67Lkf4oLvroBKzw4/E3TsaU+qO4xaIXKH/Jdus/RNz4BGpDrsA 1qr//dYHbCNJeLkD18jCw43ZcuT1fwvu2fz7NZkBG7Y9SNI7L68fkEKBCa1iQtZN6lQHLkp5 cwDqfwmwVWzpTRyO+nXkx0O0XqHK0IxdpkOt7YYMdfNsRUqwFQTWq7sIHb6z7/XYuodL3RwB CGfgZfDoLFuxkDiVX4XPlqV1Mp/gaU+gjx7/GUgFX+oxOWc3uQW2SdP+wsZVg5WlxVL89xiM 1hRanFaG/+8wCdKtuNiAUacQg1PPUjMsAi5gV4Ej3bQQESUR3TAZj91c/qE+EcCtXlQZH5H9 bWf03zoSivuYNq35CYpREp5sLb2eLSdLOEZdByPRKxp3qXWYAYJRoerbGsM7RDiAIU4jwvGo 4GGOQq2hbLTbUYtT28TUuF2Foj8jDiPIW0ESPon/aVh8aT0ZmSpwTbXQ6yuUpolGhEJmHNUz +RlI8MJXh/41SDmQvX3w0ITC+ccocPFL+butl8myaDqfldfQvdUXErsyxXD
Ironport-hdrordr: A9a23:ISL3hKPVzUNMxsBcTumjsMiBIKoaSvp037BL7TEJdfU7SL37qy nDpoV56faWslYssRMb6LS90cC7KBu2n/MY3WB7B8bEYOCJghrPEGig1+Tf6gylNSn39usY87 xhfah4ANi1KVRhl8717E2ZPr8bsby6GWyT69s2Bk0NcT1X
Ironport-phdr: A9a23:LwGUoRalhN06Ph7/BXEaUJf/LTEQ24qcDmcuAnoPtbtCf+yZ8oj4O wSHvLMx1gGPBNmAoK4bw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzH cBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94PSbglSmTawbr1/I Bq5oAjTq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ 7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4 qF2QxHqlSgHLSY0/27XhMJ+j6xVvQyvqABkzoHOfI2YLuBzcr/Bcd4YQ2dKQ8ZfVzZGAoO5d 4YCE+UBPeBZr4nmp1sOqh6+DhSyCePv0DBImmP23aoi0+s7DA7G3AwhEMgOsX/Jq9j6LqgSU ea0zKnTzTXDaPZW1Czh54jNcxAtu+uDUq5qfcrQz0kiDgXIhUifpoL5JT2azPgNs3SF4Op6U +Kik2oqph9zrzSyxskglofHi4IaxFzY6Sl0w4k7KNO2RUN/fNOpHppduiKEOoZ1Qc4vQ29mt Ts+x7EbuJO3YSgExYkhyhXCZfKHdI2I7QjiVOaXOTp4i3NleK6/hxav6kes0PHzVs6x0FtMs yFLkcHMu2gQ2xDN5MWLUPpw80m71TqRywze5PtILV4pmabFM5It3KI8m54JvUnAHiL6glj6g a6Kekk+9eWl7+Lqaaj8qJCGLY97kAT+P7wumsOhBeQ4NRADX22B9uS90L3v51H2QLBLjvEsi KbWrIrWJcUdpqKhAg9V1Jgs6wqnAju7ztgVk2MLIVNLdR6dkYTlJ1/DLOrmAfuinVigiDJry OrHPr3lDJXNNH/DkLL5cLln5E5czgszzctf55JTD7EMO+78WkrwtNDCFBA2Lxa4w+fhCNll0 IMRQnqAArWFP6PKrV+I+uUvLvGRaIMNojbyN+Al5+LyjX8+gVISYa6p3YIOZH+kGvRmPl6Wb GH3gtYBFGcKphAxQPbriF2ESz5TZmy9U7gy5jEhW8qaCtLIQZnoi7ic1g+6GIdXbyZIEAOiC 3DtIqyLXfYXaCWXauRhmyAYUqCoR48w3ADm4Ab1zbt8Lu3R0iYdtNTq35504buAxlkJ6TVoA pHFgCm2RGZukzZQL9dX9KV2oEgnj0yGzbA9mftTU9pa+/JOVA4+c5/a1e1zTd7oCUraZtncb lGgT529BC0pCMoryooHbEB8ANWlizjI2ivsCrRTlrrYTIcs/Pfk1mPqb914126A0aAgi1c8R c4aPGKgh7V/8A37DIvI1UyS0aesJuwHxCCY0mCFwCKVuV1AFg59VaKQRXcEek7ftsj0/GvHR r6qT78iM01IwoiDLMOmc/XPilNLDLfmMdXaOSeqnnuoQAyPzfWKZZbrfGMU2GPcDlIFmkYd5 yTOMw92HSqnr2/EaV4mXVvyf0Ph9/V/o3KnXwc1yQ+NdUhoy7uy/FYcm/WdT/oZ2r9Mtj0mr n14G1O03tSeDNTlxUIpdapaYMg951Jv3mfY8QV2eJ2mbuhjilMYbwVrrhb2zRwkQo5EkMUss DYr1F8rc/nejggHLWvDm8qpYO6ySCG65h2kZq/I10uL1d+X/v1K8/EksxD5uwrvEEM+8nJh2 t0T0n2G55yMAhBBNPC5Gksx6RV+oKnXJycn4IaBn3RjN6ivsjjH89ksBa0swVCheZ0MVcHMX B+3CMAcC8W0faYjlF6odRIDOchZ8a9yNsjgdv3Mi+a7ee1nmjyhl2FO5otwh1mN+yRLQenNx 58Zwvuc02NrTh/EhUy6+oDykIFAP3QJG3anjDLjD8hXb7FzeoACDSGvJde2z5NwncylV3ld/ V+lT1QIva3hMROdaV3m3QpV/U8SoDqukm25yXR4nioooayWwCHVi724L1xZYSgRHDIk1w62a YGvx8gXRk2pcxQkmH7HrQ7hyq5Xqb4+Z2jfTEFUfjTnemRrU6++rL2HMIZE7JIltzkSUfzpO ArBDOCm5UFCiGW5RjENoVJzPyunsZj4gRFg3WeULXIp6WHcZdk13xDUotrVWf9W2DMCAih+k zjeQFambLzLtZ2ZkYnOtuemWievTJpWJGPiwoWBryu84EVhBBz5lvv1m9utQm1YmWfrksJnU ynFtkO2a4bt1r+6NudPdUxpQlb3rct8UNI2gs47g5ce3mIfj5Oe8C8ckGv9Bt5c3Lr3cHsHQ TNYprydqBigwkBoKWiFgp7oTnjIiNU0fMG0OylFkjJ49c1BD72YqaBJjTcg6ETtthrfOLB4j n8LwP8qohb2mskvvwwghmWYC7EWRwxDODD00g6P5Ja4pblWY2Cmdf6x0lB/lJavFuPKpAYUQ 3v/dpo4eE04psxiLFLB1mHy4YD4aZHRa9wUrBidjxbHiaBcNpswkvMAgScvN3j6uDUpzOsyj Bom2p/f3sDPM2J24KewGQJVLBXwbsIXvDrojOBXlYCX2cHnH5lsHCkKQIq9Tf+sF2F317yvP AKPHTsg73aDTOOFRknBswE89ymJScnxZBT1bDEDwN5vRQeQPhlaiQEQBnAhm4IhUxqtz4rne Vt44TYY4hj5rAFNw6RmLUqaMC+XqQG2ZzMzUJXaIgBR61QI7kjTMNee6edbFCRZuJSq6g2LY D/+BUwAHSQSV0qICkq2dKGp/sXF+vOEC/CWKvLPZfOFrO0YXvzOxJTlge4Et36cc86IOHdlF fgy3EFOCGt4F8rukDIKUyULlijJYqZzRT+58yxz6Mu68bLiU0Tu49nXY1O9Gd5q+la/iuGCM bzJ7M6cAT1d19UFzjnJzupHtGM=
Ironport-sdr: 64f28f5b_HIhOtBUcZja/LcAXa1/n9mmU8ADDQsIlqvhnRZ0k+Df9J+t J9aslIid97Ew+yAaFWcElHZvBF6QjF4E37TdXOQ==

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