Lean编程入门：将需求转变为机器验证的定理

测试套件全部通过，程序却依然可能违反一个没人想到去测试的不变式。计数器悄悄越过了上限，重试处理器执行了两次支付，分页函数静默跳过了某些记录。这类缺陷之所以能存活，是因为测试只检查有限的执行样本，而需求描述的却是程序在所有可能执行中都必须成立的性质。

Lean 提供了一条不同的路径：把需求表述为数学命题，写出实现，然后让计算机验证实现确实满足这个命题。你不需要一次性形式化整个应用，从一个函数、一条不变式、一个证明开始就足够。

测试检查样例，规约定义义务

设想一个不允许超过配置上限的计数器自增函数。普通测试套件通常会覆盖三种情况：计数器低于上限时递增；计数器达到上限时保持不变；输入异常大时仍不越界。这些测试都有价值，但假如函数接受的是一个很大的整数域，你该测多少个输入？十个？一千个？一百万个？

对于定义在无界数学整数上的函数，穷举枚举不可能完成。性质测试通过生成大量输入来提升覆盖，而形式化验证走了另一条路：它试图为规约所描述的数学域中的每一个输入建立性质。区别在于，测试检查被选中的执行，证明则对模型所代表的所有执行下断言。

这条思路有深厚的历史根基。1969 年，计算机科学家 C. A. R. Hoare 发表了《An Axiomatic Basis for Computer Programming》，为程序正确性推理奠定了系统化基础。与之相关的核心概念是 Hoare 三元组：{P} C {Q}，其中 P 是前置条件，C 是命令，Q 是后置条件。它的读法是：如果在执行 C 之前 P 成立，那么 C 的终止执行会建立 Q。

对计数器来说，我们可以写出 {current < limit} increment(current) {result = current + 1}，但这只描述了低于上限时的行为，完整的规约还必须覆盖计数器已经到达上限的情况。

Hoare 三元组是程序逻辑中最基础的规约形式之一。{P} C {Q} 中，P 称为前置条件，描述命令执行前必须成立的状态；C 是待分析的命令或程序片段；Q 称为后置条件，描述命令终止后应当成立的状态。三元组的语义是「部分正确性」加上「终止性」时称为完全正确性：若 P 在执行 C 之前成立，则 C 若终止，Q 必然成立；若附加终止证明，则得到总正确性。

这种写法把「程序做什么」与「程序如何做到」分开：三元组本身不提及实现细节，只声明条件之间的蕴含关系。它的价值在于为推理提供组合规则——顺序、条件、循环各有对应的推导规则，使得复杂程序的正确性可以被拆解为局部条件的验证。Lean 中的规约写法（前置条件作为定理的假设参数，后置条件作为结论）正是 Hoare 风格的现代变体：h : current < limit 就像前置条件，boundedInc limit current = current + 1 就像后置条件。

把需求翻译成数学契约

从三条需求出发：结果永远不超过上限；当前值低于上限时加一；当前值已达到或超过上限时返回上限。在 Lean 中，实现可以写成：

def boundedInc (limit current : Nat) : Nat :=
  if current < limit then current + 1 else limit

这里 Nat 是 Lean 的自然数类型，函数接收两个自然数并返回自然数，if ... then ... else ... 根据比较结果选择分支。

接下来脱离实现来规约所需行为：

def BoundedIncSpec (limit current result : Nat) : Prop :=
  result <= limit ∧
  (current < limit -> result = current + 1) ∧
  (limit <= current -> result = limit)

这个定义引入了三项义务。result <= limit 要求结果不越界；∧ 表示逻辑与，两个命题都必须成立；P -> Q 表示若 P 成立则 Q 必然成立；Prop 是 Lean 的命题类型。

