Lean有理数

简介

有理数在数学中定义为可以表示为两个整数之比的数，即形如$\frac{a}{b}$（其中$b\ne 0$）的数。在Lean定理证明器中，有理数作为基础数学对象被实现，并支持完整的算术运算和证明功能。本章将详细介绍Lean中有理数的定义、操作及实际应用。

Lean中的有理数表示

在Lean中，有理数类型为ℚ（可通过\Q输入），其底层实现基于分子和分母的规范化存储。以下是一个简单的定义示例：

import data.rat.basic

-- 定义有理数
def q1 : ℚ := 3 / 4  -- 正有理数
def q2 : ℚ := -2 / 5 -- 负有理数

规范化特性

Lean会自动将有理数化简为最简形式，并保证分母为正。例如：

#eval (6 / 8 : ℚ)  -- 输出: 3/4
#eval (-4 / -10 : ℚ) -- 输出: 2/5

基本运算

Lean支持有理数的标准算术运算：

#eval (1/2 + 1/3 : ℚ)  -- 输出: 5/6
#eval (3/4 * 2/3 : ℚ)  -- 输出: 1/2
#eval (5/6 - 1/6 : ℚ)  -- 输出: 2/3
#eval (3/4 / 2/3 : ℚ)  -- 输出: 9/8

比较操作

有理数可通过==, <, >等运算符比较：

#eval (1/2 < 2/3 : bool)  -- 输出: tt (true)
#eval (3/4 == 6/8 : bool) -- 输出: tt (true)

实际案例：分数计算器

以下是一个用Lean实现简单分数计算的例子：

import data.rat.basic

def add_fractions (a b : ℚ) : ℚ := a + b

-- 计算1/2 + 1/4
#eval add_fractions (1/2) (1/4)  -- 输出: 3/4

数学证明中的应用

有理数在数学证明中常用于比例关系的推导。例如证明加法交换律：

theorem rat_add_comm (a b : ℚ) : a + b = b + a :=
begin
  rw add_comm,  -- 使用内置的加法交换律
end

高级主题：有理数与其他类型的转换

与整数的转换

#check rat.cast_int  -- ℤ → ℚ的转换函数
#eval (rat.cast_int 3 : ℚ)  -- 输出: 3/1

与自然数的转换

#check rat.cast_nat  -- ℕ → ℚ的转换函数
#eval (rat.cast_nat 5 : ℚ)  -- 输出: 5/1

性能考虑

有理数运算会产生约分操作，在性能敏感场景需注意：

• 分子分母的值域（避免大整数运算）
• 频繁运算的累积开销

常见问题

为什么1/2在Lean中不是有理数？

在Lean中，未指定类型时1/2会默认为自然数除法（结果为0）。必须显式声明类型：

#eval (1/2 : ℚ)  -- 正确输出: 1/2

如何提取有理数的分子和分母？

使用rat.num和rat.denom：

#eval rat.num (3/4)  -- 输出: 3
#eval rat.denom (3/4) -- 输出: 4

总结

Lean的有理数实现提供了完整的数学运算和证明支持，其特性包括：

• 自动规范化存储
• 完备的算术运算体系
• 与其他数字类型的无缝转换
• 数学证明友好的表示形式

通过合理使用有理数，可以构建精确的数学模型和算法实现。