没有基数参数的类型不等式答案

【问题标题】：Type inequality without cardinality arguments没有基数参数的类型不等式
【发布时间】：2026-02-06 20:55:02
【问题描述】：

如何让 Coq 让我证明句法类型不等式？

否定单价

我已阅读this question 的答案，这表明如果您假设单价，那么证明类型不等式的唯一方法是通过基数参数。

我的理解是——如果 Coq 的逻辑与单价一致，那么它也应该与单价的否定一致。虽然我知道单价的否定实际上是 some 同构类型是不相等的，但我相信应该可以表达 no 同构类型（即t 相同) 相等。

实际上，我希望 Coq 将类型和类型构造函数视为归纳定义，并做一个典型的inversion 风格的参数来说明我的两个非常明显不同的类型不相等。

可以吗？这需要：

这让我觉得弱到足以保持一致。

我有一个多态判断（实际上是带有参数forall X : Type, x -> Prop 的归纳类型），其中X 的选择由判断的构造函数决定。

我想证明，对于X（比如X = nat）的某个选择的所有判断，某些属性成立，但是如果我尝试使用inversion，一些构造函数会给我像nat = string这样的假设（例如）。即使对于具有相同基数的类型，这些类型相等假设也会出现，因此我不能（也不想）提出基数论点来产生矛盾。

我是否应该生成我关心的类型的Inductive 封闭世界编码，并让它成为上述判断的多态变量？

【问题讨论】：

标签： coq

【解决方案1】：

如果你想使用类型不等式，我认为你能做的最好的就是为你关心的每一对类型假设公理：

Axiom nat_not_string : nat <> string.
Axiom nat_not_pair : forall A B, nat <> A * B.
(* ... *)

在 Coq 中，没有一流的方法来讨论归纳定义类型的名称，因此不应该有一种方法可以用单一假设来说明这一系列公理。自然地，您可以在 OCaml 中编写一个 Coq 插件，以在每次定义归纳类型时自动生成这些公理。但是你需要的公理数量在类型数量上呈二次增长，所以我认为很快就会失控。

实际上，在这种情况下，您的“不可思议”的方法可能是最方便的。

（Nit：“如果 Coq 的逻辑与单价一致，那么它也应该与单价的否定一致”。是的，但这只是因为 Coq 不能证明单价。）

【讨论】：

W.r.t the nit：你觉得“真实，但无法证明”和逻辑的一致扩展之间有区别吗？我提到它的主要原因是因为链接的答案谈到单价，好像它绝对正确，而不是用户的选择。
@IsaacvanBakel 第一句话隐含地提到了对逻辑的特定解释，而另一句话是在谈论其句法扩展，它可能验证某些模型并使其他模型无效。我觉得您链接的答案并不是说单价在绝对意义上是正确的，而是说它是在某些逻辑中成立的原则，可能包括 Coq 的扩展。
虽然我意识到您的建议可能是推测性的，并不完全是认真的 - I have made such an axiom-generating plugin。由于我不关心单价，这实际上是稍微可取的，因为它不需要每次我想要一个新类型时都更新封闭世界编码。