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.