coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How do I convince Coq that my recursion is guarded?

From: Li-yao Xia <lysxia AT gmail.com>
To: Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] How do I convince Coq that my recursion is guarded?
Date: Sat, 8 Feb 2020 14:18:46 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=lysxia AT gmail.com; spf=Pass smtp.mailfrom=lysxia AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua1-f49.google.com
Ironport-phdr: 9a23:vjrblBKWar71cpcUCNmcpTZWNBhigK39O0sv0rFitYgeK/jxwZ3uMQTl6Ol3ixeRBMOHsq4C1rWd6vq8ESxYuNDd6StEKMQNHzY+yuwu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9Kev6AJPdgNqq3O6u5ZLTfx9IhD2gar9uMRm6twrcutQZjId4Kqs8yBTFrmZWd+lZ2GhkIU6fkwvm6sq/4ZJu/T5ct+49+8JFTK73Y7k2QbtEATo8Lms7/tfrtR7NTQuO4nsTTGAbmQdWDgbG8R/3QI7/vjP1ueRh1iaaO9b2Ta0vVjS586hrUh7ohzwZODM/7Wral9Z/jKNfoBKmuhx/34vZa5ybOfZiYq/Qe84RSHFfVchNSSNOHoK8b5MOD+UfO+ZYs5L9rEYKoRenGAWgGP/jxjpOi3Tr36M1zv4hHBnb0gI+EdIAsHfaotv7O6gdU++60KbGwC7fb/5Uwzrx9JTEfx4jrPyKQLl+cdDRyU4qFw7diFuQqJXpPjOP2eQKrmOU7utgWviygGMgrwFwoiOvx8gtiobTnY8VxVXE+j94wIYxP9G3VEl7Ydu9HZZWqiqUNJN2T9s8T210vCs20L4LtJ6hcCQU1pgr2QTTZvODfoSQ/B7vSOecLS1liH57eL+znRe//Va6xuHiVsS51ktBoDBfndnWrH8N0gTe6siZRft5+UeswTOP2BrS6uFAOEw0iLDUJ4M4zr4+mZcetV7PHiDxmEXxg6+Wclsr9vK05OTgZ7Xqvp6cN4lqhQHiKqkihNCzDOAiPgUNX2WX4/qw2KP98UHjT7hHiuU6kqzDv5DbIcQbqLS5AwhQ0os77xa+Dyym0dsZnXYdN19FdxeHgJLoO1HKOvz3EfC/g1G0nDdx2//GJqHhAonKLnXbjLjheq9951dAxwo30NBQ/IlZCqoBIfL2Qk/+rsbUDh4/MwyuwuboEs9x1o0EWTHHPqjMGazUsESI4ednCOmFeJMSoD/xK+ks9ra6hHA/mEQdeqyB1p4WLnmzWPVgdRa3e33p1/MAVHYDuUIOTeWi3FmTSi5Sbl69Wqs94ncwD4fwXtSLfZyknLHUhHTzJZZRfG0TTwnUSS61JbXBYO8FbWepGuEkkjEAUuL8GYoo1BXrqQajjrQ7f6zb/SoXsZ+l399wtbWKxEMCsAdsBsHY6FmjCmR9n2cGXTgzhfktrkl0y1PF2q990aUBSY5joshRWwJ/DqbyivRgAomrCA3Ed9aNDl2hR4f+DA==

You're welcome!

In the first case, you correctly pointed out that mNext is not a constructor but a projection. However, is there a way to rewrite the definition of MonDelayWith with the constructor Build_Monitor (which was automatically generated) and let cofix so that MonDelayWith is guarded and my attempted definition of MonJustBefore works?

This cannot be fixed just by finding a better definition of MonDelayWith or MonOr (there doesn't seem to be one anyway). At least MonSometimes itself has to be rewritten. The most straightforward way leads to your second version. Some less obvious ways consist in somehow encoding nicer mechanisms than guarded recursion in Coq, such as the two I mentioned.

I had never heard of one sized types or clocked type theory. Thanks for the pointers!

Oops, I made a typo. I meant "based on 'sized types'".

Regards,
Li-yao

[Coq-Club] How do I convince Coq that my recursion is guarded?, Agnishom Chattopadhyay, 02/08/2020
- Re: [Coq-Club] How do I convince Coq that my recursion is guarded?, Li-yao Xia, 02/08/2020
  - Re: [Coq-Club] How do I convince Coq that my recursion is guarded?, Agnishom Chattopadhyay, 02/08/2020
    - Re: [Coq-Club] How do I convince Coq that my recursion is guarded?, Li-yao Xia, 02/08/2020