编辑“︁Lean前置条件”︁

= Lean前置条件 =

前置条件（Preconditions）是程序验证中的一个核心概念，指在函数或方法执行前必须满足的条件。在Lean中，前置条件用于确保程序在正确的状态下运行，从而避免运行时错误或逻辑不一致。通过形式化验证，Lean能够静态检查这些条件是否被满足，从而提高代码的可靠性。

== 基本概念 ==

在Lean中，前置条件通常通过依赖类型（Dependent Types）或命题（Propositions）来表达。例如，一个除法函数可能要求分母不为零，否则会导致未定义行为。前置条件可以是显式的（通过类型系统强制）或隐式的（通过文档说明）。

数学上，前置条件可以表示为：
<math>P \implies Q</math>
其中：
* <math>P</math> 是前置条件
* <math> 是函数执行后必须满足的后置条件

== 代码示例 ==

以下是一个简单的Lean示例，展示如何定义带有前置条件的函数：

<syntaxhighlight lang="lean">
def safeDivide (x : Nat) (y : Nat) (h : y ≠ 0) : Nat :=
  x / y

-- 使用示例
#eval safeDivide 10 2 (by decide)  -- 输出: 5
-- #eval safeDivide 10 0 (by decide)  -- 编译错误：无法证明 `0 ≠ 0`
</syntaxhighlight>

解释：
1. `safeDivide` 是一个安全的除法函数，要求分母 `y` 不为零。
2. 参数 `h` 是前置条件的证明，类型为 `y ≠ 0`。
3. `by decide` 是Lean的自动化证明策略，用于生成简单条件的证明。
4. 如果尝试除以零，Lean会在编译时报错，因为无法满足前置条件。

== 实际应用 ==

前置条件在以下场景中特别有用：
* **输入验证**：确保函数接收有效的输入。
* **资源管理**：例如文件操作前检查文件是否存在。
* **并发控制**：确保线程安全的前置条件。

=== 案例：列表操作 ===

以下是一个操作非空列表的函数示例：

<syntaxhighlight lang="lean">
def head (xs : List α) (h : xs ≠ []) : α :=
  match xs with
  | x :: _ => x

-- 使用示例
#eval head [1, 2, 3] (by decide)  -- 输出: 1
-- #eval head [] (by decide)       -- 编译错误：无法证明 `[] ≠ []`
</syntaxhighlight>

== 高级主题 ==

对于高级用户，Lean允许通过类型类或自定义策略进一步抽象前置条件：

<syntaxhighlight lang="lean">
class NonZero (n : Nat) where
  proof : n ≠ 0

instance : NonZero (n + 1) where
  proof := by simp

def divideWithClass (x : Nat) [NonZero y] : Nat :=
  x / y

-- 自动解析 `NonZero` 实例
#eval divideWithClass 10 (y := 2)  -- 输出: 5
</syntaxhighlight>

== 可视化 ==

前置条件与后置条件的关系可以用以下流程图表示：

<mermaid>
graph LR
    A[调用函数] --> B{检查前置条件}
    B -- 满足 --> C[执行函数体]
    B -- 不满足 --> D[报错]
    C --> E[返回结果并验证后置条件]
</mermaid>

== 总结 ==

前置条件是Lean程序验证的重要组成部分，能够：
* 在编译时捕获潜在错误
* 明确函数的使用约束
* 通过类型系统强制正确性

通过合理使用前置条件，开发者可以编写更安全、更可靠的代码。初学者应从简单的条件开始，逐步掌握依赖类型和命题的使用，而高级用户可探索类型类和策略的扩展应用。

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