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: Meven Lennon-Bertrand <mgapb2 AT cam.ac.uk>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Non obvious recursion (Issue with Function + Can't unfold Program Fixpoint)
Date: Mon, 4 Sep 2023 10:40:51 +0100
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=cam.ac.uk; dmarc=pass action=none header.from=cam.ac.uk; dkim=pass header.d=cam.ac.uk; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=FKIJAILF6TF9MC6bBzbwXh9u77/K7Z3SxpCUH0WlYQw=; b=VOh9bAm2skQ8yleZZho9DIoai5scjC7oCNAQ83+gtpuein7mcsiE3evxrps/IWGab3SBu7MLy3tkx0z4OfUeRQPrsgviYPQuxbcwYWe964h0nJaWwF+age28RHLhdEW7rOrgAQL3EZpV/WZTu1mxnMO1OyMGj4W8UtfwFAT5B7i/f9RKFTOTF4n11tB/QP2DRXjL0DZ23A1vQDabG3BuTJeFXrfLJu+2zGOiSpp7VS9g0emhVPraIJ/YT1Op8DDBDf9rI+l5OzcgSE0ACGWcn2Khz81kQF/A0UQRHFh/LNmwU5oLI21zIk/ifG6uaMumw5KUHnDlgBdeDHmQXkFl4g==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=nB544h0mJlsT/3bpErzTTqEY7E949FilCJYkm36kYah3ATKFMPJVI0bRxcY2oo5Xs+G0KnRShYuip3d/CaI68YkzC8uEKvZEQnBD15aBTjCkM0XON1+EqIWWBRF6ptEtsMHMSE5c4Jvxd6xKk7YAKdtLXIJNiG7dCo7S7NM9KEvmg24f6Kb8rHAeU3LNDHgqmQDfa2HC6iPa+C+S34d51+8ByOWm7xLMP0xLyjB58ku8m4ISuCVkjzzMvJ/Q8pYPf3iKzUfcoh/naPk18oTDQ2qp5BLKYsQgaVlHw+kBqfORdp3ScBqf0BnZFVE1HiAcwkqu0QEhOC9yGZhdRlZx9w==
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mgapb2 AT cam.ac.uk; spf=Pass smtp.mailfrom=mgapb2 AT cam.ac.uk; spf=None smtp.helo=postmaster AT GBR01-CWX-obe.outbound.protection.outlook.com
Ironport-data: A9a23:n+q35a632n9nSC5ipbmbWAxRtBzCchMFZxGqfqrLsTDasY5as4F+v jccC27Qaf7eYDH1fdp2Ydu09B9Tvp6GzYBlGgptpCk1Zn8b8sCt6faxfh6hZXvKRiHgZBs6t JtGMoGowOQcFCK0SsKFa+C5xZVE/fjUAOC6UoYoAwgpLSd8UiAtlBl/rOAwh49skLCRDhiE0 T/Ii5S31GSNhXgsaAr414rZ8Ek05KWq5GtB1rADTakjUGH2xyF94K03fvnZw0vQGuF8AuO8T uDf+7C1lkuxE8AFV7tJOp6iGqE7aua60Tqm0hK6aID+6vR2nRHe545gXBYqhei7vB3S9zx54 I0lWZVd0m7FNIWU8AgWe0Ew/y2TocSqUVIISJSymZX78qHIT5fj6/pHJxs7HJIJxr9MGmZV8 tAzbyEQaznW0opawJrjIgVtrusJFpGyeaggijRnxzyfCus6S5feRamM/cVfwDo7msFJG7DZe tYdbj1sKh/HZnWjOH9LUNRnxLju3yOmNWQA9zp5poJvi4TX5Al+2aDnavLec9nMTM4Tg0XwS mfupj6lW05BbIfOodaD2mmAtuHtlw7VYalIE+2F2P5JqVuNyWNGXXX6UnP++5FVkHWWUNVGb kcQ5yAGtrk37EXtT9/nXhT+rmTsg/IHc99ZEul/4x6dxaDOu1+eADJdFmEHb8E6vsgrQzBsz kWOg97iGT1otvuSVG6Z8bCX6zi1PED5MFM/WMPNdiNdi/GLnW35pkinog9LQffl3O7mUyr92 S6LpyUYjrAex5xDnaai8FyNx3rmqpHVR0Rnrk/aT0C03DNfPYSFXo2P7USEzPBiKI3CcEKNk kJZkOej7ccPL6q3qgqzfMs3EoqE2dO5IRzHoFs2H5Ae5zWnoHGiWoZL4QBBHkRiM+daWDzlS 3LRkBN12bljA1Dzc55yXp+7UPpy/K2xTN7gb+3fTvhQbrdPdgOo+D9kZBOO01DXi0J2wLsbP LGFe/2NFlcfM7xslxCtdtce0Jgq5yEw/nzSTpbF1Caa0aKSSXqWaLUdOn6cR7kdwILdhy7K4 vBNNNCvyRpNYNbhYyLSz5EfHWoKIVc/G5ryjc5dLcyHHSZLB0AjDO3305o6Wok4gZlQqPjEz ku9VmBc1lD7o3/NcieOS3J7bYLQTYRNlm06MQMsLGSX9SAaO6j315gmdrwzYbUD385gx6QtT /A6JuOxMs4WQTHDozkgfZ3xqbJ5TyuShCWMAXuBQCM+dJteVQD26ofaXg/wxhIvUAuzl+UD+ oOF6C2KYKAtZQpYCOTuVMmO1HK05HgUp/JzVRDHI/5VY0Tdz7JpIC3Q0N4yBcEGEkjD9yrHj g+HIAw5oNPVqNQf6+j5hqGjrqaoHdBhH0FcIXLp0LauOQTe/Uuh2YVlUtvUTQvCVWjxxrquV d9Vw974LvcDulRA6Kh4LJpG0oM84IHJi4JB7wE5AkjOUUunOolgLlaCw8NLkK9HnZ1dmAmuX 3Ow6stoAqqINOzlAWwuClIcNMrb7s4tmx7W8fgRC2f57nUu/LO4DGNjDyPVgylZdLZIIIcpx Nk6g/Ev6iu9tEsOEs2HhSVq5WizPiQ+c6E4hKo7Xq7vqCQWk29nX7KNJBPy0p+1b/d0DnILO R6R3arLuKRdzBHNcl01Dnn84tBejpUv5jFP6l8IHAmJq8uY3/Ym/QZw9A4vRV9/1SR30ONUO 0lqOXZqJK6IwSxauchbU02oGCBDHBe8+HGt+2AWlWbccVakZlbNIEI5J+yJ2kITqEBYQRR24 5CazzzDfQvxXcSswBY3Z1Fpm8bjQfN16AfGvsKtROaBPpsiZAvakr2cXnUJpzTnEPEOqhX+/ 8cyx9lJaIr/KSI0iI84AdPD1b0vFTa1FFYbSvRlpK40DWXQfQ+p4ge3KmezRJJ9F6SfuwvwQ cljPdlGWBmCxT6D5GJTT7IFJ7hv2uUl/pwec7fsPnQLqKabsiEvip/L6yzinyU+dr2CSyrmx l/5LFpu01B8hEe4X0fihvMcYy+TXulBYwfxmueo7O8OCpQP9vl2dl0/2ae1uHPTNxZ7+xWTv 0XIYKq+IymOD2hzt9OEL0mBL1zcxRDPuCCg+wm29d1FK87MWSsLnx1AsUHpZmy6IpNIM+maV t2xXBrf10rA+r89FX3a83VE+2+l+u3qNNdq3gnLwLW2UMdMtAIAI/fOxoxgFaF0rQ==
Ironport-hdrordr: A9a23:mjYzBKlbNRTkHiMKjXAeyAT+vofpDfPJimdD5ihNYBxZY6Wkfp +V88jzhCWZtN9OYhwdcIi7SdC9qADnhOZICOgqTMGftWbdyQyVxe1ZjbcKoAeQUhEWlNQts5 uIGpIWYLabYzlHZK3BkWuF+qMbsb26GdeT9ILjJhlWPGJXQpAlyz08JheQE0VwSgUDL4E+Do Cg6s1OoCflUWgLb+ygb0N1F9TrlpnurtbLcBQGDxko5E2lljWz8oP3FBCew1M3Ty5P+7E/6m LI+jaJrZlL8svLgCM05VWjo6i+q+GRheerw/b8xPT9Hw+cxzpAor4RGoFq8gpF4N1Ho2xa6+ Uk6y1QRfibrUmhPV1d6CGdpjXIwXIg7WTvxkSfhmamqcvlRCgiA84Eno5BdADFgnBQye2U/Z g7rF5xjaAnfy/ojWD4/ZzFRhtqnk27rT4rlvMSlWVWVc8bZKVKpYIS8UtJGNNYdRiKn7wPAa 1rFoXR9fxWeVSVYzTQuXRu2sWlWjA2Eg2dSkYPt8SJ23xdnWx/zUEf2MsD901wgK4VWt1B/a DJI65onLZBQosfar98Hv4IRY+tBmnEUXv3QRKvyJTcZdA60l722uDKCe8OlZ2XkbQzveQPpK g=
Ironport-phdr: A9a23:AK0tDxOg46kkZnFLjv4l6naVBxdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDv6sr1QOZFtyEo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9A dgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/6z9pHJfglFizmwbbxvI Bi0sA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S 6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5 KlpVRDokj8KOCI6/m/ZhMN+kbxVoByhqRN9zIHZe5uaOOZkc67HYd8XS2hMU8BMXCJBGIO8a I4PAvIGM+lGsYnyuV0Opga4CwayAuPvzDhIhnnv0aAnzeshCx3G3BY6ENIIrXvfsdL4NKIdU e+v1KnH1ivPYuhK1jjn7YjEaAouru2WUbJtcsrc0E8iHB7KgVuMs4LqJS+V1vgTvGiB6eptT eyihmwlpgxyozWj2tsgh4vUio8Uyl3J8St3zYY3KNGkRkN2fNGpHZhMuiyEK4Z6X8AvTW9mt Ss4xbALpZy2cicMxZ86yRDfbPmHfJKJ4hLlTOueOy14hX1keLKhnRqy9lKgyuLkWsmxzllKs DRKkt/Wun8XyxPe7NWMRPhl/kq51juDyxrf5vxYLU02j6bXNoAtzqMqmpYOrUjOHDf6lFv3g aOKeEgp//Wk5/j9bbjno5KRNpN4hh37P6s1hsCyBOE1PhUOUmWd5O+yzqfs/VfjT7VPlvA2k rfWsJTdJckDp6C0HhNb3po+5xqmETqp0NUXkWAALF1eZh2LlY/pO0zSIP/jCve/nlKsnypxy /DeJL3hBYnNIWbfn7f9fLZ97EhcxBA0zdBC+5JUDrYBIPXwWkPrqNPYCRo5PxS1w+bhFtp9y psTVG2TDqODLa/erV2F6vgyL+WSeYMZoivxJ+Qn6vL2iH82g14dfa2n3ZsNb3C4G+xrI0CWY XX2mtcOCnkGsxEiQ+PwjV2OSyRcaGqoU6Ih5TE3EISmApzbSYC3nLOBxDu7HoFRZm1eF1yAC W3oeJmcW/cQdCKSJddsnSADVbi4UoMuyRWutBLhxLd8NerV+igYtYr529Rv5u3Tkwsy9T1uA MiH3WGNVTI8omRdTDgvmat7vEZVy1GZ0KE+jeYLO8ZU4qZsXxk3M9b4wup8DNa3cA/bYs2AT lruFtCpCCk7FPo6ytpIak07Btb03UOL5DajH7JAz+/DP5cz6K+JhxAZRu54wnfCjuw6ikU+B 9FIPiugj7J+8A7aA8jIlV+YnuCkb/dUxzbDoUGEy2fGp0RESEhoS6yQWH8WfkGMhd/w4wXLR PmzCudvKRNPnPaLMbACcdj1lRNDTfbnNs7ZZje0lG6oD0ygzbqJKoPhPXgej23GEEZRtQcV8 D6dMBQmQCesp2WLFDt1CVfmeF/h68FRgknjFwof8DHPaEdskb2o5hQSmPqQDesJ2a4Jszsgr DMyG0uh29XRCJyLoA8JkLx0R9Q77R8H0GvYs1Y4JZm8N+V4gVVYdQ1rvkTo3hExC4NakMFso ml4hAx1YbmV1l9MbVb6ldj5J6HXJ2/u/Ruud7+e21fQ18yT87sO7/JwokvqvQWgHE4vu3t91 Nwd33yZ75TMRA0cNPC5GkM4/gBw/ZnRayx77oiSyH4teai4vzne2s44UfM/w0XodNNePaWYU Q7qRpFCQZH2d6pzwQHvN0pbb4UwvOYuMsirduWLwvuuNedkxne9iHhfpZp62QSK/jZ9TejB2 9AExeuZ102JTWSZ7h/pv8bplIRDfTxXEHC4zH2uAYFYfqcoVY0CDCGnKIuqxZ8t4vylE24d7 1OlC14cjYWsdhOKZQbV1gRVk00c52Gk03jw33l/lDcnqbCa1SrFzrH5dRYJDWVMQXFrkVbmJ YXcY8kyZEGzdEBpkRKk4Ry/3K1HvOFlKGKVR05Ufi/wJmUkU62qt7PEbdQdoJ8vtCxWVqy7b zX4Avb4rBIC2XnLFGJbgjkwMSyp8pn0hB11jmuBIW078CKfIJkvg06FvZqFHaEZ1yFOXCRij DjLGlWwWrvhtc6ZkZvOqKH2Vm6sUIFSbTi+yIqBsCWh4mg5SRa7nv21hpjmCV1miWmij4YsD H+R6k+kPdqOtezyK+9sc0h2CUWp7sN7Hts7iY4snNQK3nNcgJyJ/H0BmGO1MNNB2Ku4YmBeI FxDi9PT/gXh31Vua3yTwIesHHCSy9NrPfGxa2ZQ0yl78sMAW8L2pPRU2DB4pFa1t1ebZPd0h j1H4fAn7TgTiKcUu0B+hjXYCbcUE05COCXqnBnd9NGyopJcY2O3eKSx3k5zzrXDRPmS5xtRU 3HjdtI+DDd9u49hZUnU3iS5ucn0PcPdZtUJuliIngfc2qJLfYkpmKNv52IvOHqh7yF9jb9hy 0Qohdbj4cCGMzk/oPr/W0YHcGWzP4RKpHnslfoMw5zQhtj3WM0nQnJSAP6KBbqpCG5A7Ky7c VrRVmV68jDCRvLeBVHNsk4+9iCWSsn5OS3PfCtLiokyIXvVbE1H3lJOVW1jzMdgT1KkmJS6I hU+umFZ50am+EFFkrs6bkCmAGmD/Fz6Om9sEMrNa0cOi2MKr0bNb57E57oqTXgBp8+v8FTWe GfDP1waXyZUAwSFHw6xZLD2vIuZqrHKCLbmdKnAOe3W+74ZCq3AgJur1sEOEy+kEMKJMzEiC vQ63hAGRnVlA4HDnD5JTSULliXLZsrdpRGm+yQxoNrtuPLsEBni44eCEd4weZ1m5gy2jKGfN uWRmDcxKDBW0YkJzGPJz75X1UAbiiVnfT2gWboasiuFQKXVk65RRxkVDkE7fNNP9L451xJRN NTzpfnPjuc9pcEFTlBPWBrmh92jYtEMLyelLlTbCU2XNbOAYzrW38XwZqD6QrpVzYA2/1Wxt TudD07/L2GDmj3uBFikNeBBij3ePQQL5Nn7K04yTzG5FZS/MkLoVb0/xSc7yrA1mH7QYGsVM DwmNlhIsqXV9yRTxPN2B21G6HNha+iCgSeQqefCefN0+bNmBDp5k+VC7TE00bxQuWtBS/Vtk nH6pddr5Vit1PSMgGkCMlIGunNQiYSHsF83c73e7YVFUG3Y8Qglwk+qU01PjORVT9rltuZX1 8TFk7/1JHFa6dXI8MAABs/SbsWaLH4mNhmvEznRRlhgL3bjJSTUgEpTl+uX/3ueo80hq5Tir 5EJT6dSSF0/Ev5y4qFNF9UHZp58GC4nw+bzZC8gylCE9ECUb/pq+5fNW7SVHOnlLyufgf9cf RwUzLjkLIMVcIrmx0hlbVo8l4PPSRK4tT9lqSRkKAY/5lhOoiEWcw==
Ironport-sdr: 64f5a633_De8P0rPmt2wpofxqrrE+YnxLgfRZcrbk+UK+LeRkwzLS/D/ kU45MdKXmfKNmwp2aIrDbRTU3O5xJjzoXbKwWNA==

Sadly, things are slightly more complex as one might think first: if a definition B relies on a definition A being transparent to be well-typed, then all further definitions depending on B might also need A to be transparent in order to be well-typed (at least if B is transparent too). That is, there is some form of dependency on some definitions being transparent. This does not mean that this is impossible, just that designing such a mechanism must be done with some care. There is an interesting proposal on how to do this on the type theoretic side in Controlling unfolding in type theory, which I believe has inspired a mechanism now implemented in Agda.

Meven LENNON-BERTRAND
Postdoc – Computer Lab, University of Cambridge
www.meven.ac

On 02/09/2023 20:12, Jim Fehrle wrote:

CALrWwX_W_sO_DkxHw4dyd6wSLQpJ9f0dC-O2rzVtKFUcPc45dg AT mail.gmail.com">
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