Coq inversion tactic生成矛盾假设的原因及相关证明问题问询

这个问题的核心在于原命题的两个假设本身就是逻辑矛盾的，我们一步步拆解来看：

首先看你给出的原命题与两种证明方式：

Example foo : forall (X : Type) (x y z : X) (l j : list X), 
  x :: y :: l = z :: j -> 
  y :: l = x :: j -> 
  x = y.

只对第二个假设做inversion时，证明很简洁：

Proof. intros X x y z l j eq1 eq2. inversion eq2. reflexivity. Qed.

这是因为inversion eq2直接根据列表cons构造子的 injective 性质，推导出y = x和l = j——第二个假设本身已经能直接推出结论，甚至不需要用到第一个假设。

但如果同时对第一个假设做inversion：

Proof. intros X x y z l j eq1 eq2. inversion eq2. inversion eq1. reflexivity. Qed.

就会生成看似矛盾的假设：

H0 : y = x
H1 : l = j
H2 : x = z
H3 : y :: l = j

结合H1和H3会得到y::j = j，这显然不可能成立，下面来解答你的疑问：

1. 现象原因是什么？ #

本质是原命题的两个假设eq1和eq2不可能同时成立，它们是逻辑矛盾的。inversion tactic的作用是根据归纳类型（这里是list）的构造子性质，把等式成立的所有必要条件全部推导出来，所以会把这种隐藏的矛盾直接暴露在上下文中。

2. 是否示例的两个假设本身矛盾？ #

是的，我们可以手动验证：
把eq2的y::l = x::j代入eq1的左边，得到x::(x::j)，而eq1的右边是z::j。根据列表cons构造子的 injective 性质，要让x::x::j = z::j成立，必须满足：

• 头部相等：x = z
• 尾部相等：x::j = j
  但第二个条件x::j = j不可能成立——cons构造的列表长度比尾部多1，x::j的长度是length j + 1，和j的长度必然不等，因此两个假设无法同时满足。

3. 是否基于爆炸原理？能否从假命题推导完成证明？ #

没错，这正是爆炸原理（ex falso quodlibet，字面意思是“从假可以推出任何”）的场景。在Coq的构造逻辑中，如果上下文存在矛盾（即能推导出False的假设），那么我们可以推导出任何命题，包括目标x = y。

4. 如何操作？ #

你原来的代码已经间接利用了这个原理——inversion eq2直接得出了y = x，所以reflexivity就能完成证明。如果是更一般的矛盾场景（没有直接给出结论），可以用这些方法：

• 用contradiction tactic：它会自动扫描上下文的矛盾假设，直接完成证明。比如上下文有H1: l = j和H3: y::l = j时，执行contradiction即可结束。
• 用discriminate tactic：针对y::j = j这种由不同构造子生成的等式（cons和nil/不同cons），discriminate会直接识别矛盾并完成证明，示例代码如下：

  Proof.
    intros X x y z l j eq1 eq2.
    inversion eq2 as [H0 H1].
    inversion eq1 as [H2 H3].
    rewrite H1 in H3.  (* 将H1代入H3，得到y::j = j *)
    discriminate H3.   (* 识别矛盾，完成证明 *)
  Qed.
  

• 显式调用爆炸原理：先用exfalso把目标转为False，再用矛盾假设证明False，最终推导任意命题。

内容的提问来源于stack exchange，提问作者Waiting for Dev...