coq - 没有基数参数的类型不等式

Question

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

否定单价

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

我的理解是——如果Coq的逻辑符合单价，那么它也应该符合单价的否定。虽然我知道单价的否定实际上是一些同构类型是不相等的，但我相信应该可以表达没有同构类型(那是' t identical) 是相等的。

类型构造函数的不等式

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

可以吗？这需要是:

1. 可用于具体类型，即没有类型变量等
2. 不一定是可判定的

这让我觉得不够稳定，无法保持一致。

上下文

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

我想证明，对于 X 的特定选择(例如 X = nat)的所有判断，某些属性都成立，但如果我尝试使用 inversion，一些构造函数给我假设，例如 nat = string(例如)。这些类型相等性假设甚至出现在具有相同基数的类型中，所以我不能(也不想)使基数参数产生矛盾。

不可思议的...

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

Answer 1

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

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

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

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

(尼特:“如果 Coq 的逻辑与单价一致，那么它也应该与单价的否定一致”。是的，但这只是因为 Coq 无法证明单价。)