CODEWITHSUNDEEP
pattern-matchingdependent-typeidristheorem-proving
Tobias Weck
Tobias Weck

Reputation: 289

Proofs about functions that depend on the ordering of their alternatives

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.

Upvotes: 4

Views: 113

Answers (3)

András Kovács
András Kovács

Reputation: 30103

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.

Upvotes: 2

pdxleif
pdxleif

Reputation: 1800

Integer isn't defined in Idris, but rather defers to GMP bigints. It's effectively opaque to Idris, and apparently not something you can reason about cases of at compile time in this way. With something like Nat, which is defined inductively, you can talk about proofs in the form of a base case and a recursive case.

That type error about n not being test n is telling you that Idris can't reduce the expression test n. I'm not sure that's how it's supposed to behave - obviously it's a total function, and it's supposed to reduce total functions afaik. Maybe that's related to the opacity of Integer to Idris?

You can test out the reduction at the repl, by introducing the free variable as a labmda param. E.g. \n => test n just echoes back \n => test n : Integer -> Integer (with nothing changed), however, if you remove the test 1 = 1 case from your definition and try again, it echoes back \n => n : Integer -> Integer - it's reduced test n to n. And then your proof would work as-is.

Upvotes: 1

Cactus
Cactus

Reputation: 27626

I'm not sure how Integer is defined, or how to do induction on it, etc., so this is not a full answer to your question; but maybe the Nat version is also going to be informative for you? (also, maybe you actually meant Nat, since in your second example you only enumerate the positive naturals?)

If you change test to use Nats:

total test : Nat -> Nat
test (S Z) = 1
test n = n

then you can do exhaustive pattern matching in lemma_test:

total lemma_test : (n : Nat) -> test n = n
lemma_test (S Z) = Refl
lemma_test Z = Refl
lemma_test (S (S k)) = Refl

Upvotes: 1

Related Questions