对术语...进行抽象会导致术语...类型错误

这是我想证明的：

  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

显而易见的下一步是rewrite L或破坏(partial_index_f (index_f n)。尝试应用重写给我一个错误：

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.

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

我能够使用以下步骤证明它，但我不确定这是最好的方法：

  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 尝试概括这一点，正如您从收到的错误消息中可以看出的那样。

现在，如果你的目标包含以下内容type提到你想要替换的东西，你可能会遇到麻烦，因为这种概括可能会使目标变得错误类型。 （请注意，该类型并不完全出现在目标中，因此 Coq 不会尝试像目标中发生某些事情时那样处理它。）回到您的情况，您的l函数有类型∀ z : nat, partial_index_f (index_f n) ≡ Some z → z < i，其中提到partial_index_f (index_f n)，您要替换的术语。在你的第一个分支match，您将此函数应用于o = Some z你抽象出来的假设。在最初的目标上，o是你想要替换的东西，但是当 Coq 尝试泛化时，两者不再匹配，因此出现错误消息。

我无法尝试自己解决问题，但您通常可以通过概括上下文中提及您要替换的术语的术语来解决此类问题，因为这样它的类型将显示在目标中，与普遍量化变量。如果您的术语是全局定义的，并且您需要它在重写后具有一定的形状，以便能够执行额外的推理步骤，这可能没有帮助，在这种情况下，您可能还必须概括您需要的引理。