Coq定义带列表命题的归纳类型时遇非严格正出现错误

嘿，你碰到的这个问题其实是Coq的**严格正性（Strict Positivity）**规则在起作用，咱们一步步拆解来看：

先回顾能正常运行的定义 #

你已经写出了两种完全合法的归纳类型定义：
第一种直接把list Foo作为构造子的参数：

Require Import Coq.Lists.List.
Import ListNotations.
Inductive Foo := MkFoo : list Foo -> Foo.

第二种用forall显式量化参数，本质和第一种是等价的：

Inductive Foo := MkFoo : forall (l : list Foo), Foo.

为什么带l <> []约束的定义会失败？ #

当你给构造子加上l <> []这个命题约束后：

Inductive Foo := MkFoo : forall (l : list Foo), l <> [] -> Foo.

Coq就抛出了Non strictly positive occurrence of "Foo" in "forall l : list Foo, l <> [] -> Foo"的错误，核心原因是：

• Coq的严格正性规则要求：归纳类型Foo只能出现在构造子类型的正位置——简单来说，Foo不能出现在箭头->的左侧（也就是否定、蕴含的前提部分）。
• 这里的l <> []其实是list Foo -> False的语法糖，展开后你会发现Foo出现在了箭头的左侧位置，直接违反了严格正性要求。这个规则是Coq用来保证归纳类型良基的关键，能避免循环定义导致的逻辑矛盾。

两种可行的解决思路 #

1. 用非空列表类型替代普通列表 #

你可以自定义一个非空列表类型，这样就不需要额外的命题约束，天然满足非空要求，也符合严格正性规则：

Require Import Coq.Lists.List.
Import ListNotations.

(* 自定义非空列表类型 *)
Inductive ne_list (A : Type) :=
| ne_cons : A -> list A -> ne_list A.

(* 用非空列表作为构造子参数 *)
Inductive Foo := MkFoo : ne_list Foo -> Foo.

2. 把约束移到归纳类型的性质中 #

如果你一定要用普通列表，可以先定义不带约束的归纳类型，再单独用谓词描述“合法的Foo实例满足列表非空”：

Require Import Coq.Lists.List.
Import ListNotations.

Inductive Foo := MkFoo : list Foo -> Foo.

(* 定义谓词标记合法的Foo *)
Definition valid_Foo (f : Foo) : Prop :=
  match f with
  | MkFoo l => l <> []
  end.

之后在做证明时，只针对满足valid_Foo的Foo实例进行推理就可以了。

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