在 Coq 中定义相互递归类型？

Question

假设我有 A、B、C、D、E、F 类型。 A 的构造函数之一采用 F 类型的参数； B 的构造函数需要 A，D 的构造函数需要 C 和 A 类型的参数，E 需要 D，F 需要 E。我应该如何定义它们？

我在网上搜索发现我可以使用关键字“with”来链接它们，但这对我不起作用。类型 C 是介于前两种类型之间的函数类型，不属于上面列出的 6 种类型中的任何一种。当我尝试使用“with”时，C 定义中的箭头以某种方式突出显示，并向我显示消息语法错误：“。”预计在 [gallina] 之后（在 [vernac_aux] 中）。

我的代码大致遵循这个结构：

Inductive A : Type :=
  | a : F -> A
  | ... (other constructors unrelated to the problem)
 
with B : Type :=
  | b: xxx -> A -> B -> B
  | ...

with C : Type := xxx -> yyy
with D : Type := 
  | d : C -> xxx -> zzz -> B -> D
  | ...
with E := list D
with F : Type :=
  | f : E -> F
  | ...
.

Answer 1

对于 C，你必须为构造函数提供 names，并且构造函数应该接受一些（零个或多个）参数并返回 C 类型的内容。

所以 C 应该是这样的

Inductive C : Type := c1 :(xxx -> yyy) -> C.

E 也一样。

Variable (xxx yyy zzz :Type).

Inductive A : Type :=
  | a : F -> A
 
with B : Type :=
  | b: xxx -> A -> B -> B

with C : Type := c1 :(xxx -> yyy) -> C

with D : Type := 
  | d : C -> xxx -> zzz -> B -> D

with E := e1: list D -> E
with F : Type :=
  | f : E -> F
.