Proofs about functions that depend on the ordering of their alternatives

Question

Having quite some experience in Haskell, I just recently started to use Idris for theorem proving. This is a minimal example that illustrates a problem I encountered when trying to prove rather simple statements.

Consider we have a total function test:

total test : Integer -> Integer
test 1 = 1
test n = n

Of course we see that the function could be simplified to test n = n, but let's prove it. I am simply going over all the cases:

total lemma_test : (n : Integer) -> test n = n
lemma_test 1 = Refl
lemma_test n = Refl

But, this doesn't type-check:

Type mismatch between
        n = n (Type of Refl) and
        test n = n (Expected type)

Specifically:
        Type mismatch between
                n
        and
                test n

So, the problem seems to be that Idris cannot infer for the second case of lemma_test that n is not equal to 1 and that also the second case of test must be applied.

We can, of course, try to explicitly list ALL the cases, which can be cumbersome, or impossible, as in the case for Integers:

total lemma_test : (n : Integer) -> test n = n
lemma_test 1 = Refl
lemma_test 2 = Refl
lemma_test 3 = Refl
...

Is there a way to prove statements like this for functions that are not defined over a finite set of data constructors but instead depend on the fact that pattern-matching works from top to bottom, like test in this example?

Maybe there is a rather simple solution that I just fail to see, considering that functions like this occur quite often.

Answer 1

As others have said, Integer is primitive, and not an inductively defined Idris type, therefore we can't do exhaustive pattern matching on it. More specifically, the issue is that in Idris (and actually in state-of-the-art Agda too!) we can't really prove things about "default" pattern matches, because they don't carry information about all the previous patterns that failed to match. In our case, test n = 1 doesn't give us evidence that n is not equal to 1.

The usual solution is to use decidable equality (Boolean equality could be good too) instead of fall-through:

import Prelude

%default total

test : Integer -> Integer
test n with (decEq n 1)
  test n | Yes p = 1
  test n | No  p = n

lemma_test : (n : Integer) -> (test n) = n
lemma_test n with (decEq n 1)
 lemma_test _ | (Yes Refl)  = Refl
 lemma_test n | (No contra) = Refl

Here, the No result carries explicit evidence about the failed match.