主要观点：Lean 4.22 即将发布的新特性之一是用于证明命令式程序属性的新验证基础设施预览。通过一个简单示例展示了如何在 Lean 中使用局部命令式编程来解决问题，并介绍了Std.Do框架用于验证命令式编程，包括 Hoare 三元组、循环不变量等概念，还对比了 Lean 与 Dafny 等系统在验证命令式编程方面的差异，最后提到 Lean 在验证函数式编程方面也很容易，且grind战术在证明过程中发挥了重要作用。

关键信息：

• 示例任务：给定一个整数列表，判断列表中是否存在两个不同位置的整数之和为 0。
• 解决方法：使用集合数据结构，遍历列表时检查是否存在相反数，时间复杂度为期望 O(n)（使用哈希集）或最坏情况 O(n log n)（使用二叉搜索树）。
• Lean 特性：是函数式编程语言，有良好的局部命令式编程支持，通过do记号实现；4.22 预览的Std.Do框架旨在使验证命令式编程容易；是交互式定理证明器，可证明程序正确性。
• Hoare 三元组：断言形式为“如果 P 为真，运行命令 C 后 Q 为真”，可组合用于证明大型程序的属性。
• 证明过程：为pairsSumToZero函数提供 Hoare 三元组的正确性属性，mvcgen生成验证条件，提供循环不变量，使用all_goals simp_all <;> grind完成证明；函数式实现的pairsSumToZero也可通过fun_induction和grind证明。
• 与 Dafny 的对比：Dafny 是自动化系统，依赖 SMT 求解器，有时间长、易超时失败、行为在版本间变化、难以构建大型引理库等问题；Lean 是交互式系统，工具围绕手动证明设计，有良好的编辑器支持、大量可复用概念和引理、强大自动化等优势。

重要细节：

• Std.HashSet和Std.TreeSet分别用于实现期望时间 O(n)和最坏情况 O(n log n)的集合操作。
• 循环不变量的具体内容及在 Lean 中的形式化表示。
• grind战术在证明过程中的作用及相关参考手册。
• 提到关于函数式语言中命令式编程的相关论文。