Lean 4.22版本将引入新的验证基础设施，用于证明命令式程序的属性。本文通过一个简单的编程任务展示了这一功能：判断整数列表中是否存在两个不同位置的数之和为零。作者提出了一种高效的解决方案，利用集合数据结构在O(n)时间内完成该任务，并与类似工具进行了比较。

主要内容总结

标题: 我的第一个经过验证的命令式程序

发布时间: 2025年7月6日

作者: Markus Himmel

文章概述: 本文介绍了Lean 4.22版本中即将推出的新功能——用于验证命令式程序属性的基础设施。作者通过一个简单的编程任务展示了这一功能，并与类似工具进行了比较。

主要内容:

1. 示例任务:

   • 任务：给定一个整数列表，判断是否存在两个不同位置的整数之和为零。
   • 示例：列表[1, 0, 2, -1]应返回true，因为1 + (-1) = 0；列表[1, 0, -2]应返回false。
   • 解决方案：使用集合数据结构，遍历列表并检查是否已存在当前元素的相反数。

2. 本地命令式编程:

   • Lean虽然是函数式编程语言，但也支持命令式编程。通过do语法，可以在单个函数内实现命令式编程。
   • 示例代码展示了如何使用集合数据结构实现上述任务。

3. 验证命令式程序的属性:

   • Lean不仅是编程语言，还是交互式定理证明器。传统上，验证命令式程序的属性较为困难，但Lean 4.22引入了Std.Do框架，简化了这一过程。
   • Std.Do基于Hoare三元组，允许用户通过断言来验证程序的正确性。
   • 示例中，作者展示了如何通过mvcgen生成验证条件，并提供循环不变量来证明程序的正确性。

4. 自动化证明工具:

   • Lean 4.22引入了grind策略，用于自动化处理许多“显而易见”的证明。
   • 通过grind，作者快速完成了五个证明任务，验证了程序的正确性。

5. Lean与其他验证工具的比较:

   • 与Dafny和Verus等自动化验证工具相比，Lean更注重交互式证明，用户可以在自动化工具失败时手动完成证明。
   • Lean的核心理念是构建可重用的理论和证明库，这使得它在复杂程序验证任务中更具优势。

6. 函数式编程的验证:

   • 作为补充，作者还展示了如何使用grind验证函数式实现的正确性。

结论: 作者对Lean 4.22的新功能表示兴奋，认为Lean在程序验证领域具有很大潜力，尤其是在需要构建可重用理论和证明库的复杂任务中。

图片: 无

1. 关于算法证明的局限性

   • 评论1指出，该证明仅适用于任意精度整数，而在固定精度整数的情况下，算法可能会错误地报告“false”。
   • 关键引用：
     • "Naturally, this proof only works for arbitrary-precision integers"（“自然地，这个证明仅适用于任意精度整数”）
     • "the algorithm will wrongfully report 'false' for arrays like e.g. [INTMIN, -1]"（“对于像[INTMIN, -1]这样的数组，算法会错误地报告‘false’”）

2. 关于证明的复杂性与实用性

   • 评论2认为，尽管Lean的新功能令人印象深刻，但证明的长度和复杂性远超程序本身，质疑其在现实世界程序中的扩展性。
   • 关键引用：
     • "the proof is significantly longer and more complex than the program itself"（“证明的长度和复杂性远超程序本身”）
     • "I wonder how well this will scale to real-world programs"（“我怀疑这在现实世界程序中的扩展性如何”）

3. 关于递归与循环的优劣

   • 评论3主张使用尾递归而非循环，认为尾递归更易于验证正确性，且能避免无限循环和早期退出问题。同时，作者批评某些语言不支持尾调用优化，导致循环更为流行。
   • 关键引用：
     • "tail recursion is better than looping: with tail recursion, you are forced to explicitly reenter the loop"（“尾递归优于循环：尾递归迫使你显式地重新进入循环”）
     • "Lean would be better if it didn’t give in and support imperative code"（“如果Lean不妥协并支持命令式代码，它会更好”）

4. 对Lean未来的期待

   • 评论4表达了对Lean未来的兴奋之情，认为其发展前景广阔。
   • 关键引用：
     • "That’s really neat! I’m very excited for the future of Lean"（“这真的很棒！我对Lean的未来非常兴奋”）

总结：评论主要围绕算法证明的局限性、证明的复杂性与实用性、递归与循环的优劣以及对Lean未来的期待展开。不同观点平衡地反映了对Lean及其新功能的认可与质疑。