值得留意的是，result 是一个独立参数。我们描述了什么算正确结果，却没有假设结果如何计算。这种分离很关键：同一个规约可以被不同实现满足——条件表达式、库函数，或针对特定环境优化过的复杂实现。规约描述义务，实现提供机制。另一个微妙之处在于，规约刻意只针对自然数和已声明的需求，它并不要求函数保留输入超出上限多少的信息。形式化规约迫使我们区分本质需求与偶然的实现细节。

Lean 中的 Prop 与 Bool 有本质区别，理解这一区别对读懂形式化规约至关重要。Bool 是一个只有 true 和 false 两个值的数据类型，可以参与计算、模式匹配，也可在 if 中使用；Prop 则是命题的类型，其元素是「证明」而不是布尔值。命题 result <= limit 的类型是 Prop，一个该命题的证明就是一个类型为 result <= limit 的项。

这一设计（源自 Curry–Howard 对应）把「命题为真」等价于「类型非空」：证明某个命题，就是在构造该类型的一个元素。因此 Lean 中 ∧、->、¬ 等逻辑连接词分别对应积类型、函数类型、函数到空类型，constructor、intro、exact 等策略本质上是在构造这些项。规约使用 Prop 的好处是：规约是数学命题，不依赖任何运行时求值，也不假定某次具体执行，因而能描述「所有输入」上的义务，而不是某次布尔判定的结果。

证明实现满足契约

有了函数和规约，Lean 能否对每一对可能的自然数证明函数满足规约？下面是一个使用 Mathlib（Lean 的数学库）的完整示例：

import Mathlib

def boundedInc (limit current : Nat) : Nat :=
  if current < limit then current + 1 else limit

def BoundedIncSpec (limit current result : Nat) : Prop :=
  result <= limit ∧
  (current < limit -> result = current + 1) ∧
  (limit <= current -> result = limit)

theorem boundedInc_le_limit (limit current : Nat) :
    boundedInc limit current <= limit := by
  unfold boundedInc
  split_ifs <;> omega

theorem boundedInc_eq_succ (limit current : Nat)
    (h : current < limit) :
    boundedInc limit current = current + 1 := by
  simp [boundedInc, h]

