Idris - 证明两个数相等

Question

我想编写一个函数，它接受两个自然参数并返回它们相等的证明。

我正在尝试

equal : (a: Nat) -> (b: Nat) -> Maybe ((a == b) = True)
equal a b = case (a == b) of
    True => Just Refl
    False => Nothing

但我收到以下错误

When checking argument x to constructor Prelude.Maybe.Just:
        Type mismatch between
                True = True (Type of Refl)
        and
                Prelude.Nat.Nat implementation of Prelude.Interfaces.Eq, method == a
                                                                                   b =
                True (Expected type)

        Specifically:
                Type mismatch between
                        True
                and
                        Prelude.Nat.Nat implementation of Prelude.Interfaces.Eq, method == a
                                                                                           b

执行此操作的正确方法是什么？

此外，作为一个额外的问题，如果我这样做

equal : (a: Nat) -> (b: Nat) -> Maybe ((a == b) = True)
equal a b = case (a == b) of
    True => proof search
    False => Nothing

我明白了

INTERNAL ERROR: Proof done, nothing to run tactic on: Solve
pat {a_504} : Prelude.Nat.Nat. pat {b_505} : Prelude.Nat.Nat. Prelude.Maybe.Nothing (= Prelude.Bool.Bool Prelude.Bool.Bool (Prelude.Interfaces.Prelude.Nat.Nat implementation of Prelude.Interfaces.Eq, method == {a_504} {b_505}) Prelude.Bool.True)
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/idris-lang/Idris-dev/issues

这是一个已知问题还是我应该报告它？

Answer 1

我们来看看Eq的实现Nat的接口(interface):

Eq Nat where
  Z == Z         = True
  (S l) == (S r) = l == r
  _ == _         = False

只需按照 (==) 的结构即可解决问题。功能如下:

total
equal : (a: Nat) -> (b: Nat) -> Maybe ((a == b) = True)
equal Z Z = Just Refl
equal (S l) (S r) = equal l r
equal _ _ = Nothing