Verified Dynamic Programming with Σ-types in Lean

Summary

1. IntroductionIf you’ve taken an algorithms class, you have likely seen dynamic programming, specifically a technique called memoization. Memoization works to optimize recursive algorithms by caching the solutions to subproblems in a table, and when a subproblem is encountered, it queries the table instead of recomputing the solution. This gives us an exponential performance boost.This blog post will show how to solve a dynamic programming problem using memoization in Lean, and verify its correctness against a specification. The technique used in the proof of correctness here is an interesting application of Lean’s dependent types, and is generalized to work for any memoization algorithm. The idea came from a conversation with GasStationManager over at the Lean Zulip chat, who I credit with coming up with the general technique.This should be pretty beginner friendly. Basic data structures+algorithms at the undergrad level. Lean experience is not necessary but is helpful for following code samples.Table of ContentsIntroductionProblemFirst SolutionType Theory Interlude: Subtypes and Dependent PairsImproved SolutionConclusionExercisesReferences 2. ProblemThe problem we will be working on here is called Bytelandian Gold Coins. The problem description is as follows:In Byteland they have a very strange monetary system. Each Bytelandian gold coin has an integer number written on it. A coin n can be exchanged in a bank into three coins: n/2, n/3 and n/4. But these numbers are all rounded down (the banks have to make a profit).You can also sell Bytelandian coins for American dollars. The exchange rate is 1:1. But you can not buy Bytelandian coins. You have one gold coin. What is the maximum amount of American dollars you can get for it?The solution is classic DP. Observe that for any amount up to 8, we can’t get more money by dividing into $n/2, n/3, n/4$. For any value, the minimum amount we can get out of it is $n$. We will compare this value with the value we get after d...