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

Question

我正在尝试通过查看一些练习来提高我的 Idris 技能 Software Foundations (最初是为 Coq 设计的，但我希望对 Idris 的翻译不会太糟糕)。我在使用 "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 中陈述的引理在自然数上不使用 bool 相等，它使用所谓的命题相等。在 Coq 中，您可以要求系统为您提供有关事物的更多信息:

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

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

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

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

当您对等式类型的值进行模式匹配时，Idris 本质上会根据相应的方程重写术语(它大致相当于 Coq 的rewrite 策略)。

顺便说一句，您可能会找到 Software Foundations in Idris项目很有用。