theorem boundedInc_eq_limit (limit current : Nat)
    (h : limit <= current) :
    boundedInc limit current = limit := by
  have h' : ¬ current < limit := by omega
  simp [boundedInc, h']

theorem boundedInc_correct (limit current : Nat) :
    BoundedIncSpec limit current (boundedInc limit current) := by
  unfold BoundedIncSpec
  constructor
  · exact boundedInc_le_limit limit current
  constructor
  · intro h
    exact boundedInc_eq_succ limit current h
  · intro h
    exact boundedInc_eq_limit limit current h

主结果是最后的定理 boundedInc_correct：对每一个自然数上限和每一个自然数当前值，boundedInc 的结果都满足规约。这里没有有限的测试集，定理覆盖了整个声明的输入域。

证明如何运作？boundedInc_le_limit 建立结果不越界：unfold 展开函数定义，split_ifs 拆分条件语句的两个分支，omega 求解由此产生的自然数算术义务。boundedInc_eq_succ 在前置条件下证明递增行为，simp 利用假设化简条件式。boundedInc_eq_limit 证明另一分支：在 limit <= current 的前提下，omega 证明 current < limit 不可能成立。最后 boundedInc_correct 把三个结果组合起来，constructor 将合取式拆解为组成义务，每项义务由前面某个定理消解。

关键字 by 引入用策略构造的证明，Lean 检查最终证明是否建立了所述命题。策略只是构造证明的便捷手段，不能替代证明检查——Lean 的可信内核会检查最终生成的证明项。这个区别是根本性的：机器不是单纯接受开发者关于函数正确的断言，而是检查一个证明实现满足命题的形式化论证。

文中反复出现的 tactic（策略） 与 证明项（proof term） 是 Lean 证明体系的两个层次。策略是构造证明的脚本，例如 unfold 展开定义、simp 化简、omega 求解 Presburger 算术、split_ifs 拆分条件式、constructor 分解合取。策略执行后并不「证明」命题本身，而是生成一个证明项。

Lean 的可信内核（kernel）独立于所有策略，只检查生成的证明项是否确实具有所声明的类型。这个设计的工程意义在于：即使某个策略实现有 bug，只要内核通过，被检查的结论仍然成立。与之相对，axiom 或 sorry 会绕过检查，前者引入未经证明的假设，后者直接关闭证明义务。因此「Lean 接受了证明」这句话的严格含义是「内核校验了一个类型为所声明命题的项」。理解这一点，才能理解为什么策略出错不会损害可信度，以及为什么审计者应当关注是否使用了 sorry 和自定义公理。

准确理解证明到底建立了什么

把一个经过验证的函数理解为“对应生产功能不可能失败”的保证，这个结论太宽泛了。我们的定理证明的是自然数上数学函数的性质，它没有证明使用 32 位整数的生产实现行为相同。32 位无符号整数有有限可表示范围，边界附近的算术可能回绕、陷入陷阱或遵循其他指定的行为，而 Lean 的 Nat 不施加这种机器级限制。要验证生产版本，需要构造能表示相关整数边界与行为的模型，再证明该模型与实现具有相应性质。

同样的区分适用于外部系统。关于授权函数的证明不会自动证明数据库事务原子提交、远程身份提供者返回可信数据，或网络重试不会重复产生外部副作用。这些是彼此独立的义务。有用的验证项目因此会明确写出假设与边界：函数对输入做了什么假设？证明建立了哪些性质？哪些性质依赖运行时、编译器、数据库或外部服务？

还有一个值得理解的局限：一个形式化验证过的实现可以完美满足一个错误的规约。 假设业务要求是客户取款永远不能超过可用余额，而开发者错误地规约成取款永远不能超过账户创建时的原始余额。Lean 或许能帮助证明后者，但它无法确立业务需求一开始被正确捕获。形式化验证减少了规约的歧义，为实现的符合性提供了证据，但判断规约是否描述了我们真正想要的系统，仍然需要人的判断。

从函数契约走向状态不变式

许多重要软件性质不只关乎函数的输出，还关乎系统状态如何随时间变化。考虑库存管理：应用跟踪产品有多少单位可用、多少单位已预留。客户下单时，系统必须把单位从可用库存转移到预留库存。两条需求立刻浮现：预留消耗的单位不能超过可用量；成功的预留必须保持被跟踪的总单位数守恒。

用结构体表示状态：

structure Inventory where
  available : Nat
  reserved : Nat

定义预留操作，库存充足时返回更新后的状态，否则失败：

def reserve (i : Inventory) (qty : Nat) : Option Inventory :=
  if qty <= i.available then
    some {
      available := i.available - qty
      reserved := i.reserved + qty
    }
  else
    none

Option Inventory 要么表示成功结果（some updatedInventory），要么表示失败（none）。现在可以表达一条有用的不变式：操作成功时，可用与预留之和保持不变。

theorem reserve_preserves_total
    (i : Inventory) (qty : Nat) (next : Inventory)
    (h : reserve i qty = some next) :
    next.available + next.reserved =
      i.available + i.reserved := by
  unfold reserve at h
  split_ifs at h with hEnough
  · injection h with hNext
    cases hNext
    simp
    omega
  · simp at h

这条定理不是测试预留三个单位或十个单位，而是覆盖每个自然数库存状态和每个请求数量：只要操作返回成功结果，被跟踪的总库存就守恒。关键假设是 reserve 的结果等于 some next；在成功分支中，Lean 可以用这个等式把返回状态与实现构造的状态对应起来，算术证明随后由“请求量未超过可用量”这一条件推出。

这说明了为什么按不变式思考很有价值。状态不变式是在允许的状态迁移中应始终保持为真的性质，例如：预留与可用资源之和保持不变；金融余额永不为负；已完成的订单不能回到待处理状态；用户不能通过未授权迁移获得权限；分布式协议在形式化假设下永不进入被禁止的状态组合。

在生产环境中，库存正确性还涉及数据库事务、并发预留、库存调整和重试等额外问题。上面的定理只证明了被建模操作的性质，它没有确立真实的数据库应用原子地实现了该操作。即便如此，这个证明为后续验证工作提供了一个精确的地基。对开发者而言，这是一种有用的模式：隔离状态迁移，写下什么必须保持为真，然后证明每条允许的迁移都保持这条不变式。

状态不变式与函数契约的关系值得单独澄清。函数契约刻画单个操作的前置/后置条件，例如 {qty ≤ available} reserve {total 守恒}；状态不变式则是一个关于状态的命题 I(s)，要求它在所有允许的迁移中保持不变，即对任意满足 I(s) 的 s 与任意合法迁移 t，I(t(s)) 仍成立。

两者配合使用时通常还需要「保持性证明」：若 I(s) 成立且操作成功返回 s'，则 I(s') 成立。文章中的 reserve_preserves_total 正是这样一条保持性定理，它把「总单位数守恒」从一个直觉性约束变成了可被机器检查的局部义务。在更大的系统中，不变式可以跨多个操作组合：初始状态满足 I、每个迁移保持 I，就能归纳证明系统运行到任意步数后 I 仍成立。这正是把单条不变式扩展成系统级保证的标准路径，也是后续若要验证并发、事务等更复杂模型时必须先建立的地基。

