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?
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.
Just playing around with the interactive editing, did a case split and proof search, yields:
lemma1 : (n : Nat) -> (n - 0) = n
lemma1 Z = refl
lemma1 (S k) = refl
This is obvious from the definition of minus, which is why it's simply refl. Maybe it was balking when the input var was simply n, because it could have different behaviour if it was Z or something else? Or the recursion?
Just in case, a lot of arithmetic lemmas are already defined in the Idris Prelude, like yours:
total minusZeroRight : (left : Nat) -> left - 0 = left
minusZeroRight Z = refl
minusZeroRight (S left) = refl
For completeness' sake (the tactic language has been deprecated in favor of elaborator reflection), I will add that the way to prove your lemma in the tactic language is to invoke induction n. You can then use trivial to show each case (after an intros in the inductive case).
---------- Goal: ----------
{hole0} : (n : Nat) -> minus n 0 = n
-lemma1> intros
---------- Other goals: ----------
{hole0}
---------- Assumptions: ----------
n : Nat
---------- Goal: ----------
{hole1} : minus n 0 = n
-lemma1> induction n
---------- Other goals: ----------
elim_S0,{hole1},{hole0}
---------- Assumptions: ----------
n : Nat
---------- Goal: ----------
elim_Z0 : minus 0 0 = 0
-lemma1> trivial
---------- Other goals: ----------
{hole1},{hole0}
---------- Assumptions: ----------
n : Nat
---------- Goal: ----------
elim_S0 : (n__0 : Nat) ->
(minus n__0 0 = n__0) -> minus (S n__0) 0 = S n__0
-lemma1> intros
---------- Other goals: ----------
{hole8},elim_S0,{hole1},{hole0}
---------- Assumptions: ----------
n : Nat
n__0 : Nat
ihn__0 : minus n__0 0 = n__0
---------- Goal: ----------
{hole9} : minus (S n__0) 0 = S n__0
-lemma1> trivial
lemma1: No more goals.
-lemma1> qed
Proof completed!
lemma1 = proof
intros
induction n
trivial
intros
trivial
