Coq中是否存在支持bool类型的可判定集合库？

核心结论 #

• 用S : U -> bool表示可判定集合是可行的，但仅当类型U对应的集合成员关系可判定时成立——换句话说，只要能对任意u : U机械地判断它是否属于目标集合，就能用这种布尔函数形式建模。
• 这种表示和U -> Prop的关系是：每个S : U -> bool都能对应一个U -> Prop（即fun u => S u = true），但反过来，不是所有U -> Prop都能转成U -> bool——只有那些可判定的谓词才行。

具体解释 #

在Coq这类证明辅助工具的语境下：

• U -> Prop是最通用的集合表示，涵盖所有可能的子集（包括不可判定的，比如和停机问题相关的集合）。
• U -> bool是它的子集，仅代表可判定集合——因为布尔函数的求值是可计算的，给定任意u : U，运行S u就能得到明确的true/false结果，直接完成成员判定。

子集计算的实现思路 #

如果你的“给定U类型元素集合”是指可枚举的有限集合（比如列表list U），计算它与S : U -> bool的交集非常直接：遍历列表，对每个元素应用S，只保留返回true的元素。示例代码如下：

Definition filter {U : Type} (S : U -> bool) (l : list U) : list U :=
  fold_right (fun u acc => if S u then u :: acc else acc) nil l.

这个函数返回的列表就是原集合中属于S的子集。

如果是无限集合，无法直接“计算”出完整的子集，但可以用U -> bool结合原集合的谓词来描述这个交集（比如fun u => (u 属于原集合) /\ S u = true），而因为S是可判定的，这个复合谓词同样具备可判定性。

关键注意点 #

不是所有类型U都能让所有U -> Prop转成U -> bool。比如当U是函数类型（比如nat -> nat）时，存在不可判定的谓词（比如“这个函数是否在所有输入上都返回0”），这类谓词就没法写成布尔函数形式——因为不存在通用算法能对任意函数做出这类判断。

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