如何基于Idris函数输出推导结论？以equalNumber函数为例

首先先明确你的函数定义（方便后续讨论）：

equalNumber: (x,y : Nat) -> Nat
equalNumber x y = case decEq x y of
    Yes Refl => 42
    No contra => 0

你要证明的引理lemma : (x : Nat) -> equalNumber x x = 42完全可以实现，而且有两种常见的证明方式，我来逐一说明：

方法一：利用标准库定理快速证明 #

Idris的标准库已经为我们提供了decEq的核心性质：任何值和自身的可判定相等必然返回Yes Refl，对应的定理是decEqSelfRefl : (x : a) -> decEq x x = Yes Refl。

我们可以借助这个定理，通过重写（rewrite）简化函数调用的结果：

lemma : (x : Nat) -> equalNumber x x = 42
lemma x = rewrite decEqSelfRefl x in Refl

证明逻辑： #

1. 展开equalNumber x x后，本质是case decEq x x of ...的结构
2. 用decEqSelfRefl x把decEq x x替换成Yes Refl，此时函数调用就变成了case Yes Refl of Yes Refl => 42
3. 这个表达式化简后就是42，和等式右边完全一致，因此用Refl（自反性）即可完成证明。

方法二：手动分析分支，处理矛盾情况 #

如果你想深入理解底层逻辑，也可以手动对decEq x x的结果做分支分析：

lemma : (x : Nat) -> equalNumber x x = 42
lemma x = case decEq x x of
    Yes Refl => Refl
    No contra => absurd contra

证明逻辑： #

1. decEq x x只有两种可能的返回值：Yes Refl或No contra
2. 对于Yes Refl分支：此时equalNumber x x直接返回42，和右边相等，所以用Refl证明
3. 对于No contra分支：这里的contra是一个x ≠ x的证明，但这显然是矛盾的（没有任何值不等于自身）。Idris提供的absurd函数可以消除这种不可能存在的分支——它接受矛盾命题作为输入，能返回任意类型的结果，完美适配这个场景。

为什么这能行？ #

Idris作为依赖类型语言，允许我们直接对函数的定义结构、输入的性质进行推理。你的equalNumber函数是完全透明的（没有隐藏副作用或黑箱逻辑），所以我们可以根据它的case分支规则，结合Nat类型的相等性性质，推导出输入为x x时的输出必然是42。

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