1

我被一个问题困住了一段时间，为此我得出了一个较小的独立示例：

Axiom f : nat -> Set.

Goal forall (n : nat) (e : n = n) (x : f n),
  match e in _ = _n return f _n -> Prop with
  | Logic.eq_refl => fun v : f n => v = x
  end x.

现在，如果您尝试destruct e，您会收到以下错误消息：

Error: Abstracting over the terms "n0" and "e" leads to a term
"fun (n0 : nat) (e : n0 = n0) =>
 forall x : f n0,
 match e in (_ = _n) return (f _n -> Prop) with
 | Logic.eq_refl => fun v : f n0 => v = x
 end x" which is ill-typed.

在挠了一阵头之后，我无法弄清楚那个术语中的错误类型......所以我尝试了这个：

Definition illt :=
  fun (n : nat) (e : n = n) =>
  forall x : f n,
  match e in _ = _n return f _n -> Prop with
  | Logic.eq_refl => fun v : f n => v = x
  end x.

Coq 接受它，在 type forall n : nat, n = n -> Prop。

那么，此错误消息有什么问题，我该如何解决/调整我的初始目标？

顺便说一句，这都是coq8.3。如果这是 8.4 中修复的问题，请告诉我，我很抱歉！:)

编辑：为了解决 Robin Green 的评论，这里是Set Printing All错误消息的版本：

Error: Abstracting over the terms "n0" and "e" leads to a term
"fun (n0 : nat) (e : @eq nat n0 n0) =>
 forall x : f n0,
 match e in (@eq _ _ _n) return (f _n -> Prop) with
 | eq_refl => fun v : f n0 => @eq (f n0) v x
 end x" which is ill-typed.

这是一个类型良好的术语，没有什么是隐含的。

4

1 回答 1

3

这是该问题的可能解释。也可以使用定理来描述构造模式匹配构造时发生的情况。这是我对您案例中使用的定理的看法。

Check eq_rect.

eq_rect
 : forall (A : Type) (x : A) (P : A -> Type),
   P x -> forall y : A, x = y -> P y

因此，当对等式进行模式匹配时，您必须提供一个公式 P 参数化任何 y恰好可证明等于 的值x。直观地说，你应该可以用 替换你的模式匹配表达式apply eq_rect，但是应该出现的属性 P 超出了 Coq 可以猜测的范围，因为x公式中的每次出现都必然是类型f n，不能只输入类型f mwhere m = n。错误消息没有说，这可能是一个错误。

为了执行您的证明，我建议使用相等的证明在某些类型的类型中是唯一的并且nat属于此类的事实。这在文件 Eqdep_dec 中处理。

Require Eqdep_dec Arith.

现在你的证明很容易通过。

Goal forall n (x : f n) (e : n = n),
  match e in _ = _n return f _n -> Prop with
  | Logic.eq_refl => fun v : f n => v = x
  end x.
intros n x e; replace e with (eq_refl n).
  reflexivity.
apply Eqdep_dec.UIP_dec, eq_nat_dec.
Qed.

现在，这个解决方案可能会让人感到不满意。这UIP_dec是从哪里来的？UIP 代表身份证明的唯一性，不幸的是，不能保证所有任意类型的此属性。对于可以确定相等性（如 表示UIP_dec）的所有类型，例如 ，它都得到保证nat。

于 2013-02-18T18:14:19.193 回答