如何在Coq中定义相互递归类型？遇语法错误求助

你遇到的语法错误核心原因是：Coq的Inductive ... with结构仅支持归纳类型之间的相互递归定义，而你在with分支里直接放入了非归纳类型的定义（C是函数类型、E是list D的类型别名），这违反了语法规则。

修正方案 #

将非归纳类型的定义从Inductive ... with结构中抽离，单独用Definition声明，仅在with中保留真正的相互递归归纳类型（A、B、D、F）。

示例代码

-- 先定义相互递归的归纳类型集合
Inductive A : Type :=
  | a : F -> A
  (* 其他无关构造器 *)
with B : Type :=
  | b : xxx -> A -> B -> B
  (* 其他无关构造器 *)
with D : Type :=
  | d : C -> xxx -> zzz -> B -> D
  (* 其他无关构造器 *)
with F : Type :=
  | f : E -> F
  (* 其他无关构造器 *)
.

-- 单独定义非归纳类型C和E
Definition C : Type := xxx -> yyy.
Definition E : Type := list D.

特殊情况调整

如果C的定义必须早于D（比如D的构造器直接依赖C），可以先单独声明C，再定义归纳类型：

Definition C : Type := xxx -> yyy.

Inductive A : Type :=
  | a : F -> A
  (* 其他无关构造器 *)
with B : Type :=
  | b : xxx -> A -> B -> B
  (* 其他无关构造器 *)
with D : Type :=
  | d : C -> xxx -> zzz -> B -> D
  (* 其他无关构造器 *)
with F : Type :=
  | f : E -> F
  (* 其他无关构造器 *)
.

Definition E : Type := list D.

内容的提问来源于stack exchange，提问作者Cs_J