coq - Coq 中的 Program Fixpoint 和 Function 有什么区别？

Question

它们似乎有类似的目的。到目前为止，我注意到的一个区别是，虽然Program Fixpoint会接受复合措施，例如{measure (length l1 + length l2) }，Function似乎拒绝这一点，并且只会允许{measure length l1}。

Program Fixpoint严格来说比 更强大Function，还是更适合不同的用例？

Answer 1

这可能不是一个完整的列表，但这是我迄今为止发现的：

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