伊德里斯 - 证明两个数字相等

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:

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