Seite 1 von 1

2.2.d

Verfasst: 2. Dez 2011 21:04
von SchottCh
Hallo, sitzen jetzt schon eine Zeit lang daran und versuchen das Hilfslemma
dbl(x) 6= succ(dbl(y)) zu beweisen. Haben schon viele Lemmata ausprobiert. :( Kann uns vielleicht jemand einen tipp geben ? Danke

Re: 2.2.d

Verfasst: 2. Dez 2011 22:02
von Matthias Senker
Ich kann ja mal versuchen zu beschreiben, wie ich das gelöst habe, ohne die Lösung zu verraten.
(wobei ich anmerken möchte, dass ich nicht sicher bin, ob es nicht eine einfacherer Lösung gibt)

Überlegt doch mal, welche simple Eigenschaft dbl(x) auf jeden fall für alle x hat und formuliert das als Lemma. (Die Funktion, die die Eigenschaft beschreibt ist schon gegeben!)
Dann müsst ihr nur noch in einem Lemma angeben, dass eben für 2 Zahlen n, m, die diese Eigenschaft besitzen, n != succ(m) gilt. Das sollte sich dann automatisch beweisen lassen.

Interessant ist, dass jetzt zwar offensichtlich sein sollte, wie der Beweis für dbl(x) != succ(dbl(y)) zu führen ist, aber man trotzdem das 2. Lemma manuell mit Use Lemma anwenden muss. Keine Ahnung, warum VeriFun das nicht selbst hinkriegt...

Re: 2.2.d

Verfasst: 2. Dez 2011 23:49
von Christoph Walther
SchottCh hat geschrieben:Hallo, sitzen jetzt schon eine Zeit lang daran und versuchen das Hilfslemma
dbl(x) 6= succ(dbl(y)) zu beweisen. Haben schon viele Lemmata ausprobiert. :( Kann uns vielleicht jemand einen tipp geben ? Danke
Lemma "lemma dbl_lemma <= ∀ x, y : ℕ¬ dbl(x) = ⁺(dbl(y))" eingeben und dann den Verify button drücken. Beweisbaum nach der 1. Simplification abschneiden. Der goalterm lautet dann "¬ dbl(x) = ⁺(⁺(⁺(dbl(⁻(y)))))". Jetzt mit Unfold Procedure den aufruf von dbl(x) öffnen. Den dabei entstehenden goalterm mit der induktionshypothese vergleichen. Frage: Was verhindert die anwendung der induktionshypothese? Wenn man die antwort hat, dann ein lemma formulieren, mit dem man die lästigen sachen im goalterm los wird, so daß die induktionshypothese anwendbar wird.

Re: 2.2.d

Verfasst: 3. Dez 2011 11:25
von SchottCh
Vielen Dank für die Antworten.
Unser Problem lag daran, dass wir extra im Beweis angeben mussten, dass ein bestimmtes Lemma benutzt werden muss. :)

Re: 2.2.d

Verfasst: 4. Dez 2011 22:17
von philipp_m
Das selbe Problem hatte ich auch, aber sobald man das weiß, kann man auch komplett strukturell an die Sache gehen, d.h. der Gedankengang der Lemmata wäre ca. dieser:
Bedingung gilt für bestimmte Zahlen (1)
Anwendung einer bestimmten Funktion auf die bestimmten Zahlen aus (1) führt zu einer anderen Bedingung für die entstandenen Zahlen (2)
Zahlen mit Bedingung (1) und Zahlen mit Bedingung (2) können nicht identisch sein (3)

(3) nutzt VeriFun jedoch nicht automatisch, d.h. den kompletten Baum abschneiden und per "Proof Rules -> Use Lemma" (3) anwenden lassen, (1) und (2) nutzt er dann automatisch.

Ich hoffe, das ist okay, das so zu posten, da oben von einem Mod auch schon eine andere Herangehensweise beschrieben wurde. Habe versucht, so viel wie möglich wegzulassen, sodass man noch versteht, welche Art von Lemma nicht automatisch benutzt wird.

Re: 2.2.d

Verfasst: 4. Dez 2011 22:36
von SchottCh
Also wir haben es auch genau so wie beschrieben gemacht. :)