如何在Idris中证明若n=m且m=o则n+m=m+o？

你的证明思路完全正确——这个分支确实不可能发生，问题出在如何正确利用absurd来处理矛盾场景。我们一步步拆解问题并修正：

为什么你的代码会报错？ #

absurd函数需要接收一个Void类型的参数（代表逻辑上不可能存在的情况），但你当前的n_eq_m类型是(S n == Z) = True，也就是False = True——这和Void不是同一个类型，Idris无法直接将其识别为可用于absurd的矛盾值，因此抛出类型不匹配错误。

修正方法：用uninhabited转换矛盾类型 #

Idris的Prelude.Uninhabited模块提供了uninhabited函数，它可以把像False = True这种不可能成立的类型转换为Void。你可以把这个分支改成：

plusIdExercise (S n) Z Z n_eq_m _ = absurd (uninhabited n_eq_m)

这里uninhabited n_eq_m会把False = True这个矛盾命题转换成Void，让absurd能够正常发挥作用，表达“这个情况不可能存在”的逻辑。

更优雅的方案：改用命题相等（推荐） #

你当前使用的是布尔等式(n == m) = True，但在Idris的定理证明场景中，命题相等n = m（表示两个值在定义上完全相等）是更常用、更自然的选择。如果把函数定义改成命题相等的形式：

plusIdExercise : (n : Nat) -> (m : Nat) -> (o : Nat) -> n = m -> m = o -> n + m = m + o

证明会变得异常简洁，直接通过替换规则就能完成：

plusIdExercise n m o n_eq_m m_eq_o =
  rewrite n_eq_m in  -- 将左边的n替换为m，得到m + m
  rewrite m_eq_o in  -- 将右边的o替换为m，得到m + m
  Refl

这种方式不需要复杂的分情况分析，直接利用Idris的rewrite规则完成逻辑替换，证明逻辑清晰且易维护。

补充：其他分支的处理思路 #

如果坚持使用布尔等式的定义，其他不可能的分支（比如n=Z, m=S k）都可以用uninhabited+absurd的组合处理；对于合法的分支（比如n=S n', m=S m'），则可以递归调用plusIdExercise，结合自然数加法的性质完成证明。

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