Idris - proving equality of two numbers

4
votes

I would like to write a function that takes two natural arguments and returns a maybe of a proof of their equality.

I'm trying with

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

but I get the following error

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

Which is the correct way to do this?

Moreover, as a bonus question, if I do

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

I get

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

Is it a known issue or should I report it?

2
idristheorem-proving
Bear in mind that tactic-based proofs are obsolete in Idris, while a making decision to report an issue. – Anton Trunov
You might want to consider using decEq. – michaelmesser

2 Answers

5
votes

Let's take a look at the implementation of the Eq interface for Nat:

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

You can solve the problem just by following the structure of the (==) function as follows:

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
4
votes

You can do it by using with instead of case (dependent pattern matching):

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

Note that, as Anton points out, this merely a witness on a boolean test result, a weaker claim than proper equality. It might be useful for advancing a proof about if a==b then ..., but it won't allow you to substitute a for b.