Coq 中的 Program Fixpoint 和 Function 有什么区别？答案

【问题标题】：What's the difference between Program Fixpoint and Function in Coq?Coq 中的 Program Fixpoint 和 Function 有什么区别？
【发布时间】：2017-06-17 15:24:28
【问题描述】：

它们似乎有相似的目的。到目前为止我注意到的一个区别是，虽然Program Fixpoint 将接受像{measure (length l1 + length l2) } 这样的复合度量，但Function 似乎拒绝了这一点，并且只允许{measure length l1}。

Program Fixpoint 是否比Function 更强大，或者它们更适合不同的用例？

【问题讨论】：

顺便说一句，Coq v8.7 roadmap 说他们的实现将被合并。
这是个好问题，如果您需要详细的答案，我建议您去 Coq 的 gitter，因为了解它的人不会阅读 SO AFAIK； Function 和 Program 的实现是由不同的人在不同的环境中完成的，因此它们的特性集确实不是另一个特性的子集。有计划将它们合并到一个新的“方程式”插件中，但这不会在 8.7 中发生，即使已经取得了很多进展。话虽如此，我认为如果您关心与未来 Coq 版本的兼容性，通常最好使用 Program。

标签： coq totality

【解决方案1】：

这可能不是一个完整的列表，但这是我目前发现的：

正如您已经提到的，Program Fixpoint 允许度量查看多个参数。
Function 创建一个 foo_equation 引理，可用于使用其 RHS 重写对 foo 的调用。对于避免Coq simpl for Program Fixpoint 之类的问题非常有用。
在某些（简单？）情况下，Function 可以定义一个foo_ind 引理，以沿foo 的递归调用结构执行归纳。同样，对于证明 foo 的事情非常有用，而无需在证明中有效地重复终止论点。
Program Fixpoint 可以被欺骗支持嵌套递归，请参阅 https://stackoverflow.com/a/46859452/946226。这也是为什么Program Fixpoint 可以define the Ackermann 起作用而Function 不能起作用的原因。

【讨论】：

用Function定义阿克曼函数似乎也是不可能的，但是Program Fixpointcan do it。
谢谢，已将其添加到答案中。