Coq：`Function ... with` syntax

Question

看来，由于w/Inductive和Fixpoint，您可以相互定义Function的w/with。你能给出这个的语法和/或例子吗？我什么都找不到。我想这跟Fixpoint 一样（也没有发现这个）。非工作（但半编译 - 2分最后几行以红色突出显示），例如：

Variable ARG:Type. 
Variable phy inf phyinf: ARG. 
Function Phy (x:ARG): ARG := match x with Inf x => phyinf | _ => phy end 
with Inf (x:ARG): ARG := match x with Phy x => phyinf | _ => inf end. (*Error: Unknown constructor: Inf.*) 

Answer 1

好吧，我想我终于明白你的问题。

确实有一种方法可以相互定义几个Fixpoint。它（略）记录在变体部分here中。

同样，有一种方法可以相互定义几个Inductive类型（记录的here）。

还有一种方法可以相互定义几个Function。但请注意，手动使有关此功能句话：

的Function建设也享有with扩展定义相互递归定义。但是，此功能对非结构递归函数不起作用。

您在半工作示例中遇到的错误与语法无关，但与Function ... with功能也没有关系。错误是你只能在归纳类型上使用模式匹配，并且分支必须以构造函数开始。在你的例子中，ARG不是一个归纳类型，并且Inf不是一个构造函数。我不能真正“改正”你的榜样，因为我没有看到你想表达的内容。这个例子仅仅是为了这个问题吗？在这种情况下，你将其剥离得太少。 PS：我不知道你是否试图做induction-recursion（定义一个递归函数和一个归纳类型）。如果是这种情况，那就不要运气了：Coq还没有这个功能。