对术语...的抽象会导致术语...类型错误 [英] Abstracting over the term ... leads to a term ... which is ill-typed

问题描述

以下是我要证明的内容：

Here is what I am trying to prove:

  A : Type
  i : nat
  index_f : nat → nat
  n : nat
  ip : n < i
  partial_index_f : nat → option nat
  L : partial_index_f (index_f n) ≡ Some n
  V : ∀ i0 : nat, i0 < i → option A
  l : ∀ z : nat, partial_index_f (index_f n) ≡ Some z → z < i
  ============================
   V n ip
   ≡ match
       partial_index_f (index_f n) as fn
       return (partial_index_f (index_f n) ≡ fn → option A)
     with
     | Some z => λ p : partial_index_f (index_f n) ≡ Some z, V z (l z p)
     | None => λ _ : partial_index_f (index_f n) ≡ None, None
     end eq_refl

步骤是重写L 或销毁（partial_index_f（index_f n）。尝试应用重写会给我一个错误：

The obvious next step is either rewrite L or destruct (partial_index_f (index_f n). Trying to applying rewrite gives me an error:

Error: Abstracting over the term "partial_index_f (index_f n)"
leads to a term
"λ o : option nat,
 V n ip
 ≡ match o as fn return (o ≡ fn → option A) with
   | Some z => λ p : o ≡ Some z, V z (l z p)
   | None => λ _ : o ≡ None, None
   end eq_refl" which is ill-typed.

我不明白是什么导致了这个问题，我也想了解我一般如何处理它。

I do not understand what is causing this problem. I also would like to understand how I can deal with it in general.

我可以使用以下步骤来证明这一点，但是我不确定这是最好的方法：

I was able to prove it using the following steps, but I am not sure this is the best way:

  destruct (partial_index_f (index_f n)).
  inversion L.
  generalize (l n0 eq_refl).
  intros. subst n0.
  replace l0 with ip by apply proof_irrelevance.
  reflexivity.
  congruence.

推荐答案

按照Coq的理论，当您使用等式，您必须对要替换的等式进行概括。在您的情况下，您想替换 partial_index_f（index_f n），因此Coq试图将其概括化，正如您从收到的错误消息中所知道的。

In Coq's theory, when you perform a rewrite with an equation, you have to generalize over the side of the equation that you want to replace. In your case, you want to replace partial_index_f (index_f n), so Coq tries to generalize that, as you can tell from the error message you got.

现在，如果目标中包含 type 所要替换的内容，则可能会遇到麻烦，因为这种泛化可能会使目标生病型。 （请注意，该类型并非完全出现在目标中，因此Coq不会像目标中发生某种情况那样尝试处理它。）回到您的情况，您的 l 函数的类型为∀z：nat，partial_index_f（index_f n）≡一些z→z< i ，其中提到要替换的术语 partial_index_f（index_f n）。在匹配的第一分支中，将此函数应用于抽象的 o =某些z 假设。最初的目标是要替换 o ，但是当Coq尝试推广时，两者不再匹配，因此出现错误消息。

Now, if your goal contains something whose type mentions the thing that you want to replace, you might run into trouble, because this generalization might make the goal become ill-typed. (Notice that that type does not exactly occur in the goal, hence Coq does not try to deal with it like it does when something occurs in the goal.) Going back to your case, your l function has type ∀ z : nat, partial_index_f (index_f n) ≡ Some z → z < i, which mentions partial_index_f (index_f n), the term you want to replace. In the first branch of your match, you apply this function to the o = Some z hypothesis that you abstracted over. On the original goal, o was the thing you wanted to replace, but when Coq tries to generalize, the two do not match anymore, hence the error message.

我无法自行解决问题，但通常可以通过在上下文中概括提及要替换的术语的方式来解决此类问题。其类型将显示在目标中，并与通用量化变量相关联。如果您的术语是全局定义的，并且在重写后需要使其具有一定的形状以便能够执行其他推理步骤，则这可能无济于事，在这种情况下，您可能还必须归纳一下所需的引理

I can't try to fix the problem on my own, but you can solve issues like this usually by generalizing over the term in your context that mentions the term you are replacing, because then its type will show in the goal, associated to a universally quantified variable. This might not help if your term is defined globally and you need it to have a certain shape after the rewrite in order to be able to perform additional reasoning steps, in which case you will probably have to generalize over the lemmas that you need as well.

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