Trick für Lemma-Ideen ?

[FeG]

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

[Christoph Walther]

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?

Tricks gibt es nicht. Es gibt methoden, die in vielen (einfachen) fällen funktionieren - s. abschnitt "2.4 Einschub: Durch Generalisierung Lemmata “erfinden”" auf folie 2/36. Solche "lemma-erfindungsprozeduren" kann man dann auch implementieren (und sind ja auch in VeriFun implementiert - s. menue Proof\Generalize).

Aber i.A. kommt man auf die erforderlichen lemmata nur durch eigene überlegung. Dazu muß man sich obendrein im gegenstandsbereich auskennen, sonst hat man keine chance. Die mathematik, die den übungsaufgaben & testaten von FGdI 3 zu grunde liegt, ist so einfach, daß man deren kenntnis durch studenten des 3. semesters erwarten kann. Beispielsweise kenntnisse über die grundrechenarten, teilbarkeit, restklassen, ggt usw. Bei den sortieraufgaben muß man sich nur mit totalen ordnungen und listen auskennen. Trotzdem ist das erfinden von lemmata am anfang nicht einfach - das soll eben hier gelernt werden. Ergebnis sind dann erfahrungen & kenntnisse, die einem helfen ähnliche probleme später besser & schneller zu lösen. Das ist genau so wie bei der programmierung - mit den ersten programmen hat man sich ja auch schwer getan bis dann irgendwann genug erfahrungen & kenntnisse vorhanden waren.

Wichtig ist, daß man sich im gegenstandsbereich gut auskennt oder sich zumindest diese fähigkeit erarbeiten kann. Wir könnten ja z.B. auch die korrektheit des RSA verfahrens mit VeriFun in FGdI 3 beweisen. Nur ist die zu grunde liegende mathematik hier eben nicht mehr so einfach - wenn man sich nicht mit den (nicht-trivialen) grundlagen der zahlentheorie auskennt, so hat man keine chance die erforderlichen lemmata auch zu "erfinden". Wer das nicht glaubt, kann sich ja mal am nachweis der assoziativität des ggt versuchen.

cw.

[aderhold]

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.

Auf dieses Lemma kommt man durch Generalisierung. Solange das Lemma fehlt, bleibt im Goalterm

Code: Alles auswählen

if{?ø(y),
  if{x1 = x2,
    if{x1 = hd(z) :: append(tl(z), x1),
      ¬ length(x1) = succ(length(tl(z)) + length(x1)),
      true},
    true},
  true}

stehen. Jetzt sieht man sich den am weitesten eingerückten Teilterm an (denn da steht oft - jedoch nicht immer - der "Kern" der zu zeigenden Aussage), also:

Code: Alles auswählen

¬ length(x1) = succ(length(tl(z)) + length(x1))

Dieser Teilterm legt folgende Generalisierung nahe: Ersetze "length(x1)" durch eine frische Variable "x : nat" und "length(tl(z))" durch eine frische Variable "y : nat". Dies ergibt

Code: Alles auswählen

¬ x = succ(y + x)

also genau das Lemma aus dem Lösungsvorschlag.