byte2nat is injective wfbyte

radix89
Mausschubser
Mausschubser
Beiträge: 66
Registriert: 13. Apr 2011 13:45

byte2nat is injective wfbyte

Beitrag von radix89 »

Ich komme da einfach nicht weiter, hat jemand nen tipp?
danke

[-=thomas=-]
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 137
Registriert: 27. Apr 2009 10:47
Wohnort: Darmstadt

Re: byte2nat is injective wfbyte

Beitrag von [-=thomas=-] »

Hi,

vielleicht etwas konkreter?

Allgemeine Tipps:
- verschachtelte Induktionen bringen meist nichts
- nach der letzten "Simplification" abschneiden
- konkrete Werte in den Goalterm einsetzen und überlegen, was passiert
- bei vielen "if ??? then true else ..."-Kaskaden mit "Insert Hyptheses" vereinfachen

Gruß
Thomas
Tutor:
WS 11/12: FGdI 3, FoC
SS 11: CMS

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: byte2nat is injective wfbyte

Beitrag von Nathan Wasser »

Ich habe sogar vier Tipps:

1. In einer Gruppe aus 3 bis 4 Studenten die Aufgaben bearbeiten.

2. Im Forum schauen ob schon zu diesem Thema Fragen und Antworten stehen.

3. Eine etwas hilfreichere Beschreibung des Problems angeben. (Aber bitte keine halbfertigen Lösungen hochladen.)

4. Die Poolbetreuung wahrnehmen. (Hier kann der Tutor sogar die halbfertige Lösung direkt betrachten und somit gezielter weiterhelfen.)

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

Re: byte2nat is injective wfbyte

Beitrag von Christoph Walther »

[-=thomas=-] hat geschrieben:Allgemeine Tipps:
- bei vielen "if ??? then true else ..."-Kaskaden mit "Insert Hyptheses" vereinfachen
Der tip is gut, damit werden beweisziele übersichtlicher. Aber besser erst mal mit Case Analysis arbeiten als mit Insert Hypotheses. Die in beiden fällen entstehenden sequenzen sind äquivalent, aber bei Insert Hypotheses kann es passieren, daß prozeduraufrufe ausgeführt werden und das system dadurch die induktionshypothesen nicht mehr anwenden kann. Manchmal ist Insert Hypotheses aber doch erfolgreicher, muß man im konkreten fall ausprobieren. Und dann einen term wählen, bei dem man etwa gleich große fälle erhält. Bei "if ??? then true else ..." bringt eine fallunterscheidung nach ??? z.B. nichts - in ersten fall erhält man dann true und im zweiten fall den else-term. Damit ist nichts gewonnen.

klte
Windoof-User
Windoof-User
Beiträge: 31
Registriert: 7. Sep 2011 15:22

Re: byte2nat is injective wfbyte

Beitrag von klte »

Sorry, aber was heisst "Case Analysis"? Soll ich dann auf einem Blatt alle IF's aufschreiben und mit Werten ersetzen :?:

einalex
Nichts ist wie es scheint
Beiträge: 23
Registriert: 23. Aug 2010 13:40

Re: byte2nat is injective wfbyte

Beitrag von einalex »

Bei "byte2nat is injective" wird in der ersten Induktion der Beweisbaum in 3 Teile geteilt,
den ersten und letzten hab ich ohne Probleme lösen können

Beim mittleren Teil steh ich allerdings auf dem Schlauch.
Ich kann nach dem ersten "Use Lemma*: IH-1" ne Hypothese einfügen, die zu einer erhbelichen - ich sag mal - Komprimierung des Beweisterms führt,
allerdings steh ich jetzt, ob ich da vereinfache oder nicht, vor den Dank dem "dbl(x) != succ(dbl(y))" erschienen Termen und alle meine Ideen, das entweder direkt zu zeigen oder aber die Terme so umzuformen, dass sie einfacher werden, schlagen fehl.

Kann hier jemand einen Tipp dahingehend geben, in welche Richtung man denken sollte?

einalex
Nichts ist wie es scheint
Beiträge: 23
Registriert: 23. Aug 2010 13:40

Re: byte2nat is injective wfbyte

Beitrag von einalex »

bevor sich einer die Mühe macht zu antworten:
alle Probleme lösten sich, nachdem klar wurde, dass eine bestimmte Funktion auch ein Lemma braucht, das sie als injektiv ausweist.
Aber dafür 1.5 Tage dran zu sitzen ist nicht schön. Das hätte verdammt nochmal auch eine Teilaufgabe sein können.

Aaron_H
Erstie
Erstie
Beiträge: 14
Registriert: 4. Okt 2010 16:30

Re: byte2nat is injective wfbyte

Beitrag von Aaron_H »

Wow, vielen Dank. Hab da auch schon ewig drangesessen und bin trotzdem nur (mit Hilfe von drei verschiedenen Lemmata) auf eine Teillösung gekommen...

kruse
Mausschubser
Mausschubser
Beiträge: 49
Registriert: 15. Okt 2009 15:10
Kontaktdaten:

Re: byte2nat is injective wfbyte

Beitrag von kruse »

Danke an einalex!!!

Antworten

Zurück zu „Archiv“