证明如果 n = m 和 m = o，那么 Idris 中的 n + m = m + o？

Question

我正在尝试通过查看一些练习来提高我的 Idris 技能 Software Foundations (originally for Coq, but I am hoping the translation to Idris not too bad). I am having trouble with the "Exercise: 1 star (plus_id_exercise)" 上面写着：

Remove "Admitted." and fill in the proof.

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) 的后继。我能做些什么来解决这个问题吗？我是否正确地处理了这个问题？我有点困惑。

Answer 1

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

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

上面的意思是=（它是eq类型的语法糖）接受两个A类型的参数并产生一个命题，不是布尔值。

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

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

并且当您对相等类型的值进行模式匹配时，Idris 实质上是根据相应的等式重写项（这大致相当于 Coq 的 rewrite 策略）。

顺便说一下，您可能会发现 Software Foundations in Idris 项目很有用。

证明如果 n = m 和 m = o，那么 Idris 中的 n + m = m + o？

Proving if n = m and m = o, then n + m = m + o in Idris?

proof

idris