coq - 我们可以在 Coq 中定义递归定义吗？

Question

我知道 Coq 允许定义相互递归的归纳类型。但是有没有办法在 Coq 中编写递归定义？

例如，我想写一个定义为：

Definition myDefinition A := forall B C, (myDefinition B) \/ (A = C).

上述定义中的重要部分是myDefinition B，它在另一个参数上递归调用相同的定义。在 Coq 中可以做到这一点吗？

Answer 1

您可以使用Fixpoint而不是Definition. 如果您想了解更多信息，我鼓励您查看文档。

Fixpoint myDefinition A := 
  forall B C, (myDefinition B) \/ (A = C).

请注意，上述内容不会被 Coq 接受为终止，因此不会被视为有效定义。再一次，文档应该解释你可以用例子做什么，不能做什么。

---

编辑

如果您的定义应该是一种类型，那么您也可以将其定义为归纳类型。

Inductive myDefinition (A : Prop) : Prop :=
| myDef : forall B C, (myDefinition B) \/ (A = C) -> myDefinition A.

这里我们说建立一个证明myDefinition A就足够证明了forall B C, (myDefinition B) \/ (A = C)。这就是你想要的。但是，您可能很难证明这一点，但是您的具体情况可能有所不同。