Coq中可判定相等性的Set与Prop表述差异及相关疑问

二者的核心差异 #

• 所属宇宙与计算能力不同：
  • forall x y : A, x = y \/ x <> y 是Prop类型的命题，仅声明「任意两个A类型元素相等或不相等」的逻辑成立，没有携带可用于计算的信息，在代码提取阶段会被完全擦除，无法用于代码的分支判断逻辑。
  • forall x y : A, {x = y} + {x <> y} 是Set类型的可计算函数，接收任意两个A类型元素作为输入，会明确返回二者相等的证明、或是二者不等的证明，具备完整的计算能力，提取代码时会生成为真实的相等性判断函数，可直接用于分支逻辑。
• 推导关系：你之前的理解方向相反，只能从后者推导前者，Coq标准库已经提供了从{P} + {Q}到P \/ Q的自动转换；反向推导不成立，因为Prop层面的逻辑断言没有可执行的计算内容，不可能仅通过「要么相等要么不等」的逻辑声明，凭空构造出能实际判断二者是否相等的可执行函数。

符合前者但不符合后者的类型实例 #

确实存在这类类型，最典型的两个例子：

• Coq标准库的实数类型R：基于经典逻辑的排中律可以证明forall r1 r2:R, r1=r2 \/ r1<>r2成立，但实数相等性是理论上不可判定的，不存在能对任意两个实数判断是否相等的算法，因此不可能构造出{r1=r2} + {r1<>r2}的实例。
• 图灵机类型：同样可以用经典排中证明任意两个图灵机要么相等要么不等，但图灵机相等等价于停机问题，不可判定，因此也无法构造Set层面的判定函数。

这也是Eqdep_dec模块会区分两类前提的原因：仅需要逻辑证明的结论用Prop层面的前提就足够，而需要依赖相等性判定做分支计算、或是要提取为可执行代码的结论，就要求提供Set层面的可判定相等性实例。

可判定相等性的定义 #

标准语境下的「可判定相等性（decidable equality）」确实指的是{x = y} + {x <> y}的版本。因为构造主义/类型论语境下的「可判定」本身就要求「存在可执行算法给出命题的判定结果」，必须有计算内容，Prop层面的或命题只是经典逻辑下的排中律应用，不满足「可判定」的定义。

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