Praxis 1.2b)

ohoffman
Erstie
Erstie
Beiträge: 22
Registriert: 21. Apr 2009 01:06

Praxis 1.2b)

Beitrag von ohoffman »

Hi zusammen!

Kann mir vielleicht jemand einen Denkanstoß geben für die Aufgabe?! Ich stehe leider ein wenig auf dem Schlauch...
Man soll ja zeigen, dass die Häufigkeit von Elementen in einer Liste sich nicht ändert, wenn man die Liste umdreht, richtig?

Im Evaluation Viewer bekomme ich schließlich dieses Ziel

Code: Alles auswählen

if{?::(k),
  if{hd(k) = x,
    hd(k) # snoc(reverse(tl(k)), hd(k)) = ⁺(hd(k) # tl(k)),
    x # snoc(reverse(tl(k)), hd(k)) = x # tl(k)},
  true}
Die Aussage müssen wir zeigen, oder? Allerdings leide ich gerade an einer Lemma-Schreib-Blockade :(

Hat jemand einen Tipp?

dschneid
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 271
Registriert: 14. Dez 2009 00:56

Re: Praxis 1.2b)

Beitrag von dschneid »

Erst einmal ist ein guter Tipp in diesem Fall, den Beweisbaum weiter oben abzuschneiden (auf jeden Fall vor "Move Hypothesis", was hier schon angewendet wurde). Man kann zwar auch bei deinem Goal schon sehen, worauf es ankommt, aber es geht ein bisschen in Überflüssigem unter.

Ansonsten überleg dir Folgendes: Du hast eine Liste, und ein Element, dessen Häufigkeit in dieser Liste du zählst. Jetzt fügst du mit snoc ein neues Element in die Liste ein. Wann und wie verändert sich dabei die Häufigkeit des gezählten Elementes? Dann schau dir mal an, was das Goal aussagt, und versuche, es sinnvoll zu generalisieren.

ohoffman
Erstie
Erstie
Beiträge: 22
Registriert: 21. Apr 2009 01:06

Re: Praxis 1.2b)

Beitrag von ohoffman »

Jetzt ist es grün :D

Antworten

Zurück zu „Archiv“