Praxis 1.2b)

[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]

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]

Jetzt ist es grün