Lean整数

Lean整数

介绍

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

定义与表示

在Lean中，整数通过归纳类型定义，其核心结构如下：

  
inductive Int  
| ofNat   : Nat → Int  -- 非负整数（包含零）  
| negSucc : Nat → Int  -- 负整数（如 -n-1）

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

示例

  
#check Int.ofNat 5      -- 输出: 5 : Int  
#check Int.negSucc 2    -- 输出: -3 : Int

基本运算

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

  
-- 加法  
#eval (1 : Int) + (-3)  -- 输出: -2  

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

-- 绝对值  
#eval Int.abs (-7)      -- 输出: 7

定理与证明

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]  
  -- 其他情况省略

实际应用案例

案例1：欧几里得算法

计算最大公约数（GCD）的经典算法实现：

  
def gcd : Int → Int → Int  
| a, 0 => Int.abs a  
| a, b => gcd b (a % b)  

#eval gcd 18 (-12)  -- 输出: 6

案例2：解线性方程

验证方程$2x+3=7$的解：

  
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

可视化表示

整数与自然数的关系可通过以下Mermaid图展示：

graph LR N[Nat] -->|ofNat| Z[Int] N -->|negSucc| Z

进阶主题

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

总结

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