Trick für Lemma-Ideen ?
Verfasst: 20. Nov 2008 21:04
Hi zusammen,
ich habe bei beiden Präsenzübung das Problem gehabt, dass ich nicht auf die 'kleinen' Lemmata gekommen bin, die man braucht, um die eigentlichen Lemmata oder Hilfslemmata zu beweisen.
Beispiel:
In der Übung 2, Aufgabe 2.3 war ja im Beweis von "append is right-cancelable" etwas Eigenarbeit gefordert. Der Beweisbaum bricht ab und man ist an dem Punkt, den Ausdruck x1 = hd(z) :: append(tl(z), x1) zu widerlegen.
Die Sache ist offensichtlich falsch, soweit klar. Ich hatte dann versucht ein Lemma einzusetzen der Form
not l = element :: (apppend(k), l)
für alle k, l : list[@A] und element : @A.
Das Hilfslemma hat sich dann aber zu weit verstrickt, ich bin letztlich dabei gelandet, x1 = el :: hd(z) :: append(tl(z), x1) (so ähnlich) zu beweisen, es wurde also nur komplizierter.
Dann bin ich sogar auf die Idee gekommen das Lemma "length(k) != length(l) -> k != l" einzusetzen und hab dann versucht, mit einem Hilfslemma zu argumentieren, dass length(l) != length(element :: l) ist, was sich aber nicht einsetzen ließ.
In der Musterlösung hab ich jetzt gesehen, dass es hier nur das Lemma "x != +(x + y)" gebraucht hätte, also nur eine Aussage über eine Gegebenheit in den natürlichen Zahlen.
Lange Rede, kurzer Sinn - meine Frage wäre: Gibt's da eventuell irgendwelche Tricks, mit denen man rausfinden / sehen kann, welches Lemma man jetzt braucht? Weil schwer waren die beiden in dem Fall ja nicht, aber ich komme nicht drauf, dass so etwas wie ""x != +(x + y)" gebraucht werden könnte.
Vielleich gibt es ja sowas, oder ist es doch nur alles Erfahrung?
Viele Grüße
FeG
ich habe bei beiden Präsenzübung das Problem gehabt, dass ich nicht auf die 'kleinen' Lemmata gekommen bin, die man braucht, um die eigentlichen Lemmata oder Hilfslemmata zu beweisen.
Beispiel:
In der Übung 2, Aufgabe 2.3 war ja im Beweis von "append is right-cancelable" etwas Eigenarbeit gefordert. Der Beweisbaum bricht ab und man ist an dem Punkt, den Ausdruck x1 = hd(z) :: append(tl(z), x1) zu widerlegen.
Die Sache ist offensichtlich falsch, soweit klar. Ich hatte dann versucht ein Lemma einzusetzen der Form
not l = element :: (apppend(k), l)
für alle k, l : list[@A] und element : @A.
Das Hilfslemma hat sich dann aber zu weit verstrickt, ich bin letztlich dabei gelandet, x1 = el :: hd(z) :: append(tl(z), x1) (so ähnlich) zu beweisen, es wurde also nur komplizierter.
Dann bin ich sogar auf die Idee gekommen das Lemma "length(k) != length(l) -> k != l" einzusetzen und hab dann versucht, mit einem Hilfslemma zu argumentieren, dass length(l) != length(element :: l) ist, was sich aber nicht einsetzen ließ.
In der Musterlösung hab ich jetzt gesehen, dass es hier nur das Lemma "x != +(x + y)" gebraucht hätte, also nur eine Aussage über eine Gegebenheit in den natürlichen Zahlen.
Lange Rede, kurzer Sinn - meine Frage wäre: Gibt's da eventuell irgendwelche Tricks, mit denen man rausfinden / sehen kann, welches Lemma man jetzt braucht? Weil schwer waren die beiden in dem Fall ja nicht, aber ich komme nicht drauf, dass so etwas wie ""x != +(x + y)" gebraucht werden könnte.
Vielleich gibt es ja sowas, oder ist es doch nur alles Erfahrung?

Viele Grüße
FeG