Lean 中的备忘录化动态规划证明

本文介绍了如何在 Lean 编程语言中使用备忘录化技术解决动态规划问题，并通过依赖类型对其正确性进行验证。作者首先提出了一个经典的动态规划问题——Bytelandian 金币问题，然后给出了一个使用 HashMap 的备忘录化解法，并解释了直接证明其正确性的困难。随后，文章引入了子类型和依赖对的概念，并利用它们构建了一个新的 Memoization 表 PropMap，该表不仅存储计算结果，还存储了其正确性的证明。最终，作者通过在算法中嵌入证明的方式，实现了算法的正确性验证，并给出了一个简单的最终证明。