编辑“︁Lean标准库简介”︁（章节）

= Lean标准库简介 =

Lean标准库是Lean编程语言的核心组成部分，它提供了基础数据类型、函数、定理和证明工具，使开发者能够高效地进行形式化验证和数学证明。本节将详细介绍Lean标准库的结构、核心模块及其应用场景。

== 概述 ==
Lean标准库（通常称为`Std`或`Mathlib`）是一个经过形式化验证的库，包含以下关键功能：
* 基础数据类型（如`Nat`, `Int`, `List`）
* 逻辑构造（如命题、谓词逻辑）
* 代数结构（如群、环、域）
* 数学分析工具（如极限、导数）

标准库的设计遵循模块化原则，允许用户按需导入功能。例如：
<syntaxhighlight lang="lean">
import Std.Data.List.Basic
import Mathlib.Algebra.Group.Defs
</syntaxhighlight>

== 核心模块 ==
=== 基础数据类型 ===
Lean内置了以下基础类型：

<mermaid>
graph TD
    A[基础类型] --> B[Bool]
    A --> C[Nat]
    A --> D[Int]
    A --> E[String]
    A --> F[List α]
</mermaid>

示例：使用`Nat`类型进行递归计算
<syntaxhighlight lang="lean">
def factorial : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

#eval factorial 5  -- 输出: 120
</syntaxhighlight>

=== 逻辑系统 ===
标准库实现了直觉逻辑和经典逻辑工具：
* 命题连接词：<math>\forall, \exists, \land, \lor</math>
* 证明构造器：`have`, `show`, `by_contra`

示例：构造一个简单命题证明
<syntaxhighlight lang="lean">
example (P Q : Prop) : P → Q → P ∧ Q :=
  fun hp hq => ⟨hp, hq⟩
</syntaxhighlight>

== 数学库（Mathlib）==
Mathlib是标准库的扩展，包含超过10万条形式化数学定义：

<mermaid>
pie
    title Mathlib内容分布
    "代数" : 35
    "分析" : 25
    "几何" : 20
    "数论" : 15
    "其他" : 5
</mermaid>

实际案例：证明平方数性质
<syntaxhighlight lang="lean">
import Mathlib.Algebra.Parity

theorem even_square {n : ℤ} (h : Even n) : Even (n^2) := by
  rw [Even] at h ⊢
  obtain ⟨k, rfl⟩ := h
  use 2 * k^2
  ring
</syntaxhighlight>

== 高级特性 ==
=== 类型类系统 ===
Lean通过类型类实现多态：
<syntaxhighlight lang="lean">
class Monoid (α : Type) where
  mul : α → α → α
  one : α

instance : Monoid Nat where
  mul := Nat.mul
  one := 1
</syntaxhighlight>

=== 元编程 ===
标准库提供宏系统用于代码生成：
<syntaxhighlight lang="lean">
macro "triv" : tactic => `(tactic| exact True.intro)

example : True := by triv
</syntaxhighlight>

== 最佳实践 ==
1. 使用`import`语句时指定最小依赖
2. 优先使用Mathlib中已验证的定理
3. 利用`#check`和`#print`命令探索库定义

== 总结 ==
Lean标准库为形式化数学和验证编程提供了坚实基础。通过组合基础模块和数学库，用户可以：
* 构建从简单到复杂的证明
* 开发经过验证的算法
* 探索高阶数学结构

建议初学者从`Std.Data`和`Mathlib.Init`模块开始逐步探索。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean与数学库]]