2.2.d

SchottCh
Mausschubser
Mausschubser
Beiträge: 74
Registriert: 4. Okt 2010 16:39

2.2.d

Beitrag von SchottCh » 2. Dez 2011 21:04

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

Matthias Senker
Windoof-User
Windoof-User
Beiträge: 41
Registriert: 14. Okt 2010 22:42

Re: 2.2.d

Beitrag von Matthias Senker » 2. Dez 2011 22:02

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...
Zuletzt geändert von Matthias Senker am 3. Dez 2011 00:55, insgesamt 1-mal geändert.

Christoph Walther
Dozentin/Dozent
Beiträge: 86
Registriert: 1. Nov 2005 18:51

Re: 2.2.d

Beitrag von Christoph Walther » 2. Dez 2011 23:49

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.

SchottCh
Mausschubser
Mausschubser
Beiträge: 74
Registriert: 4. Okt 2010 16:39

Re: 2.2.d

Beitrag von SchottCh » 3. Dez 2011 11:25

Vielen Dank für die Antworten.
Unser Problem lag daran, dass wir extra im Beweis angeben mussten, dass ein bestimmtes Lemma benutzt werden muss. :)

philipp_m
Mausschubser
Mausschubser
Beiträge: 99
Registriert: 4. Dez 2010 18:10

Re: 2.2.d

Beitrag von philipp_m » 4. Dez 2011 22:17

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.

SchottCh
Mausschubser
Mausschubser
Beiträge: 74
Registriert: 4. Okt 2010 16:39

Re: 2.2.d

Beitrag von SchottCh » 4. Dez 2011 22:36

Also wir haben es auch genau so wie beschrieben gemacht. :)

Antworten

Zurück zu „Archiv“