I can't prove (n - 0) = n with Idris

Question

I am trying to prove, what to my mind is a reasonable theorem:

theorem1 : (n : Nat) -> (m : Nat) -> (n + (m - n)) = m

Proof by induction gets to the point where me need to prove this:

lemma1 : (n : Nat) -> (n - 0) = n

This is what happens when I try to prove it (the lemma, for simplicity sake) using the interactive prover:

----------                 Goal:                  ----------
{hole0} : (n : Nat) -> minus n 0 = n

> intros
----------              Other goals:              ----------
{hole0}
----------              Assumptions:              ----------
 n : Nat
----------                 Goal:                  ----------
{hole1} : minus n 0 = n

> trivial
Can't unify
        n = n
with
        minus n 0 = n

Specifically:
        Can't unify
                n
        with
                minus n 0

I felt like I must be missing something about the definition of minus, so I looked it up in the source:

||| Subtract natural numbers. If the second number is larger than the first, return 0.
total minus : Nat -> Nat -> Nat
minus Z        right     = Z
minus left     Z         = left
minus (S left) (S right) = minus left right

The definition I need is right there! minus left Z = left. My understanding was that Idris should just replace minus m 0 with m here, and this is then reflexively true. What have I missed?

Idris is a dependently typed programming language, which makes proofs and programs synonymous due to the Curry-Howard isomorphism. I need to prove this theorem in code in order for my function to be well typed (I left the function out because explaining it would take up unnecessary space). Idris comes with an interactive prover for this reason. So the question is a question about how to use the programming language Idris, not about the maths itself. — Vic Smith
Sorry if this is obvious, not being familiar with the language, but looking through some of the examples for this language - this is far from clear. Are 0 and Z always treated as synonymous or is there something required there to make it work? — Damien_The_Unbeliever
Numeric literals are polymorphically overloaded like in Haskell. Nat is a member of the Num class, which one of the functions is fromInteger. And fromInteger 0 = Z. (There is also some special casing for Nat that goes on in the language itself and in the terminal I think.) In short I don't think that is the problem, although I am not certain enough to be entirely sure. — Vic Smith
An aside: I don't think this is provable as stated. Sure, it makes sense mathematically, but minus isn't really well-defined on Naturals in a total manner. A failing case: if m is zero, and n is non-zero - zero minus anything is defined as zero. So that then leaves you trying to prove (S k) + 0 = 0. Maybe we need a better definition of a "minus" operation on Nats, else stop trying to use them for mathy proofs. — pdxleif

David Christiansen David Christiansen · Accepted Answer · 2014-05-08T07:49:52

Unfortunately, the theorem that you want to prove here is not in fact true, because Idris naturals truncate subtraction at 0. A counterexample to your theorem1 is n=3, m=0. Let's step through the evaluation:

First, we substitute:

3 + (0 - 3) = 0

Next, we desugar the syntax to the underlying Num instance, and put in the actual functions being called:

plus (S (S (S Z))) (minus Z (S (S (S Z))))) = Z

Idris is a strict, call-by-value language, so we evaluate the arguments to the functions first. Thus, we reduce the expression minus Z (S (S (S Z)))). Looking at the definition of minus, the first pattern applies, because the first argument is Z. So we have:

plus (S (S (S Z))) Z = Z

plus is recursive on its first argument, so the next step of evaluation yields:

S (plus (S (S Z)) Z) = Z

We continue this way until plus gets a Z as its first argument, at which point it returns its second argument Z, yielding the type:

S (S (S Z)) = Z

which we cannot construct an inhabitant for.

Sorry if the above seemed a bit pedantic and low-level, but its very important to take specific reduction steps into account when working with dependent types. That's the computation that you get "for free" inside of types, so it's good to arrange for it to produce convenient results.

pdxleif's solution above works well for your lemma, though. The case split on the first argument was necessary to get the pattern match in minus to work. Remember that it proceeds from top to bottom in the pattern matches, and the first pattern has a concrete constructor on the first argument, which means that reduction cannot proceed until it knows whether that constructor matched.

I can't prove (n - 0) = n with Idris

4 Answers