编辑“︁Lean不变量”︁

= Lean不变量 =

== 介绍 ==
在程序验证和形式化数学中，'''不变量（Invariant）'''是指在程序执行或数学结构变换过程中始终保持为真的性质。Lean定理证明器使用不变量来验证程序的正确性，特别是在循环、递归或状态转换系统中。不变量是形式化验证的核心工具之一，它能帮助开发者确保程序在任意状态下都满足特定约束条件。

== 基本概念 ==
不变量可以分为多种类型：
* '''循环不变量'''：在循环的每次迭代前后都成立的条件
* '''类不变量'''：在对象生命周期中始终保持的性质
* '''数据结构不变量'''：在数据结构操作后仍然保持的约束

在Lean中，不变量通常表示为命题或谓词，并通过数学归纳或霍尔逻辑进行验证。

== 循环不变量示例 ==
以下是一个简单的Lean4示例，展示如何用不变量验证循环的正确性：

<syntaxhighlight lang="lean">
def sum_to_n (n : Nat) : Nat :=
  let rec loop (i : Nat) (acc : Nat) : Nat :=
    if h : i < n then
      loop (i + 1) (acc + (i + 1))
    else
      acc
  loop 0 0

-- 不变量：acc = Σ_{k=0}^{i-1} k ∧ i ≤ n
theorem sum_to_n_correct (n : Nat) :
  sum_to_n n = n * (n + 1) / 2 := by
  unfold sum_to_n
  sorry  -- 实际证明需要使用不变量
</syntaxhighlight>

在这个例子中，注释描述了循环不变量：累加器`acc`始终包含从0到`i-1`的整数和，且`i`永远不会超过`n`。

== 数据结构不变量 ==
考虑一个简单的有序列表数据结构，其不变量是列表始终保持有序：

<syntaxhighlight lang="lean">
inductive SortedList : List Nat → Prop where
  | nil : SortedList []
  | single (x : Nat) : SortedList [x]
  | cons (x y : Nat) (ys : List Nat) :
      x ≤ y → SortedList (y :: ys) → SortedList (x :: y :: ys)
</syntaxhighlight>

这个定义确保了任何`SortedList`类型的实例都满足排序不变量。

== 不变量验证技术 ==
在Lean中验证不变量通常涉及以下技术：

1. '''数学归纳法'''：对递归结构或循环迭代次数进行归纳
2. '''霍尔逻辑'''：使用前置条件、后置条件和循环不变量
3. '''依赖类型'''：将不变量编码为类型约束

== 实际应用案例 ==
=== 银行账户系统 ===
考虑一个简单的银行账户模型，不变量是余额永远不会为负：

<syntaxhighlight lang="lean">
structure BankAccount where
  balance : Nat
  invariant : balance ≥ 0

def withdraw (account : BankAccount) (amount : Nat) : Option BankAccount :=
  if amount ≤ account.balance then
    some { account with balance := account.balance - amount }
  else
    none
</syntaxhighlight>

类型系统强制要求所有`BankAccount`实例必须满足`balance ≥ 0`的不变量。

== 可视化表示 ==
以下是循环不变量在程序执行过程中的可视化：

<mermaid>
stateDiagram-v2
    [*] --> 初始化
    初始化 --> 循环条件检查: 建立不变量
    循环条件检查 --> 循环体: 条件为真
    循环体 --> 循环条件检查: 保持不变量
    循环条件检查 --> 结束: 条件为假
</mermaid>

== 数学表达 ==
不变量可以用数学公式表示为：
<math>
\forall s \in S, I(s)
</math>
其中：
* <math>S</math>是程序状态空间
* <math>I</math>是不变量谓词

== 常见错误与陷阱 ==
1. '''不变量太弱'''：无法提供有用的保证
2. '''不变量太强'''：难以证明或维护
3. '''忽略边界条件'''：忘记验证初始状态或终止条件
4. '''混淆前置条件与不变量'''：前置条件只在入口处检查，不变量在所有状态都需保持

== 高级主题 ==
对于高级用户，Lean还支持：
* '''共归纳不变量'''：用于无限数据结构或永不终止的程序
* '''概率不变量'''：在概率程序中保持的概率性质
* '''时间不变量'''：在实时系统中需要考虑的时间约束

== 练习建议 ==
1. 为简单循环（如阶乘计算）定义并证明循环不变量
2. 设计一个带有不变量的数据结构（如红黑树）
3. 尝试在现有Lean项目中发现并使用不变量

== 总结 ==
不变量是Lean程序验证中的基础工具，它们提供了程序正确性的形式化保证。通过将不变量编码为类型或命题，Lean可以在编译时验证这些约束，从而减少运行时错误。掌握不变量的定义和使用是成为Lean高级用户的关键步骤。

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