抽象导致术语不良类型...但类型正确 [英] Abstracting leads to a term ill-typed... yet well-typed

问题描述

我在一个问题上停留了一段时间，为此我导出了一个较小的独立示例:

I was stuck on a problem for a while, for which I derived a smaller standalone example:

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.

现在，如果您尝试破坏e ，则会收到以下错误消息:

Now, if you try to destruct e, you get the following error message:

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.

挠了一下头后，我不知道那个词是什么错字……所以我尝试了这个:

After scratching my head for a while, I couldn't figure out what was ill-typed in that term... So I tried this:

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接受它，类型为 forall n:nat，n = n->道具.

And Coq accepts it, at type forall n : nat, n = n -> Prop.

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

So, what is wrong with this error message, and how could I solve/tweak my initial goal?

顺便说一句，这都是coq8.3.如果这在8.4中已解决，请告诉我，我深表歉意！:)

BTW this is all coq8.3. If this is something fixed in 8.4, please tell me, and my apologies! :)

要解决Robin Green的评论，这是错误消息的 Set Printing All 版本:

To address Robin Green's comment, here is the Set Printing All versions of the error message:

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.

这是一个类型明确的术语，没有任何隐含的内容.

It is a well-typed term, and nothing is implicit.

推荐答案

以下是对该问题的可能解释.构造模式匹配构造时会发生什么，也可以使用一个定理来描述.这是我对您的案例中所使用的定理的看法.

Here is a possible explanation of the problem. What happens when constructing a pattern-matching construct can also be described using a theorem. Here is my view of the theorem that is being used in your case.

Check eq_rect.

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

因此，当在等式上进行模式匹配时，您必须根据任何值 y 设置参数P，该值恰好等于 x .直观上，您应该能够用 apply eq_rect 替换模式匹配表达式，但是应该出现的属性P超出了Coq可以猜测的范围，因为每次出现公式中的x 必然是 fn 类型，而不能只是 fm 类型，其中 m = n .错误消息没有说明，这可能是一个错误.

So when pattern matching on an equality, you have to provide a formula P parametrized on any value y that happens to be provably equal to x. Intuitively, you should be able to replace your pattern-matching expression by apply eq_rect, but the property P that should come up there is beyond the reach of what Coq can guess, because every occurrence of x in your formula is bound to be in type f n and cannot just be in type f m where m = n. The error message does not say that, it is probably a mistake.

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

To perform your proof, I suggest rather to use the fact that proofs of equality are unique in certain classes of types, and nat belongs to such a class. This is treated in the file Eqdep_dec.

Require Eqdep_dec Arith.

现在，您的证明很容易通过.

Now your proof goes through quite easily.

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 .

Now, this solution may feel unsatisfactory. Where does this UIP_dec come from? UIP stands for uniqueness of identity proofs and unfortunately, this property is not guaranteed for all arbitrary types. It is guaranteed for all types where equality is decidable (as expressed by UIP_dec), for instance nat.

这篇关于抽象导致术语不良类型...但类型正确的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！