Ich versuche, ein einfaches Lemma in Agda zu beweisen, was ich für wahr halte.
Wenn ein Vektor mehr als zwei Elemente hat, ist die Übernahme von
headnach der Verwendung voninitgleichbedeutend mit der gleichzeitigen Verwendung vonhead.
Ich habe es wie folgt formuliert:
%Vor%Was gibt mir?
%Vor%als Antwort.
Ich verstehe nicht ganz, wie man die (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)) -Komponente liest. Ich nehme an, meine Fragen sind; ist es möglich, wie und was bedeutet dieser Begriff?
Vielen Dank.
Ich verstehe nicht ganz, wie lies die
(init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs))-Komponente. ich Angenommen, meine Fragen sind; ist es möglich, wie und was heißt das? gemein.
Dies sagt Ihnen, dass der Wert init (x ∷ xs) von dem Wert von alles rechts von | abhängt. Wenn Sie in Agda etwas in einer Funktion beweisen, muss Ihr Beweis die Struktur der ursprünglichen Definition haben.
In diesem Fall müssen Sie das Ergebnis von initLast berücksichtigen, weil die Definition von initLast dies vor dem Erzeugen von Ergebnissen tut.
Also hier ist, wie wir das Lemma schreiben.
%Vor% Ich habe mir erlaubt, Ihr Lemma auf Vec A zu verallgemeinern, da das Lemma nicht vom Inhalt des Vektors abhängt.
Ok. Ich habe das durch Betrug und ich hoffe, dass jemand eine bessere Lösung hat. Ich habe alle zusätzlichen Informationen, die du von init bekommst, in initLast weggeworfen und meine eigene naive Version erstellt.
Jetzt ist das Lemma trivial.
Irgendwelche anderen Angebote?
Tags und Links agda theorem-proving