如何解决Coq中无效类型等于的目标？

Question

我的证明脚本给了我愚蠢的类型平等,nat = bool或者 nat = list unit我需要用来解决相互矛盾的目标.

在正常的数学中,这将是微不足道的.鉴于集合bool := { true, false }, nat := { 0, 1, 2, ... }我知道true ? bool,但是true ? nat,因此bool ? nat.在Coq,我甚至不知道如何陈述true :? nat.

题

有没有办法证明这些平等是错误的？或许,这不可能吗？

(编辑:删除了一长串失败的attemts,仍然可以在历史上看到.)

Answer 1

tl; dr基数参数是显示不等等类型的唯一方法.你可以通过一些反思更有效地自动化基数论证.如果你想更进一步,通过构建一个宇宙给你的类型一个句法表示,确保你的证明义务被构造为表示的句法不等式而不是类型的语义不等式.

同构作为平等

人们普遍认为(并且甚至可能存在某种证据),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)

但是你仍然可以通过这种方式构建宇宙来完成很多工作.例如,人们可以为这样的宇宙配备计算有效的伸展相等.