Tipps für "MATCH is sound"?

[JanK]

Bei dem Beweis des Lemmas "Match is sound" kommen wir bei den letzten beiden Induktionsschritten nicht weiter. Wir haben noch kein anwendbares Lemma für diesen Beweis gefunden.
Hat jemand Tipps dafür?

[fetzer]

Sitzen beim selben Problem und finden leider keinerlei Ansatzpunkte. Würde mich ebenfalls über Tipps oder Anfangspunkte freuen.

[pigbird]

zu dem oberen der letzten Schritte habe ich ein Lemma über :: - Operator, eine Substitution σ angewandt auf eine Liste (nämlich tl(k)) gebraucht. Zu beachten ist die Induktionshypothese. Ich weiss nicht wie es bei euch ist, aber das Hilfslemma soll sich selbst beweisen, wenn Ihr die anderen Lemmas von anderen Aufgaben habt.
zu dem anderen, habe ich das Hilfslemma MATCH(k, l) ≠ ↯ → | k | = | l | mit "Use Lemma" benutzt. Weitere Lemmas über die Länge sind bei mir nötig. Ich hoffe, es kann euch weiter helfen.

[_Peter_]

habt ihr eine grobe Vorgehensweise für die 3.5? Brauch grad nen Denkanstoss.
Habe das Hilfslemma noch nicht beweisen können.

[_Peter_]

Ich hab ja ein Lemma, was wunderbar zum Beweis von MATCH(k, l) ≠ ↯ → | k | = | l | passen müsste, aber leider trotzdem nicht funktioniert.

Edit: das Lemma war zu lang und zu übertrieben. Ein kleines lemma über | zweier Listen und schwupp wars bewiesen

[hangman]

Hallo,

wir haben auch Probleme mit 3.5. Beim 1. der 3 blauen "Äste" komme ich auf diesen Goalterm

Code: Alles auswählen

(result(MATCH(tl(k), tl(l))) ⊫ k) = l

Ich habe versucht die Vollständigkeit darauf anzuwenden aber ohne Erfolg. Die Aussage sieht ja ziemlich trivial aus.

[Nathan Wasser]

Ich finde die Aussage zwar nicht sonderlich trivial (gilt nur unter zusätzlichen Bedingungen), aber evtl wäre Unfold Procedure eine Überlegung wert.

[Nadine]

Tipps zu den zwei untersten blauen Zweigen wären hilfreich.

[_Peter_]

Tipps für den ersten blauen Zweig sind auch gerne gesehen

[C0RNi666]

Ich finde die Aussage zwar nicht sonderlich trivial (gilt nur unter zusätzlichen Bedingungen), aber evtl wäre Unfold Procedure eine Überlegung wert.

Dieser Tip bezieht sich auf den ersten der letzten drei blauen Zweige, allerdings komme ich bei den anderen auch nicht weiter und bin für jeden Hinweis dankbar

[hangman]

Diese Behauptung muss Gelten wenn es ein Matcher für tl(k) und tl(l) gibt. Gibt es andere Bedingungen?

Code: Alles auswählen

(result(MATCH(tl(k), tl(l))) ⊫ k) = l

[mister_tt]

Wie kommst du denn darauf? Dies gilt keinesfalls ohne weitere Bedingungen. Da muss hd(k) ja noch mit hd(l) gematcht werden...

[hangman]

Unfold hat geholfen. Danke!

[petzchri]

Servus! Bin auch immer noch bei der letzten Aufgabe und komm beim vorletzten Zweig einfach nicht weiter als:



Ist jemand schon weiter gekommen? Wo setzt man denn da am bessten an? Lemmas über pair :: σ haben bei mir nicht geklappt

[Nathan Wasser]

Schauen Sie sich die Induktionshypothese an. Schauen Sie sich den Goalterm an. Was für ein (generalisiertes) Lemma bräuchten Sie um Goalterm und Induktionshypothese gleichzusetzen? Was für Bedingungen müssten da gelten? Sind diese zufällig in den globalen Hypothesen zu finden?