跳到主要内容

Lean 有理数

有理数是数学中的基本概念之一，表示可以表示为两个整数之比的数。在 Lean 中，有理数的定义和操作是数学证明和计算的重要组成部分。本文将带你逐步了解 Lean 中有理数的定义、基本操作以及实际应用。

什么是有理数？​

有理数是指可以表示为两个整数之比（分数形式）的数，其中分母不为零。例如，1/2、-3/4 和 5/1 都是有理数。有理数集通常用符号 ℚ 表示。

在 Lean 中，有理数的定义基于整数和分数的概念。Lean 提供了内置的有理数类型 ℚ，并支持有理数的各种操作。

Lean 中的有理数定义​

在 Lean 中，有理数类型 ℚ 是通过 rat 类型实现的。我们可以使用 rat.mk 函数来创建一个有理数，该函数接受两个整数作为参数，分别表示分子和分母。

lean
import data.rat.basic

-- 创建一个有理数 1/2
def half : ℚ := rat.mk 1 2

-- 创建一个有理数 -3/4
def neg_three_fourths : ℚ := rat.mk (-3) 4
备注

注意：rat.mk 函数会自动将分数化简为最简形式。例如，rat.mk 2 4 会返回 1/2。

有理数的基本操作​

Lean 提供了丰富的有理数操作函数，包括加法、减法、乘法和除法。以下是一些基本操作的示例：

lean
-- 定义两个有理数
def a : ℚ := rat.mk 1 2
def b : ℚ := rat.mk 3 4

-- 加法
def sum : ℚ := a + b  -- 结果为 5/4

-- 减法
def diff : ℚ := a - b  -- 结果为 -1/4

-- 乘法
def prod : ℚ := a * b  -- 结果为 3/8

-- 除法
def quot : ℚ := a / b  -- 结果为 2/3
提示

提示：在 Lean 中，有理数的除法会自动处理分母为零的情况，确保不会出现除以零的错误。

有理数的比较​

Lean 还支持有理数的比较操作，包括等于、不等于、大于、小于等。以下是比较操作的示例：

lean
-- 比较两个有理数
def is_equal : bool := a = b  -- 结果为 ff (false)
def is_less : bool := a < b   -- 结果为 tt (true)

实际应用案例​

有理数在数学证明和计算中有广泛的应用。以下是一个简单的实际案例，展示如何在 Lean 中使用有理数进行证明。

案例：证明两个有理数的和是有理数

lean
-- 定义两个有理数
def x : ℚ := rat.mk 1 2
def y : ℚ := rat.mk 3 4

-- 证明 x + y 是有理数
theorem sum_is_rational : ∃ (a b : ℤ), x + y = rat.mk a b :=
begin
  use [5, 4],  -- 5/4 是 x + y 的结果
  refl,
end

在这个案例中，我们定义了两个有理数 x 和 y，并证明了它们的和 x + y 也是一个有理数。

总结​

通过本文，我们了解了 Lean 中有理数的定义、基本操作以及实际应用。有理数是数学中的基本概念，掌握它们在 Lean 中的表示和操作对于进一步学习数学证明和计算至关重要。

附加资源与练习​

  • 练习 1：在 Lean 中定义一个有理数 2/3，并计算它与 1/2 的和。
  • 练习 2：证明两个有理数的乘积仍然是有理数。
  • 附加资源：阅读 Lean 官方文档中关于有理数的部分，了解更多高级操作和定理。

通过不断练习和探索，你将能够熟练地在 Lean 中使用有理数进行数学证明和计算。祝你学习愉快！