Anleitung
Deine Aufgabe ist es, die Gleichheit zwischen einer eigenen Funktion zum Umkehren von Listen und dem eingebauten List.reverse zu beweisen.
Aufgrund der Natur dieser Übung wird der Beweis nicht durch traditionelle Laufzeittests überprüft, sondern durch ein Theorem check.
Du kannst den Test als bestanden ansehen, wenn dieses Theorem die Typprüfung besteht.
Wenn du lokal oder in Leans Online-Spielwiese arbeitest, bekommst du über Lean InfoView sofort Rückmeldung darüber, ob ein Theorem gelingt oder scheitert und warum es scheitert.
Es ist ein unschätzbar wertvolles Werkzeug, das alle lokalen Werte, die dein Beweis verwendet, und dein aktuelles Ziel anzeigen kann.
Die sorry-Taktik lässt jeden Beweis korrekt erscheinen.
Aus diesem Grund kann es scheinen, als ob das Theorem check automatisch typprüft, bevor überhaupt ein Beweis geschrieben wurde.
Sobald du sorry aus deinem Beweis entfernst, zeigt Lean InfoView die korrekte Rückmeldung.
Theoreme in Lean beweisen
Das Beweisen von Theoremen ist ein fester Bestandteil von Lean.
Es ermöglicht Programmierenden, Eigenschaften ihrer Programme zu beweisen, Rückschlüsse auf deren Verhalten zu ziehen und Einschränkungen und Spezifikationen auf Typebene zu kodieren.
Dieses Kapitel bietet eine gute Einführung in das Beweisen von Theoremen in Lean.
Für einen tieferen Einblick ist dieses Buch als offizielle Ressource auf der Lean-Website aufgeführt.
Lean bietet viele Taktiken, mit denen sich Beweise oder Teile davon automatisieren lassen.
Vielleicht möchtest du einen Blick in eine Sprachreferenz werfen.
Wir können das Compiler-Attribut csimp für ein Theorem verwenden, das die Gleichheit zweier Definitionen beweist.
Dieses Attribut weist den Compiler an, die zweite Definition anstelle der ersten zu verwenden:
@[csimp]
theorem custom_reverse_eq_spec_reverse : @Extra.custom_reverse = @List.reverse := by
... -- proof here
-- now any occurrence of `Extra.custom_reverse` may now compile to `List.reverse`.
Besonders nützlich ist es, wenn eine Implementierung effizienter, aber weniger klar ist.
Wir können eine einfache Spezifikation schreiben und den kompilierten Code stattdessen die effizientere Implementierung verwenden lassen.
Viele Funktionen von List und Array folgen diesem Muster.
