为何无法用simpl化简`j = j -> x = y`？Coq证明求助

当前你的证明目标是j = j -> x = y，处理起来很直接：

• 先引入这个蕴含式的前提（j=j本身是恒真命题，无需额外证明），再聚焦推导x=y即可。

补充当前状态的证明代码 #

在现有证明基础上添加以下步骤就能完成证明：

intros _. (* 引入j=j的前提，直接忽略名字 *)
rewrite Hnm1. (* 用Hnm1把x替换成z，目标变为z=y *)
rewrite <- H2 in H. (* 将H里的j替换成z::l，得到y::l = z::l *)
injection H as Hyz. (* 对list等式做injection，得到y=z *)
rewrite Hyz. (* 把z替换成y，目标变为y=y *)
reflexivity.

更简洁的初始证明思路 #

其实你之前的步骤里没必要额外assert H3，从初始的两个前提直接推导更高效：

Example injection_ex3 : forall (X : Type) (x y z : X) (l j : list X),
  x :: y :: l = z :: j ->
  j = z :: l ->
  x = y.
Proof.
  intros X x y z l j H1 H2.
  injection H1 as Hxz Hj. (* 一次injection得到x=z和y::l = j *)
  rewrite H2 in Hj. (* 把Hj里的j替换成z::l，得到y::l = z::l *)
  injection Hj as Hyz. (* 得到y=z *)
  rewrite Hxz, Hyz. (* 利用x=z和z=y的传递性，目标变为y=y *)
  reflexivity.
Qed.

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