在 Idris 中证明如果 n = m 且 m = o，则 n + m = m + o？

我正在尝试通过查看一些练习来提高我的伊德里斯技能软件基础 https://softwarefoundations.cis.upenn.edu/lf-current/toc.html（最初是为 Coq 设计的，但我希望对 Idris 的翻译不会太糟糕）。我遇到了问题“练习：1 星 (plus_id_exercise)” https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html#lab31内容如下：

删除“已承认”。并填写证明。

Theorem plus_id_exercise : ∀ n m o : nat,
  n = m → m = o → n + m = m + o.
Proof.
  (* FILL IN HERE *) Admitted.

我在 Idris 中翻译了以下问题：

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

我正在尝试进行个案分析，但遇到了很多问题。第一种情况：

plusIdExercise Z Z Z n_eq_m n_eq_o = Refl

似乎可行，但我想说的是：

plusIdExercise (S n) Z Z n_eq_m n_eq_o = absurd

但这不起作用并给出：

When checking right hand side of plusIdExercise with expected type
        S n + 0 == 0 + 0 = True

Type mismatch between
        t -> a (Type of absurd)
and
        False = True (Expected type)

Specifically:
        Type mismatch between
                \uv => t -> uv
        and
                (=) FalseUnification failure

我想说这种情况永远不会发生，因为 n == m，但 Z (= m) 永远不会是任何数字 (n) 的后继。我能做些什么来解决这个问题吗？我的做法正确吗？我有些困惑。

我认为翻译并不完全正确。 Coq 中陈述的引理在自然数上不使用布尔相等，它使用所谓的命题相等。在 Coq 中，您可以要求系统为您提供有关事物的更多信息：

Coq < About "=".
eq : forall A : Type, A -> A -> Prop

以上的意思是=（它是语法糖eqtype) 接受某种类型的两个参数A并产生一个主张，不是布尔值。

这意味着直接翻译将是以下片段

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

当你对等式类型的值进行模式匹配时，Idris 本质上会根据相应的方程重写项（它大致相当于 Coq 的rewrite战术）。

顺便说一下，你可能会发现伊德里斯的软件基础 https://github.com/idris-hackers/software-foundations项目有用。