7

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

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

问题

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

（Ed.：删除了一长串失败的尝试，仍然可以在历史记录中查看。）

4

2 回答 2

8

tl; dr基数参数是显示类型不相等的唯一方法。您当然可以通过一些反思更有效地自动化基数论证。如果您想走得更远，请通过构建一个 Universe 为您的类型提供语法表示，确保您的证明义务被框架为表示的语法不等式，而不是类型的语义不等式。

作为平等的同构

人们普遍认为（甚至可能在某处有证明）Coq 的逻辑与同构集合在命题上相等的公理是一致的。事实上，这是 Vladimir Voevodsky 的 Univalence Axiom 的结果，目前人们对此非常感兴趣。我必须说，它是一致的（在没有类型大小写的情况下）似乎非常合理，并且可以构造一种计算解释，通过插入任何给定时刻所需的同构的任何组件，以某种方式在相等类型之间传输值。

如果我们假设这样一个公理是一致的，我们会发现逻辑中的类型不等式仅通过反驳类型同构的存在才能成立。结果，您的部分解决方案至少在原则上是它所在的位置。可枚举性是显示非同构的关键。我不确定它的状态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

其中 index 是列表的新鲜度测试

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)

But you can still get a lot of stuff done with a universe built that way. For example, one can equip such a universe with a computationally effective extensional equality.

于 2012-09-07T09:22:10.893 回答
1

扩展部分解

作为参考，这是我的证明nat = bool -> False。（它很长，但我希望很容易看到这个证明的一般结构。）

Goal nat = bool -> False.
  (* For any two types, if they are actually identical, the identity is an
     isomorphism. *)
  assert (forall (T U : Set), T = U ->
              exists (f : T -> U) (g : U -> T),
              (forall t, (g (f t)) = t) /\ (forall u, (f (g u)) = u))
          as Hiso
  by (intros T U H; rewrite H; exists (@id U); exists (@id U);
          split; intro; reflexivity).
  (* our nat = bool *)
  intro HC.
  (* combining the facts gives an iso between nat and bool *)
  pose proof (Hiso nat bool HC); clear HC Hiso.
  inversion H as [phi [phi_inv [Hl Hr]]]; clear H Hr.
  (* this breaks because ||bool|| = 2 while ||nat|| > 2 -- we get collisions *)
  assert (forall m n o,
              phi m = phi n \/ phi n = phi o \/ phi m = phi o)
   by (intros m n o;
        case (phi m); case (phi n); case (phi o); clear; tauto).
  (* building the collision for 0, 1 and 2 *)
  pose proof (H 0 1 2) as HC; clear H.
  (* (false) identity preservation for 0, 1, 2 *)
  pose proof (Hl 0) as H0; pose proof (Hl 1) as H1;
  pose proof (Hl 2) as H2; clear Hl.
  (* case analysis on phi calls yields equalities on non-equal numbers... *)
  destruct (phi 0); destruct (phi 1); destruct (phi 2);
  (* ...rewriting leads to an equality '0 = 2' or '0 = 1' or '1 = 2'... *)
  try (rewrite H2 in H0); try (rewrite H1 in H0); try (rewrite H2 in H1);
  (* ...which can be used to solve by constructor inequality *)
  try inversion H0; inversion H1.
Qed.

如您所见，这实际上不适用于大型有限类型（即使是自动化的）——这些术语太大了。对此的任何改进都会很棒。

于 2012-09-01T01:59:53.323 回答