编辑“︁Lean整数”︁（章节）

= Lean整数 =

== 介绍 ==  
'''Lean整数'''是[[Lean定理证明器]]中用于表示数学整数的基本类型，属于Lean数学库（Mathlib）的核心组成部分。整数在Lean中定义为自然数的扩展，包含正整数、零和负整数（<math>\mathbb{Z} = \{\ldots, -2, -1, 0, 1, 2, \ldots\}</math>）。Lean通过内置类型`Int`和一系列定理、操作符支持整数的运算与证明。

== 定义与表示 ==  
在Lean中，整数通过归纳类型定义，其核心结构如下：  
<syntaxhighlight lang="lean">  
inductive Int  
| ofNat   : Nat → Int  -- 非负整数（包含零）  
| negSucc : Nat → Int  -- 负整数（如 -n-1）  
</syntaxhighlight>  

* `ofNat n` 表示自然数`n`对应的非负整数（如`ofNat 3 = 3`）。  
* `negSucc n` 表示`-n-1`（如`negSucc 0 = -1`）。  

=== 示例 ===  
<syntaxhighlight lang="lean">  
#check Int.ofNat 5      -- 输出: 5 : Int  
#check Int.negSucc 2    -- 输出: -3 : Int  
</syntaxhighlight>  

== 基本运算 ==  
Lean提供标准算术运算，包括加法、减法、乘法和比较。以下是常见操作符：  

<syntaxhighlight lang="lean">  
-- 加法  
#eval (1 : Int) + (-3)  -- 输出: -2  

-- 乘法  
#eval (4 : Int) * (-2)  -- 输出: -8  

-- 绝对值  
#eval Int.abs (-7)      -- 输出: 7  
</syntaxhighlight>  

== 定理与证明 ==  
Lean允许通过定理证明整数的性质。例如，证明加法交换律：  
<syntaxhighlight lang="lean">  
theorem add_comm (a b : Int) : a + b = b + a := by  
  induction a, b with  
  | ofNat n, ofNat m => simp [Int.add]  
  | negSucc n, negSucc m => simp [Int.add]  
  -- 其他情况省略  
</syntaxhighlight>  

== 实际应用案例 ==  
=== 案例1：欧几里得算法 ===  
计算最大公约数（GCD）的经典算法实现：  
<syntaxhighlight lang="lean">  
def gcd : Int → Int → Int  
| a, 0 => Int.abs a  
| a, b => gcd b (a % b)  

#eval gcd 18 (-12)  -- 输出: 6  
</syntaxhighlight>  

=== 案例2：解线性方程 ===  
验证方程<math>2x + 3 = 7</math>的解：  
<syntaxhighlight lang="lean">  
def solve_linear (a b c : Int) : Option Int :=  
  if a ≠ 0 then some ((c - b) / a) else none  

#eval solve_linear 2 3 7  -- 输出: some 2  
</syntaxhighlight>  

== 可视化表示 ==  
整数与自然数的关系可通过以下Mermaid图展示：  
<mermaid>  
graph LR  
  N[Nat] -->|ofNat| Z[Int]  
  N -->|negSucc| Z  
</mermaid>  

== 进阶主题 ==  
* '''类型转换'''：`Int`与`Nat`的相互转换需注意负数处理。  
* '''性能优化'''：大整数运算依赖Lean的底层表示。  

== 总结 ==  
Lean整数是数学证明和编程中不可或缺的基础类型，通过`Int`类型和Mathlib库支持丰富的操作与证明。初学者可通过简单运算入门，高级用户可探索其形式化验证能力。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean数学基础]]