Korrektheit von Memoisierung in Lean beweisen: Eine Fallstudie

Dieser Blogbeitrag zeigt, wie man ein dynamisches Programmierproblem mithilfe von Memoisierung im Lean-Theorembeweiser löst und seine Korrektheit formal verifiziert. Der Autor behandelt das Problem der Bytelandianischen Goldmünzen und präsentiert zunächst eine memorierte Lösung unter Verwendung eines HashMap. Die Schwierigkeit, seine Korrektheit direkt zu beweisen, wird hervorgehoben, da das Schließen über Datenstrukturinvarianten herausfordernd ist. Die Lösung verwendet Subtypen und abhängige Paare, um ein `PropMap` zu erstellen, eine Memoisierungstabelle, die nicht nur berechnete Werte, sondern auch Beweise für ihre Korrektheit speichert. Die Korrektheit des Algorithmus wird dann inkrementell innerhalb der rekursiven Implementierung selbst bewiesen, was zu einem trivialen Beweis auf oberster Ebene führt. Dieser Ansatz verbindet elegant Code und Beweis und zeigt eine leistungsstarke Technik zur formalen Verifizierung von Algorithmen der dynamischen Programmierung.