把规约集成进开发流程

证明只有在成为常规工程流程的一部分、而非孤立的研究练习时，才最有价值。一个可行的流程是：写出需求 → 定义模型与契约 → 实现函数 → 证明契约 → Lean 是否接受证明？若否，审查代码、证明与规约并回到证明步骤；若是，审查假设与系统边界，然后在 CI 中运行测试与验证。

从纯函数开始：输出只依赖输入、没有外部副作用的函数更容易规约，因为描述其行为不需要建模数据库、网络连接、时钟或可变环境。对已有应用，找到一个计算或状态迁移，尽量把它与周围的 I/O 分离，用 Lean 定义其输入、输出与不变式，证明所需性质，并把这些定义和证明与实现放在一起。随后把相关的构建与验证命令加入持续集成：如果某个代码改动使定理无法证明，验证构建就应当失败。

这之所以有价值，是因为它把不变式变成了明确的工程约束。团队不再依赖每个未来开发者记住某个条件为何重要，而是维护一个经过检查、必须持续成立的命题。形式化还能改善代码审查：一位审查者可以独立于实现检查规约，追问它是否捕获了预期行为；另一位审查者可以专注于证明及其假设。这种分离让两个不同的问题变得可见——我们实现的需求对吗？实现满足这个需求吗？

测试仍然是这个流程的一部分。单元测试检验具体样例，集成测试检查与依赖的交互，运维监控揭示部署环境中的实际行为。Lean 贡献的是另一种形式的证据：关于代码被建模性质的一个证明。务实的采用策略是从一个小部件开始，把它的证明集成进构建，只有在这个方法被证明对团队有用时才扩展。

从一条不变式开始

最有效的第一个 Lean 项目，多半不是完整应用，也不是试图验证现有代码库的每一行。选择一个带有有意义不变式的函数：有界计数器、分页辅助函数、资源分配器、校验例程，或某个状态迁移。精确陈述需求，编码实现，证明实现满足需求。

这个更宏大的想法自程序逻辑的奠基时代就已存在。Lean 把这种推理风格带进了现代编程环境，把可执行定义、数学命题、证明自动化与机器检查的证明结合在一起。转变在于：从“记录代码应该做什么”，走向“编码一个机器可以对照实现的正式模型来检查的需求”。保证的范围取决于规约的质量和模型的边界，这让选择正确的不变式本身成为一项重要的工程任务。

你的代码库中，哪一条不变式最值得变成机器可检查的定理？