“解构时对术语…的定义不明确”

Question

尝试破坏依赖类型的术语时，我经常在Coq中遇到错误。我知道关于堆栈溢出有两个与此问题相关的问题，但是对于我自己的证明而言，这两个问题都不够笼统。

这里是发生错误的简单示例。

我们定义了一个类型族t：

Inductive t: nat -> Set :=
| t_S: forall (n: nat), t (S n).
我们现在尝试证明该类型家族的每个成员t (S n)都有一个术语，即t_S n。

Goal forall (n: nat) (p: t (S n)), p = t_S n.
我们从开始：

intros n p.
下一步是销毁p：

destruct p.
…但是会遇到以下错误：

Abstracting over the terms "n0" and "p" leads to a term fun (n1 : nat) (p0 : t n1) => p0 = t_S n
which is ill-typed.
Reason is: Illegal application: 
The term "@eq" of type "forall A : Type, A -> A -> Prop"
cannot be applied to the terms
 "t n1" : "Set"
 "p0" : "t n1"
 "t_S n" : "t (S n)"
The 3rd term has type "t (S n)" which should be coercible to "t n1".
[在我看来，它正在尝试将p转换为t_S n1，但是以某种方式未能调和n1必须等于n的事实，从而导致=的相对端不匹配类型。

为什么会发生这种情况以及如何解决这个问题？

尝试破坏依赖类型的术语时，我经常在Coq中遇到错误。我知道有两个与此问题相关的堆栈溢出问题，但都没有...

Answer 1

这个事实的简单证明是>

Goal forall (n: nat) (p: t (S n)), p = t_S n.
Proof.
  intros n p.
  refine (
    match p with
    | t_S n => _
    end
  ).
  reflexivity.
Qed.