不带基数参数的类型不等式

Question

怎样才能让Coq让我证明句法类型的不等式？

否定单价

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

我的理解是-如果Coq的逻辑与单价一致，它也应该与单价的否定一致。虽然我知道单价的否定实际上是某些同构类型是不相等的，但我认为应该可以表示没有同构类型(不完全相同)是相等的。

类型构造函数的不等式

实际上，我希望Coq将类型和类型构造函数作为归纳定义，并执行一个典型的inversion-style参数来说明我的两个非常不同的类型是不相等的。

能办到吗？这需要：

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插件，以便在定义归纳类型时自动生成这些公理。但是你需要的公理的数量在类型的数量上呈二次增长，所以我认为很快就会失控。

实际上，在这种情况下，你的“不可想象”的方法可能是最方便的。

(Nit：“如果Coq的逻辑与单价一致，它也应该与单价的否定一致”。是的，但仅仅是因为Coq不能证明是单价。)