如何拆分两个列表的相等性？Coq中应用H0和H1完成列表相等性证明的战术查询

嘿，针对你的两个问题我来一步步解答：

一、如何拆分两个列表的相等性？ #

如果你的目标是类似 x :: l1 = y :: l2 这样的列表等式，想要拆分成头部相等和尾部相等两个子目标，可以使用 injection 战术。执行 injection 后，Coq会生成两个子目标：x = y 和 l1 = l2，方便你分别证明这两个等式。

二、当前证明目标的可用战术 #

回到你给出的证明上下文，目标是证明 x :: l1' = y :: l2'，而你已经有了 H0 : x = y 和 H1 : l1' = l2' 这两个关键假设，有几种简单的战术可以直接完成证明：

1. 使用 subst 战术（最便捷） #

subst 战术会自动把上下文中的所有等式代入目标和其他假设里。执行 subst 后，Coq会把目标里的 x 替换成 y，l1' 替换成 l2'，目标就变成了 y :: l2' = y :: l2'，这时候Coq会自动用自反性完成证明，很多情况下甚至不需要你额外输入 reflexivity——subst 之后目标会直接被判定为成立。

2. 使用 rewrite 战术分步替换 #

如果你想更清晰地看到每一步的替换过程，可以分两次用 rewrite：

• 先执行 rewrite H0：把目标里的 x 替换成 y，目标变为 y :: l1' = y :: l2'
• 再执行 rewrite H1：把目标里的 l1' 替换成 l2'，目标变为 y :: l2' = y :: l2'
• 最后执行 reflexivity，完成证明

你也可以反过来先执行 rewrite H1 再执行 rewrite H0，效果是完全一样的。

3. 使用 f_equal 战术 #

f_equal 战术的作用是：如果目标是 f a = f b，它会生成子目标 a = b。在这个场景里，配合 assumption 也能完成证明：

• 执行 f_equal，目标会拆分成两个子目标：x = y 和 l1' = l2'
• 分别对这两个子目标执行 assumption，直接调用上下文里的H0和H1完成证明

不过相比之下，subst 是最直接高效的选择。

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