Coq中Program Definition定义的向量append结合性引理无法apply的问题

首先咱们来拆解你遇到的apply失败的核心原因：

• 你用Program Definition定义的t_app_assoc，本质上生成的是一个返回Prop的命题，但你的目标是具体类型内的等式。更关键的是，append (append a b) c的类型是t v ((p+q)+r)，而append a (append b c)的类型是t v (p+(q+r))——Coq默认会把这两个长度类型视为不同的，除非你利用自然数加法的结合性来建立它们的等价关系。Program虽然帮你跳过了初始类型检查，但生成的引理没有自动处理类型转换，导致apply时无法统一两边的类型。

下面给你两种可行的解决方案：

方案一：修正现有Program Definition的应用方式 #

你需要先借助自然数加法结合性引理plus_assoc统一两边的类型，再应用你的引理。针对你的示例目标，具体代码如下：

Require Import Coq.Arith.Plus.
Goal (append (append (nil nat) (nil _)) (nil _) = append (nil _) (append (nil _) (nil _))).
  (* 引入加法结合性的证明 *)
  pose proof (plus_assoc 0 0 0) as H.
  (* 将左边的项转换到右边的类型 *)
  rewrite <- (eq_rect _ (fun n => t nat n) _ H (append (append (nil nat) (nil _)) (nil _))).
  (* 现在两边类型一致，可直接应用引理 *)
  apply t_app_assoc.
Qed.

方案二：更优的引理定义方式（无需Program） #

其实完全可以不用Program Definition，直接用Lemma配合类型转换来定义结合性，这样生成的引理能直接被apply调用。核心是利用plus_assoc建立长度类型的等价，再用VectorDef提供的cast函数转换向量的类型：

Require Import Coq.Vectors.VectorDef Coq.Arith.Plus.

Lemma t_app_assoc {v p q r} (a : t v p) (b : t v q) (c : t v r) :
  cast (plus_assoc p q r) (append (append a b) c) = append a (append b c).
Proof.
  induction a as [|p' x a' IH]; simpl.
  - reflexivity.
  - f_equal; apply IH.
Qed.

cast函数的作用是：当两个长度类型相等时，把一个向量从原长度类型转换到目标长度类型。我们用plus_assoc p q r作为类型相等的证明，把append (append a b) c（类型t v ((p+q)+r)）转换为t v (p+(q+r))，让两边类型完全一致，等式就能直接证明。

用这个引理处理你的示例目标，直接apply即可：

Goal (append (append (nil nat) (nil _)) (nil _) = append (nil _) (append (nil _) (nil _))).
apply t_app_assoc.
Qed.

额外补充：调整Program Definition的写法 #

如果你坚持想用Program Definition，可以修改定义让它自动包含类型转换逻辑，这样生成的引理也能直接应用：

Require Import Coq.Vectors.VectorDef Omega Coq.Arith.Plus.
Program Definition t_app_assoc {v p q r} (a : t v p) (b : t v q) (c : t v r) :
  cast (plus_assoc p q r) (append (append a b) c) = append a (append b c) := _.
Next Obligation.
induction a; simpl; auto.
Qed.

内容的提问来源于stack exchange，提问作者user1544337