Lean循环验证

Lean循环验证是程序验证中的关键技术，用于证明循环的正确性（如终止性、不变式保持等）。在Lean定理证明器中，通过依赖类型和归纳构造，开发者可以形式化验证循环的行为是否符合预期。本文将系统介绍其原理、实现方法及实际应用案例。

核心概念

循环验证主要解决两个关键问题：

1. 循环不变式（Loop Invariant）：在每次迭代中保持为真的性质
2. 终止性（Termination）：确保循环不会无限执行

在Lean中，循环通常通过递归函数或`while`语法糖实现，验证则依赖以下数学构造：

• 归纳类型（Inductive Types）
• 测度函数（Measure Function）
• 命题等式（Propositional Equality）

基础验证模式

递归函数验证

Lean中循环常用递归实现，以下阶乘函数为例：

def factorial : Nat → Nat
| 0 => 1
| (n + 1) => (n + 1) * factorial n

终止性证明依赖Nat参数的递减性。可通过添加注解显式声明：

@[termination_by]  -- 显式指定测度函数
def factorial (n : Nat) : Nat :=
  if n = 0 then 1
  else n * factorial (n - 1)
termination_by _ => n  -- n作为测度

While循环验证

使用`Lean.WHILE`宏时（需导入`Lean.Meta.WHILE`），验证框架会自动生成证明义务：

import Lean.Meta.WHILE

def sumToN (n : Nat) : Nat :=
  let mut i := 0
  let mut sum := 0
  while i < n do
    sum := sum + i
    i := i + 1
  sum

系统会要求证明： 1. 循环条件`i < n`最终会变为假（终止性） 2. 变量`sum`始终满足`sum = ∑_{k=0}^{i-1} k`（不变式）

高级验证技术

不变式标注

使用`invariant`关键字显式声明循环不变式：

def power (x : Nat) (n : Nat) : Nat :=
  let mut y := 1
  let mut i := 0
  while i < n do
    invariant y = x^i ∧ i ≤ n  -- 不变式声明
    y := y * x
    i := i + 1
  y

变体函数

对于复杂终止条件，需定义变体函数（Variant Function）：

graph TD A[循环开始] --> B{条件满足?} B -->|是| C[执行循环体] C --> D[变体函数值递减] D --> B B -->|否| E[退出循环]

对应Lean实现：

def euclid (a b : Nat) : Nat :=
  let mut x := a
  let mut y := b
  while x ≠ y do
    decreasing_if x > y then x - y else y - x  -- 变体函数
    if x > y then x := x - y
    else y := y - x
  x

实际案例

数组求和验证

验证循环正确计算数组元素和：

def arraySum (arr : Array Nat) : Nat :=
  let mut sum := 0
  let mut i := 0
  while i < arr.size do
    invariant sum = ∑ j in Finset.range i, arr[j]  -- 数学式不变式
    sum := sum + arr[i]
    i := i + 1
  sum

其中不变式使用了Finset求和表示法：$\text{sum}=\sum _{j=0}^{i-1}\text{arr}[j]$

二分查找验证

验证经典算法的正确性与终止性：

def binarySearch (arr : Array α) [Ord α] (target : α) : Option Nat :=
  let mut low := 0
  let mut high := arr.size
  while low < high do
    invariant 0 ≤ low ≤ high ≤ arr.size  -- 边界不变式
    invariant ∀ i, i < low → arr[i] < target  -- 值不变式
    invariant ∀ i, i ≥ high → arr[i] ≥ target
    decreasing high - low  -- 显式变体
    let mid := (low + high) / 2
    if arr[mid] < target then
      low := mid + 1
    else
      high := mid
  if low < arr.size ∧ arr[low] = target then some low else none

常见问题

循环验证问题排查

错误类型	可能原因	解决方案
无法证明终止	变体函数未递减	检查循环条件是否严格递减
不变式被破坏	循环体修改了不变式依赖的变量	添加中间断言检查
类型不匹配	不变式与循环状态类型不一致	使用`have`语句显式转换类型

延伸阅读

• 循环不变式的数学归纳法基础
• 霍尔逻辑（Hoare Logic）中的循环规则
• 测度函数的自动推导技术

通过系统应用这些技术，开发者可以构建经严格验证的循环结构，这是形式化方法在软件工程中的重要实践。