证明n = m和m = o,那么Idris中的n + m = m + o？

Question

我试图通过查看一些软件基础练习(最初用于Coq,但我希望对Idris的翻译不太糟糕)来提高我的Idris技能.我在"练习:1星(plus_id_exercise)"中遇到问题,其中包括:

删除"已录取".并填写证明.

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策略).

顺便说一句,您可能会发现Idris项目中的软件基础非常有用.