Ich kann mit Idris nicht beweisen, dass (n - 0) = n ist
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?