编辑“︁Lean循环验证”︁

{{DISPLAYTITLE:Lean循环验证}}

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

== 核心概念 ==

循环验证主要解决两个关键问题：
# '''循环不变式（Loop Invariant）'''：在每次迭代中保持为真的性质
# '''终止性（Termination）'''：确保循环不会无限执行

在Lean中，循环通常通过递归函数或`while`语法糖实现，验证则依赖以下数学构造：
* 归纳类型（Inductive Types）
* 测度函数（Measure Function）
* 命题等式（Propositional Equality）

== 基础验证模式 ==

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

<syntaxhighlight lang="lean">
def factorial : Nat → Nat
| 0 => 1
| (n + 1) => (n + 1) * factorial n
</syntaxhighlight>

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

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

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

<syntaxhighlight lang="lean">
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
</syntaxhighlight>

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

== 高级验证技术 ==

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

<syntaxhighlight lang="lean">
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
</syntaxhighlight>

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

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

对应Lean实现：

<syntaxhighlight lang="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
</syntaxhighlight>

== 实际案例 ==

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

<syntaxhighlight lang="lean">
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
</syntaxhighlight>

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

=== 二分查找验证 ===
验证经典算法的正确性与终止性：

<syntaxhighlight lang="lean">
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
</syntaxhighlight>

== 常见问题 ==

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

== 延伸阅读 ==

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

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

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean程序验证]]