如何证明伊德里斯的通勤平等？答案

【问题标题】：How to prove equality commutes in Idris?如何证明伊德里斯的通勤平等？
【发布时间】：2020-07-27 21:43:42
【问题描述】：

试图证明以下断言：

equalityCommutesNat : (n : Nat) -> (m : Nat) -> n = m -> m = n

我在库中找到了plusCommutes，但没有发现任何平等。

【问题讨论】：

我对这些东西很陌生，但这不是= 的定义吗？你想用equalityCommutesNat做什么？
这纯粹是一个自我设定的任务，我只是从小的简单属性开始，以建立我对定理证明的理解，因为它目前对我来说非常不直观。我假设有一个证明在概念上是这样的：n = m 实际上等价于 x = x 对于一些 x 即 n = x, m = x。因此 m = x = n。
在库中您可能会发现对此有用的一件事是sym。也许您正在查看特定于 Nat 的证明，但这适用于任何相等：sym : a = b -> b = a
感谢@EdwinBrady - 我尝试使用sym 来证明它，但它在idris2 中对我不起作用：equalityCommutes _ _ p = rewrite sym in p。
你只能用等式重写，而sym是一个从一个等式到另一个等式的函数，所以你需要把它应用到p上。之后，您已经有了答案，无需重写。

标签： idris

【解决方案1】：

= 的唯一居民是Refl : (a = a)，所以如果你进行模式匹配，你会得到n 是m 的证据。

这意味着您可以使用 Refl，因为 Idris 的模式匹配现在知道它们是相同的：

equalityCommutesNat : (n : Nat) -> (m : Nat) -> n = m -> m = n
equalityCommutesNat _ _ Refl = Refl

你可以在 REPL 中玩这个：

> equalityCommutesNat 1 1 Refl
Refl : 1 = 1

【讨论】：