Coq Vector 在证明模式下爆炸？

Question

关于 Coq 向量的一些机械问题。在我的证明中，我有

input: Vector.t nat 1
==================================
compliacted_fixpoint_for input = true

我正在寻找可以分解向量的 theorem/tactic，这样我就可以用内部 nat 重写，如下所示，这样我就可以使用 cbn.

input: Vector.t nat 1
n: nat
Hin: input = [n]
==================================
complicated_fixpoint_for [n] = true

inversion input 确实引入了 n: nat 但令人惊讶的是没有引入 Hin，这对我之后调用 cbn 没有帮助。

Answer 1

改用dependent inversion input.。当您想要反转的是出现在目标中的术语，而不仅仅是 proof/hypothesis，您想要使用 dependent inversion.

Answer 2

我想你正在寻找 rewrite (eta input).

这里有两个有用的引理：

Import VectorNotations.

Lemma vec0 {T}: forall (v:Vector.t T 0), v = [].
  apply (case0 (fun x => x=[])).
  reflexivity.
Qed.

Lemma vec1 {T} : forall (v:Vector.t T 1), v = [hd v].
  intros.
  rewrite (VectorSpec.eta v).
  apply f_equal.
  apply vec0.
Qed.

Coq Vector 在证明模式下爆炸？

Coq Vector explode in proof mode?

coq