摘要这个术语......会导致一个术语......这是一个错误的类型

Question

这是我想要证明的:

  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.

Answer 1

在Coq的理论中,当您使用方程执行重写时,您必须对要替换的等式的一侧进行推广.在您的情况下,您想要替换partial_index_f (index_f n),因此Coq尝试概括,因为您可以从您收到的错误消息中得知.

现在,如果您的目标包含某些类型提及您想要替换的内容,那么您可能会遇到麻烦,因为这种泛化可能会使目标变得不合适.(请注意,该类型并不完全出现在目标中,因此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试图概括时,两者不再匹配,因此错误消息.

我不能尝试自己解决这个问题,但是你可以通过在你的上下文中提及你要替换的术语来概括这个问题来解决这个问题,因为那时它的类型将显示在目标中,与普遍量化的变量.如果您的术语是全局定义的,并且您需要在重写后具有某种形状以便能够执行其他推理步骤,这可能无济于事,在这种情况下,您可能必须对您需要的词汇进行概括. .