Coq练习中transitivity命令针对列表中间项j失效的原因咨询

你正在完成的LF练习代码：

Example injection_ex3 : ∀ (X : Type) (x y z : X) (l j : list X),
  x :: y :: l = z :: j →
  j = z :: l →
  x = y.

你执行以下证明步骤时遇到transitivity命令失败问题：

Proof.
  intros X x y z l j H I. 
  injection H as J.
  Fail transitivity j. (* shouldn't fail imho *) 

此时的证明环境：

1 subgoal

X : Type
x, y, z : X
l, j : list X
J : x = z
H : y :: l = j
I : j = z :: l

========================= (1 / 1)

x = y

错误提示信息：

The command has indeed failed with message:
In environment
X : Type
x, y, z : X
l, j : list X
J : x = z
H : y :: l = j
I : j = z :: l
The term "j" has type "list X" while it is expected to have type "X".  

问题根源 #

transitivity命令默认作用于当前目标等式，你当前的目标是x = y——这是一个X类型元素间的等式，因此transitivity要求传入的中间项必须是X类型的对象。但你传入的j是list X类型的列表，类型完全不匹配，所以命令报错。

你可能误以为transitivity会自动识别环境中的列表等式，但实际上它只会处理当前目标。若要对环境中的列表等式使用传递性，需要先通过rewrite等操作将目标关联到列表等式，或者明确指定作用的等式。

修正思路与代码 #

利用已有的等式链推导：

1. 通过rewrite H in I将I中的j替换为y :: l，得到y :: l = z :: l
2. 对这个等式使用injection得到y = z
3. 此时目标x = y可以通过中间项z（X类型）使用transitivity完成证明

修正后的证明代码：

Proof.
  intros X x y z l j H I.
  injection H as J.
  rewrite H in I.
  injection I as K.
  transitivity z.
  - exact J.
  - exact K.
Qed.

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