有没有更优雅的方法让Coq识别基于列表的假设是矛盾的？

你遇到的discriminate失效的原因是它只能识别直接的归纳类型构造器冲突，比如[] = a :: l这种两边头构造器不一样的等式，但你的H2是[] = l2 ++ [x0]，右边是app函数的调用结果，不是直接的cons构造器，所以discriminate没法直接判断。

下面是几种可行的解决策略：

方案1：对l2做分类讨论（最直观，无需额外引理） #

对l2执行destruct拆分情况，就能把app的结果展开为直接的构造器形式，后续discriminate就能正常识别矛盾：

destruct l2.
- (* l2 为空时，H2 化简为 [] = [x0] *)
  discriminate.
- (* l2 为非空时，H2 化简为 [] = _ :: _ *)
  discriminate.

如果需要更简洁的写法，可以直接用now destruct l2.一步完成。

方案2：通过列表长度推导矛盾 #

利用列表长度的性质，把等式两边映射为自然数，就能得到自然数的构造器冲突：

(* 把长度函数应用到等式两边 *)
apply f_equal with (f := @length T) in H2.
(* 化简后得到 0 = S (length l2) *)
simpl in H2.
(* 此时discriminate可以直接识别自然数的构造器矛盾 *)
discriminate.

方案3：自动化策略直接解决 #

如果你的环境支持高阶 congruence 推导，直接用congruence策略就可以自动完成上述推导，一步解决矛盾：

congruence.

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