Idris - proving equality of two numbers

Question

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?

Lipscomb

Bear in mind that tactic-based proofs are obsolete in Idris, while a making decision to report an issue. – Intrude

You might want to consider using decEq. – Segalman

Answer 1

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

Intrude

thanks for the answer! For Nat is easy since you can pattern match and procede by induction (I should have chosen another type for the example, probably...). What about Int or any other type implementing Eq? – Lipscomb

(==) returns a boolean, so it can (in principle) return False all the time. How are we supposed to know that a == b entails a = b without looking at the implementation of (==)? With proofs, either your function must have a sufficiently strong output type (like decEq) to convey its meaning or you'll need access to the body of the function. – Intrude

Answer 2

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.

Mort

@Lipscomb I think this should be the answer, because it works for equal : Eq ty => (a, b : ty) -> Maybe ((a == b) = True). – Intrude