Ich versuche zu beweisen, was meiner Meinung nach ein vernünftiger Satz ist:

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

Der Beweis durch Induktion kommt an den Punkt, an dem ich dies beweisen muss:

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

Folgendes passiert, wenn ich versuche, es (der Einfachheit halber das Lemma) mit dem interaktiven Beweis zu beweisen:

----------                 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

Ich hatte das Gefühl, dass mir etwas an der Definition von Minus fehlen muss, also habe ich in der Quelle nachgeschlagen:

||| 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

Die Definition, die ich brauche, ist genau dort!minus left Z = left. Mein Verständnis war, dass Idris nur ersetzen sollteminus m 0 mitm hier, und das ist dann reflexiv wahr. Was habe ich vermisst?