我知道 Coq 允许定义相互递归的归纳类型。但是有没有办法在 Coq 中编写递归定义？
例如，我想写一个定义为：
Definition myDefinition A := forall B C, (myDefinition B) \/ (A = C).
上述定义中的重要部分是myDefinition B，它在另一个参数上递归调用相同的定义。在 Coq 中可以做到这一点吗？
【问题讨论】：
A 用作一条数据（如数字或字符串），如果是这种情况，则递归受到数据类型的归纳结构的严格限制。跨度>
标签： coq theorem-proving coqide
您可以使用Fixpoint 代替Definition。如果您想了解更多信息，我鼓励您查看documentation。
Fixpoint myDefinition A :=
forall B C, (myDefinition B) \/ (A = C).
请注意，上述内容不会被 Coq 接受为终止，因此不会被视为有效定义。 documentation 应该再次说明您可以通过示例做什么和不能做什么。
编辑
如果你的定义应该是一个类型，那么你也可以将它定义为一个归纳类型。
Inductive myDefinition (A : Prop) : Prop :=
| myDef : forall B C, (myDefinition B) \/ (A = C) -> myDefinition A.
这里我们说要建立myDefinition A 的证明，证明forall B C, (myDefinition B) \/ (A = C) 就足够了。这就是你想要的。
但是，您可能很难证明这一点，但您的具体情况可能有所不同。
【讨论】：