types - 如何解决 Coq 中无效类型相等的目标？

Question

我的证明脚本给了我愚蠢的类型相等性，比如 nat = bool或者nat = list unit我需要用它来解决相互矛盾的目标。

在普通数学中，这将是微不足道的。给定集 bool := { true, false }和nat := { 0, 1, 2, ... }我知道true ∈ bool ，但是 true ∉ nat ,
因此 bool ≠ nat .在 Coq 中，我什至不知道如何表述 true :̸ nat .

题

有没有办法证明这些等式是错误的？或者，这是不可能的吗？

(编辑:删除了一长串失败的尝试，仍然可以在历史记录中查看。)

Answer 1

tl;博士 基数参数是显示类型不等的唯一方法。您当然可以通过一些反射(reflection)更有效地自动化基数参数。如果你想更进一步，通过构造一个宇宙来给你的类型一个句法表示，确保你的证明义务被构建为表示的句法不等式，而不是类型的语义不等式。

作为等式的同构

人们普遍认为(甚至可能在某处证明了这一点)，Coq 的逻辑与同构集在命题上相等的公理一致。事实上，这是 Vladimir Voevodsky 的Univalence Axiom 的结果，人们现在玩得很开心。我必须说，它是一致的(在没有 typecase 的情况下)似乎非常合理，并且可以构造一个计算解释，通过在任何给定时刻插入任何需要的同构组件，以某种方式在相等类型之间传输值。

如果我们假设这样的公理是一致的，我们就会发现逻辑中的类型不等式只能通过驳斥类型同构的存在来成立。因此，您的部分解决方案至少在原则上是可行的。可枚举性是显示非同构的关键。我不确定 nat = (nat -> nat) 的状态可能是，但从系统外部可以清楚地看出，nat -> nat 的每个居民有一个范式，并且存在可数的许多范式:至少有可能存在一致的公理或反射原则，它们使逻辑更具内涵并验证该假设。

自动化基数参数

我可以看到你可以采取两个步骤来改善目前的情况。不太激进的步骤是通过更好地使用反射来改进您的通用技术，以制作这些基数参数。您很适合这样做，因为一般来说，您希望证明有限集与某个更大的集不同。假设我们有一些 DList A 的概念，A 的不同元素列表.如果你能构建一个详尽的DList A和更长的 DList B ，那么你可以反驳 A = B .

归纳递归有一个可爱的 DList 定义，但 Coq 没有归纳递归。幸运的是，这是我们可以通过仔细使用索引来模拟的定义之一。原谅我的非正式语法，但让我们有

Parameters
  A   : Set
  d   : A -> A -> bool
  dok : forall x y, d x y = true -> x = y -> False

那是 d为“与众不同”。如果一个集合已经有可判定的相等，你可以用 d 装备它非常简单地。大一套可以配够用d为了我们的目的，没有太多的工作。实际上，这是关键的一步:遵循 SSReflect 团队的智慧，我们通过与 bool 合作，利用我们域的小优势。而不是 Prop ，并使计算机完成繁重的工作。

现在，让我们有

DListBody : (A -> bool) -> Set

其中索引是列表的新鲜度测试

dnil  : DListBody (const true)       (* any element is fresh for the empty list *)
dsnoc : forall f, (xs : DListBody f) -> (x : A) -> is_true (f x) ->
          DListBody (fun y => f y /\ d x y)

如果你愿意，你可以定义 DList包装DListBody存在的。不过，也许这实际上隐藏了我们想要的信息，因为要详尽地展示这样的事情是这样的:

Exhaustive (f : A -> bool)(mylist : DListBody f) = forall x : A, is_false (f x)

因此，如果您可以为有限枚举写出 DListBody，则可以仅通过带有琐碎子目标的案例分析来证明它是详尽无遗的。

然后，您只需要进行一次归类论证。当您想反驳类型之间的相等性时(假设您已经有合适的 d 候选者)，您可以详尽地枚举较小的列表并从较大的列表中展示更长的列表，仅此而已。

在宇宙中工作

更激进的选择是质疑你为什么要实现这些目标，以及它们是否真的意味着你想要的。类型应该是什么，真的吗？这个问题有多种可能的答案，但至少在某种意义上它们是“基数”是公开的。如果您想将类型视为更具体和句法，如果它们是由不同的结构构建的，那么您可能需要通过在 Universe 中工作来为类型配备更具体的表示。您为类型定义了“名称”的归纳数据类型，以及将名称解码为类型的方法，然后根据名称重新构建您的开发。您应该发现名称的不等式遵循普通的构造函数区分。

问题在于 Coq 中的宇宙构造可能有点棘手，同样是因为不支持归纳递归。这在很大程度上取决于您需要考虑的类型。也许你可以归纳地定义一些 U : Set然后实现一个递归解码器 T : U -> Set .对于简单类型的宇宙来说，这当然是合理的。如果你想要一个依赖类型的世界，事情就会变得有点麻烦。你至少可以做这么多

U : Type   (* note that we've gone up a size *)
NAT : U
PI : forall (A : Set), (A -> U) -> U

T : U -> Set
T NAT = nat
T (PI A B) = forall (a : A), T (B a)

但请注意 PI 的域在 Set 中未编码，不在 U .归纳递归 Agdans 可以克服这个问题，定义 U和 T同时

U : Set   (* nice and small *)
NAT : U
PI : forall (A : U), (T A -> U) -> U   (* note the use of T *)

T : U -> Set
T NAT = nat
T (PI A B) = forall (a : T A), T (B a)

但 Coq 不会。同样，解决方法是使用索引。这里的成本是U不可避免地很大。

U : Set -> Type
NAT : U nat
PI : forall (A : Set)(B : A -> Set),
       U A -> (forall a, U (B a)) -> U (forall a, B a)

但是你仍然可以通过以这种方式构建的宇宙完成很多事情。例如，可以为这样一个宇宙配备一个计算有效的 extensional equality .