6. 结构体（Structures）

现代数学广泛使用了代数结构，这些代数结构封装了可在不同环境中实例化的模式，而且往往有多种方法来对它们进行定义和实例化。

因此，Lean 提供了相应的方法来形式化定义这些结构并对其进行操作。 此前你已经接触过一些代数结构的示例，比如在 Chapter 2 中的环（rings）和格（lattices）。 本章将解释之前出现过的方括号语法，比如 [Ring α]、 [Lattice α]，并介绍如何创建和使用自定义的代数结构。

如需了解更多技术细节，可以参考 Theorem Proving in Lean， 以及 Anne Baanen 的这篇论文 Use and abuse of instance parameters in the Lean mathematical library。

6.1. 定义结构体

广义上来说，结构体是对特定形式数据集合的约定，包括包含数据的形式以及这些数据要满足的一些约束条件。 而结构体的实例则是某一组满足约束的具体数据。例如，我们可以规定一个点是由三个实数组成的三元组：

@[ext]
structure Point where
  x : ℝ
  y : ℝ
  z : ℝ

上面用到的 @[ext] 注解让 Lean 自动生成一个定理，内容是当该结构体的两个实例各组成部分对应相同时，这两个实例相等。该属性也称为外延性（extensionality）。

#check Point.ext

example (a b : Point) (hx : a.x = b.x) (hy : a.y = b.y) (hz : a.z = b.z) : a = b := by
  ext
  repeat' assumption

接着我们定义一个 Point 结构体的实例。 Lean 提供多种实例化方式来达成目的。

def myPoint1 : Point where
  x := 2
  y := -1
  z := 4

def myPoint2 : Point :=
  ⟨2, -1, 4⟩

def myPoint3 :=
  Point.mk 2 (-1) 4

第一个例子中，我们明确地指明了结构体的各个字段。 在定义 myPoint3 时用到的函数 Point.mk 叫做 Point 结构体的构造函数（constructor），用于构造结构体成员。 你也可以为构造函数指定一个不同的名字，比如 build。

structure Point' where build ::
  x : ℝ
  y : ℝ
  z : ℝ

#check Point'.build 2 (-1) 4

接下来的两个例子展示了如何定义结构体的函数。 第二个例子中明确指出了构造函数 Point.mk 中的字段名，而第一个例子则使用更为简洁的匿名构造函数。 Lean 能根据 add 的目标类型推断出所需的构造函数。 通常，我们会将与结构体（例如这里的 Point）相关的定义和定理放在一个同名的命名空间（namespace）中。 在下面的示例中，由于我们启用了 Point 命名空间，所以 add 的完整名称实际是 Point.add。 当命名空间没被启用时，就得使用完整名称。 不过这时也可以使用匿名投影记号（anonymous projection notation），它允许我们用 a.add b 代替 Point.add a b。 因为 a 的类型是 Point，Lean 能在没有开启对应命名空间的时候将 a.add b 推断为 Point.add a b。

namespace Point

def add (a b : Point) : Point :=
  ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩

def add' (a b : Point) : Point where
  x := a.x + b.x
  y := a.y + b.y
  z := a.z + b.z

#check add myPoint1 myPoint2
#check myPoint1.add myPoint2

end Point

#check Point.add myPoint1 myPoint2
#check myPoint1.add myPoint2

接下来我们继续在相关命名空间中添加定义，但在引用的代码片段中会省略开关命名空间相关的指令。 在证明加法函数性质时，可使用 rw 来展开定义，并用 ext 将结构体两个实例之间的等号转化为它们各个组成部分之间的等号。 下面的代码使用 protected 关键字，使得在命名空间打开的情况下定理的名字依然是 Point.add_comm。 当我们希望避免与泛型定理如 add_comm 产生歧义时，这样做是有帮助的。

protected theorem add_comm (a b : Point) : add a b = add b a := by
  rw [add, add]
  ext <;> dsimp
  repeat' apply add_comm

example (a b : Point) : add a b = add b a := by simp [add, add_comm]

因为 Lean 能在内部自动展开定义并简化投影，所以有时我们需要的等式在定义上就自动成立。

theorem add_x (a b : Point) : (a.add b).x = a.x + b.x :=
  rfl

与在 Section 5.2 中定义递归函数类似，我们定义函数时也可以使用模式匹配。 下面定义的 addAlt 和 addAlt' 本质上是相同的，形式上的的区别在于我们在后者的定义中使用了匿名构造函数。 虽然以此方式定义函数有时会显得更加简洁，并且结构化 η-规约（structural eta-reduction）也确保了这种简写在定义上的等价性，但这么做可能会为后续的证明带来不便。

def addAlt : Point → Point → Point
  | Point.mk x₁ y₁ z₁, Point.mk x₂ y₂ z₂ => ⟨x₁ + x₂, y₁ + y₂, z₁ + z₂⟩

def addAlt' : Point → Point → Point
  | ⟨x₁, y₁, z₁⟩, ⟨x₂, y₂, z₂⟩ => ⟨x₁ + x₂, y₁ + y₂, z₁ + z₂⟩

theorem addAlt_x (a b : Point) : (a.addAlt b).x = a.x + b.x := by
  rfl

theorem addAlt_comm (a b : Point) : addAlt a b = addAlt b a := by
  rw [addAlt, addAlt]
  -- the same proof still works, but the goal view here is harder to read
  ext <;> dsimp
  repeat' apply add_comm

数学构造通常涉及将捆绑的信息拆分开来，并以不同的方式重新组合。 这也是 Lean 和 Mathlib 提供如此多方法来高效处理这些操作的原因。 作为练习，请尝试证明 Point.add 是满足结合律的。 然后请定义点的标量乘法并证明其满足对加法的分配律。

protected theorem add_assoc (a b c : Point) : (a.add b).add c = a.add (b.add c) := by
  sorry

def smul (r : ℝ) (a : Point) : Point :=
  sorry

theorem smul_distrib (r : ℝ) (a b : Point) :
    (smul r a).add (smul r b) = smul r (a.add b) := by
  sorry

使用结构体是走向代数抽象的第一步。 我们目前还没有方法将 Point.add 与泛型的 + 符号联系起来， 抑或是将 Point.add_comm、Point.add_assoc 与泛型的 add_comm、add_assoc 定理联系起来。 这些任务属于结构体在代数层面的应用，我们将在下一节介绍如何具体实现。 对现在来说，我们只需要把结构体视作一种捆绑对象和信息的方法。

在结构体中我们不仅可以指定数据类型，还可以指定数据需要满足的约束。 在 Lean 中，后者被表示为类型 Prop 的字段。 例如，标准2-单纯形（standard 2-simplex）定义为满足 \(x ≥ 0\)，\(y ≥ 0\)，\(z ≥ 0\)，\(x + y + z = 1\) 的点 \((x, y, z)\) 的集合。 如果你不熟悉这个概念，可以画个图，其实这个集合就是三维空间中以 \((1, 0, 0)\)，\((0, 1, 0)\)，和 \((0, 0, 1)\) 为顶点的等边三角形以及其内部。 在 Lean 中可以这样形式化表示：

structure StandardTwoSimplex where
  x : ℝ
  y : ℝ
  z : ℝ
  x_nonneg : 0 ≤ x
  y_nonneg : 0 ≤ y
  z_nonneg : 0 ≤ z
  sum_eq : x + y + z = 1

请注意，最后四个字段用到的 x，y，z 指的就是前三个字段。 我们可以定义一个从2-单纯形到其自身的映射，该映射交换 x 和 y：

def swapXy (a : StandardTwoSimplex) : StandardTwoSimplex
    where
  x := a.y
  y := a.x
  z := a.z
  x_nonneg := a.y_nonneg
  y_nonneg := a.x_nonneg
  z_nonneg := a.z_nonneg
  sum_eq := by rw [add_comm a.y a.x, a.sum_eq]

有趣的来了，我们可以计算单纯形内两个点的中点。 为此需要先在文件开头加上 noncomputable section 语句以便使用实数上的除法。

noncomputable section

def midpoint (a b : StandardTwoSimplex) : StandardTwoSimplex
    where
  x := (a.x + b.x) / 2
  y := (a.y + b.y) / 2
  z := (a.z + b.z) / 2
  x_nonneg := div_nonneg (add_nonneg a.x_nonneg b.x_nonneg) (by norm_num)
  y_nonneg := div_nonneg (add_nonneg a.y_nonneg b.y_nonneg) (by norm_num)
  z_nonneg := div_nonneg (add_nonneg a.z_nonneg b.z_nonneg) (by norm_num)
  sum_eq := by field_simp; linarith [a.sum_eq, b.sum_eq]

上面的代码中，对于 x_nonneg，y_nonneg，z_nonneg，我们用简洁的证明项即可建立。 而对于 sum_eq ，我们选择使用 by 在策略模式下进行证明。

给定参数 \(\lambda\) 满足 \(0 \le \lambda \le 1\)， 可定义标准2-单纯形中 \(a\) 和 \(b\) 两点的加权平均为 \(\lambda a + (1 - \lambda) b\)。 请尝试参考前面的 midpoint 形式化定义该加权平均。

def weightedAverage (lambda : Real) (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1)
    (a b : StandardTwoSimplex) : StandardTwoSimplex :=
  sorry

结构体还可以依赖于参数。 例如，可以将标准2-单纯形推广到任意维数 \(n\) 下的 \(n\) -单纯形。 目前阶段，你不需要对 Fin n 了解太多，只需知道它有 \(n\) 个元素，并且 Lean 直到如何在其上进行就和操作即可。

open BigOperators

structure StandardSimplex (n : ℕ) where
  V : Fin n → ℝ
  NonNeg : ∀ i : Fin n, 0 ≤ V i
  sum_eq_one : (∑ i, V i) = 1

namespace StandardSimplex

def midpoint (n : ℕ) (a b : StandardSimplex n) : StandardSimplex n
    where
  V i := (a.V i + b.V i) / 2
  NonNeg := by
    intro i
    apply div_nonneg
    · linarith [a.NonNeg i, b.NonNeg i]
    norm_num
  sum_eq_one := by
    simp [div_eq_mul_inv, ← Finset.sum_mul, Finset.sum_add_distrib,
      a.sum_eq_one, b.sum_eq_one]
    field_simp

end StandardSimplex

作为额外练习，请尝试定义一下标准 :math`n` -单纯形中两点的加权平均。 可以使用 Finset.sum_add_distrib 和 Finset.mul_sum 来实现相关的求和操作。

前面我们已经了解到结构体可以用来将数据和属性打包在一起。 有趣的是，结构体也可以用来打包脱离具体数据的抽象属性。 例如，下面的结构体 IsLinear，将线性性（linearity）的两个主要组成部分打包在了一起。

structure IsLinear (f : ℝ → ℝ) where
  is_additive : ∀ x y, f (x + y) = f x + f y
  preserves_mul : ∀ x c, f (c * x) = c * f x

section
variable (f : ℝ → ℝ) (linf : IsLinear f)

#check linf.is_additive
#check linf.preserves_mul

end

值得一提的是，结构体并不是打包数据的唯一方法。 前面提到的 Point 数据结构也可以用泛型乘积类型来定义，而 IsLinear 可以使用简单的 and 来定义。

def Point'' :=
  ℝ × ℝ × ℝ

def IsLinear' (f : ℝ → ℝ) :=
  (∀ x y, f (x + y) = f x + f y) ∧ ∀ x c, f (c * x) = c * f x

泛型类型构造甚至可以替代包含依赖关系的结构体。 例如，子类型（subtype）构造结合了一段数据以及一条属性。 你可以将下面例子中的 PReal 看作正实数类型。 每个 x : PReal 都有两个分量：它的值，以及“它是正的”这一属性。 你可以分别用 x.val 与 x.property 来访问这两个分量，其中前者的类型为 ℝ，后者是一个属性 0 < x.val。

def PReal :=
  { y : ℝ // 0 < y }

section
variable (x : PReal)

#check x.val
#check x.property
#check x.1
#check x.2

end

我们也可以用子类型来定义前面的标准2-单纯形，以及任意维数 \(n\) 下的标准 \(n\) -单纯形。

def StandardTwoSimplex' :=
  { p : ℝ × ℝ × ℝ // 0 ≤ p.1 ∧ 0 ≤ p.2.1 ∧ 0 ≤ p.2.2 ∧ p.1 + p.2.1 + p.2.2 = 1 }

def StandardSimplex' (n : ℕ) :=
  { v : Fin n → ℝ // (∀ i : Fin n, 0 ≤ v i) ∧ (∑ i, v i) = 1 }

类似地，Sigma 类型是有序对的推广，其中第二个分量的类型依赖于第一个分量。

def StdSimplex := Σ n : ℕ, StandardSimplex n

section
variable (s : StdSimplex)

#check s.fst
#check s.snd

#check s.1
#check s.2

end

给定 s : StdSimplex，它的第一个分量 s.fst 是个自然数，第二个分量是对应维数下标准单纯形中的一个元素 StandardSimplex s.fst。 Sigma 类型与子类型的区别在于 Sigma 类型的第二个分量是数据而非属性。

尽管可以使用乘积类型、子类型、 Sigma 类型等替代结构体，但使用结构体其实有许多好处。 定义结构体可以抽象出底层的表达，且能为成员提供自定义的名称以供访问。 这使得证明更加健壮： 对于那些仅依赖结构体接口的证明，通常只需用新接口替换旧接口，就能让证明代码在结构体定义变更后依然有效。 此外，正如我们即将看到的，Lean 支持将各种结构体编织成一个丰富的、相互关联的层次体系，以管理它们之间的交互关系。

6.2. 代数结构

为了阐明我们所说的 代数结构 这一短语的含义，考虑一些例子会有所帮助。

1. 偏序集 由集合 \(P\) 以及定义在 \(P\) 上的二元关系 \(\le\) 组成，该关系具有传递性和自反性。

2. 群 由集合 \(G\) 以及其上的一个结合二元运算、一个单位元 \(1\) 和一个将 \(G\) 中每个元素 \(g\) 映射为其逆元 \(g^{-1}\) 的函数 \(g \mapsto g^{-1}\) 构成。若运算满足交换律，则称该群为阿贝尔群或交换群。

3. 格 是一种具有交和并运算的部分有序集。

4. 环 由一个（加法表示的）阿贝尔群 \((R, +, 0, x \mapsto -x)\) 以及一个结合的乘法运算 \(\cdot\) 和一个单位元 \(1\) 组成，并且乘法对加法满足分配律。如果乘法是可交换的，则称环为 交换环 。

5. 一个 有序环 \((R, +, 0, -, \cdot, 1, \le)\) 由一个环以及其元素上的一个偏序关系组成，满足以下条件：对于 \(R\) 中的任意 \(a\)、\(b\) 和 \(c\)，若 \(a \le b\)，则 \(a + c \le b + c\)；对于 \(R\) 中的任意 \(a\) 和 \(b\)，若 \(0 \le a\) 且 \(0 \le b\)，则 \(0 \le a b\)。

#. 度量空间 由一个集合 \(X\) 和一个函数 \(d : X \times X \to \mathbb{R}\) 组成，满足以下条件： - 对于集合 X 中的任意 x 和 y，有 \(d(x, y) \ge 0\) 。 - 当且仅当 x = y 时，\(d(x， y) = 0\) 。 - 对于集合 X 中的任意 x 和 y，有 \(d(x， y) = d(y， x)\) 。 - 对于集合 X 中的任意 x、y 和 z，有 \(d(x, z) \le d(x, y) + d(y， z)\) 。

#. 拓扑空间 由集合 \(X\) 以及 \(X\) 的子集所构成的集合 \(\mathcal T\) 组成，这些子集被称为 \(X\) 的开子集，且满足以下条件： - 空集和 \(X\) 是开集。 - 两个开集的交集是开集。 - 任意多个开集的并集是开集。

在上述每个例子中，结构的元素都属于一个集合，即 载体集 ，有时它可代表整个结构。例如，当我们说“设 \(G\) 是一个群”，然后说“设 \(g \in G\)”，这里 \(G\) 既代表结构本身，也代表其载体。并非每个代数结构都以这种方式与单个载体集相关联。例如， 二部图 涉及两个集合之间的关系，伽罗瓦连接 也是如此。 范畴 也涉及两个感兴趣的集合，通常称为 对象 和 态射 。 这些示例表明了证明助手为了支持代数推理需要完成的一些工作。 首先，它需要识别结构的具体实例。 数系 \(\mathbb{Z}\)、\(\mathbb{Q}\) 和 \(\mathbb{R}\) 都是有序环， 我们应当能够在这些实例中的任何一个上应用关于有序环的一般定理。 有时，一个具体的集合可能以不止一种方式成为某个结构的实例。 例如，除了构成实分析基础的通常的 \(\mathbb{R}\) 上的拓扑外， 我们还可以考虑 \(\mathbb{R}\) 上的 离散 拓扑，在这种拓扑中，每个集合都是开集。 其次，证明助手需要支持结构上的通用符号表示。在 Lean 中，符号 * 用于所有常见数系中的乘法，也用于泛指群和环中的乘法。当我们使用像 f x * y 这样的表达式时，Lean 必须利用关于 f 、 x 和 y 的类型信息来确定我们所指的乘法运算。 第三，它需要处理这样一个事实，即结构可以通过多种方式从其他结构继承定义、定理和符号。有些结构通过添加更多公理来扩展其他结构。交换环仍然是环，因此在环中有意义的任何定义在交换环中也有意义，任何在环中成立的定理在交换环中也成立。有些结构通过添加更多数据来扩展其他结构。例如，任何环的加法部分都是加法群。环结构添加了乘法和单位元，以及管理它们并将其与加法部分相关联的公理。有时我们可以用另一种结构来定义一种结构。任何度量空间都有一个与之相关的标准拓扑，即“度量空间拓扑”，并且任何线性序都可以关联多种拓扑。 最后，重要的是要记住，数学使我们能够像使用函数和运算来定义数字一样，使用函数和运算来定义结构。群的乘积和幂次仍然是群。对于每个 \(n\)，模 \(n\) 的整数构成一个环，对于每个 \(k > 0\)，该环中系数的 \(k \times k\) 多项式矩阵再次构成一个环。因此，我们能够像计算其元素一样轻松地计算结构。这意味着代数结构在数学中有着双重身份，既是对象集合的容器，又是独立的对象。证明助手必须适应这种双重角色。 在处理具有代数结构相关联的类型的元素时，证明助手需要识别该结构并找到相关的定义、定理和符号。这一切听起来似乎工作量很大，确实如此。但 Lean 使用一小部分基本机制来完成这些任务。本节的目标是解释这些机制并展示如何使用它们。 第一个要素几乎无需提及，因为它太过显而易见：从形式上讲，代数结构是 Section 6.1 中所定义的那种结构。代数结构是对满足某些公理假设的数据束的规范，我们在 Section 6.1 中看到，这正是 structure 命令所设计要容纳的内容。这简直是天作之合！ 给定一种数据类型 α ，我们可以按如下方式定义 α 上的群结构。

structure Group₁ (α : Type*) where
  mul : α → α → α
  one : α
  inv : α → α
  mul_assoc : ∀ x y z : α, mul (mul x y) z = mul x (mul y z)
  mul_one : ∀ x : α, mul x one = x
  one_mul : ∀ x : α, mul one x = x
  inv_mul_cancel : ∀ x : α, mul (inv x) x = one

请注意，在 group₁ 的定义中，类型 α 是一个 参数 。因此，您应当将对象 struc : Group₁ α 视为是在 α 上的一个群结构。我们在 Section 2.2 中看到，与 inv_mul_cancel 相对应的 mul_inv_cancel 可以从其他群公理推导出来，所以无需将其添加到定义中。

这个群的定义与 Mathlib 中的 Group 定义类似，我们选择使用 Group₁ 这个名称来区分我们的版本。如果您输入 #check Group 并点击定义，您会看到 Mathlib 版本的 Group 被定义为扩展了另一个结构；我们稍后会解释如何做到这一点。如果您输入 #print Group ，您还会看到 Mathlib 版本的 Group 具有许多额外的字段。出于稍后会解释的原因，有时在结构中添加冗余信息是有用的，这样就有额外的字段用于从核心数据定义的对象和函数。现在先别担心这个问题。请放心，我们的简化版本 Group₁ 在本质上与 Mathlib 使用的群定义相同。

有时将类型与结构捆绑在一起是有用的，Mathlib 中也包含一个与以下定义等价的 GroupCat 结构定义：

structure Group₁Cat where
  α : Type*
  str : Group₁ α

Mathlib 版本位于 Mathlib.Algebra.Category.GroupCat.Basic 中，如果您在示例文件开头的导入中添加此内容，可以使用 #check 查看它。

出于下文会更清楚说明的原因，通常更有用的做法是将类型 α 与结构 Group α 分开。我们将这两个对象一起称为 部分捆绑结构 ，因为其表示将大部分但并非全部的组件组合成一个结构。在 Mathlib 中，当某个类型被用作群的载体类型时，通常会使用大写罗马字母如 G 来表示该类型。

让我们构建一个群，也就是说，一个 Group₁ 类型的元素。对于任意的类型α和β，Mathlib 定义了类型 Equiv α β ，表示α和β之间的 等价关系 。 Mathlib 还为这个类型定义了具有提示性的记号 α ≃ β 。 一个元素 f : α ≃ β 是α和β之间的双射，由四个部分表示： 从α到β的函数 f.toFun ， 从β到α的逆函数 f.invFun ， 以及两个指定这些函数确实是彼此逆函数的性质。

variable (α β γ : Type*)
variable (f : α ≃ β) (g : β ≃ γ)

#check Equiv α β
#check (f.toFun : α → β)
#check (f.invFun : β → α)
#check (f.right_inv : ∀ x : β, f (f.invFun x) = x)
#check (f.left_inv : ∀ x : α, f.invFun (f x) = x)
#check (Equiv.refl α : α ≃ α)
#check (f.symm : β ≃ α)
#check (f.trans g : α ≃ γ)

请注意最后三个构造的创造性命名。我们将恒等函数 Equiv.refl 、逆运算 Equiv.symm 和复合运算 Equiv.trans 视为明确的证据，表明处于双射对应关系的性质是一个等价关系。

还要注意， f.trans g 要求将前向函数按相反的顺序组合。Mathlib 已经声明了从 Equiv α β 到函数类型 α → β 的一个 强制转换 ，因此我们可以省略书写 .toFun ，让 Lean 为我们插入。

example (x : α) : (f.trans g).toFun x = g.toFun (f.toFun x) :=
  rfl

example (x : α) : (f.trans g) x = g (f x) :=
  rfl

example : (f.trans g : α → γ) = g ∘ f :=
  rfl

Mathlib 还定义了 α 与其自身的等价关系类型 perm α 。

example (α : Type*) : Equiv.Perm α = (α ≃ α) :=
  rfl

显然， Equiv.Perm α 在等价关系的组合下形成了一个群。我们将乘法定义为 mul f g 等于 g.trans f ，其前向函数为 f ∘ g 。换句话说，乘法就是我们通常所认为的双射的组合。这里我们定义这个群：

def permGroup {α : Type*} : Group₁ (Equiv.Perm α)
    where
  mul f g := Equiv.trans g f
  one := Equiv.refl α
  inv := Equiv.symm
  mul_assoc f g h := (Equiv.trans_assoc _ _ _).symm
  one_mul := Equiv.trans_refl
  mul_one := Equiv.refl_trans
  inv_mul_cancel := Equiv.self_trans_symm

实际上，Mathlib 在文件 GroupTheory.Perm.Basic 中为 Equiv.Perm α 精确地定义了这个 Group 结构。 和往常一样，您可以将鼠标悬停在 permGroup 定义中使用的定理上以查看其陈述，并且可以跳转到原始文件中的定义以了解它们是如何实现的。

在普通数学中，我们通常认为符号表示与结构是相互独立的。 例如，我们可以考虑群 \((G_1, \cdot, 1, \cdot^{-1})\)、\((G_2， \circ， e， i(\cdot))\) 和 \((G_3， +， 0, -)\)。 在第一种情况下，我们将二元运算写为 \(\cdot\)，单位元为 \(1\)，逆函数为 \(x \mapsto x^{-1}\)。 在第二种和第三种情况下，我们使用所示的符号替代形式。 然而，在 Lean 中对群的概念进行形式化时，符号表示与结构的联系更为紧密。 在 Lean 中，任何 Group 的组成部分都命名为 mul 、 one 和 inv ，稍后我们将看到乘法符号是如何与它们关联的。 如果我们想使用加法符号，则使用同构结构 AddGroup （加法群的基础结构）。其组成部分命名为 add 、 zero 和 neg ，相关符号也是您所期望的那样。

回想一下我们在 Section 6.1 中定义的类型 Point ，以及在那里定义的加法函数。这些定义在本节附带的示例文件中有所重现。作为练习，请定义一个类似于我们上面定义的 Group₁ 结构的 AddGroup₁ 结构，但使用刚刚描述的加法命名方案。在 Point 数据类型上定义否定和零，并在 Point 上定义 AddGroup₁ 结构。

structure AddGroup₁ (α : Type*) where
  (add : α → α → α)
  -- fill in the rest
@[ext]
structure Point where
  x : ℝ
  y : ℝ
  z : ℝ

namespace Point

def add (a b : Point) : Point :=
  ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩

def neg (a : Point) : Point := sorry

def zero : Point := sorry

def addGroupPoint : AddGroup₁ Point := sorry

end Point

我们正在取得进展。 现在我们知道了如何在 Lean 中定义代数结构，也知道如何定义这些结构的实例。 但我们还希望将符号与结构相关联，以便在每个实例中使用它。 此外，我们希望安排好，以便可以在结构上定义一个操作，并在任何特定实例中使用它，还希望安排好，以便可以在结构上证明一个定理，并在任何实例中使用它。

实际上，Mathlib 已经设置好使用通用群表示法、定义和定理来处理 Equiv.Perm α 。

variable {α : Type*} (f g : Equiv.Perm α) (n : ℕ)

#check f * g
#check mul_assoc f g g⁻¹

-- 群幂，定义适用于任何群
#check g ^ n

example : f * g * g⁻¹ = f := by rw [mul_assoc, mul_inv_cancel, mul_one]

example : f * g * g⁻¹ = f :=
  mul_inv_cancel_right f g

example {α : Type*} (f g : Equiv.Perm α) : g.symm.trans (g.trans f) = f :=
  mul_inv_cancel_right f g

您可以检查一下，对于上面要求您定义的 Point 上的加法群结构，情况并非如此。 我们现在要做的就是理解幕后发生的神奇操作，以便让 Equiv.Perm α 的示例能够像预期那样运行。

问题在于，Lean 需要能够根据我们输入的表达式中所包含的信息来 找到 相关的符号表示和隐含的群结构。同样地，当我们输入 x + y 且表达式 x 和 y 的类型为 ℝ 时，Lean 需要将 + 符号解释为实数上的相关加法函数。它还必须识别类型 ℝ 是交换环的一个实例，这样所有关于交换环的定义和定理才能被使用。再举个例子，连续性在 Lean 中是相对于任意两个拓扑空间来定义的。当我们有 f ： ℝ → ℂ 并输入 Continuous f 时，Lean 必须找到 ℝ 和 ℂ 上的相关拓扑。

这种魔力是通过三者的结合实现的。

1. 逻辑 。在任何群组中都应如此解释的定义，其参数应包含群组的类型和群组结构。同样，关于任意群组元素的定理，其开头应包含对群组类型和群组结构的全称量词。

2. 隐式参数 。类型和结构的参数通常被隐式省略，这样我们就不必书写它们，也不必在 Lean 的信息窗口中看到它们。Lean 会默默地为我们补充这些信息。

3. 类型类推断 。也称为 类推断 ，这是一种简单但强大的机制，使我们能够为 Lean 注册信息以供日后使用。当 Lean 被要求为定义、定理或符号填写隐式参数时，它可以利用已注册的信息。

而注释 (grp : Group G) 告诉 Lean 它应该期望明确给出该参数，注释 {grp : Group G} 告诉 Lean 它应该尝试从表达式中的上下文线索中推断出来，注释 [grp ： Group G] 则告诉 Lean 应该使用类型类推断来合成相应的参数。由于使用此类参数的全部意义在于我们通常无需明确引用它们，Lean 允许我们写成 [Group G] 并将名称匿名化。您可能已经注意到，Lean 会选择诸如 _inst_1 这样的名称。自动地。 当我们使用带有 variables 命令的匿名方括号注释时，只要变量仍在作用域内，Lean 就会自动为提及 G 的任何定义或定理添加参数 [Group G] 。

我们如何注册 Lean 进行搜索所需的信息？ 回到我们的群示例，我们只需做两个改动。 首先，我们不用 structure 命令来定义群结构，而是使用关键字 class 来表明它是一个类推断的候选对象。 其次，我们不用 def 来定义特定实例，而是使用关键字 instance 来给Lean注册特定实例。与类变量的名称一样，我们也可以让实例定义的名称保持匿名，因为通常我们希望 Lean 能够找到它并加以利用，而不必让我们操心其中的细节。

class Group₂ (α : Type*) where
  mul : α → α → α
  one : α
  inv : α → α
  mul_assoc : ∀ x y z : α, mul (mul x y) z = mul x (mul y z)
  mul_one : ∀ x : α, mul x one = x
  one_mul : ∀ x : α, mul one x = x
  inv_mul_cancel : ∀ x : α, mul (inv x) x = one

instance {α : Type*} : Group₂ (Equiv.Perm α) where
  mul f g := Equiv.trans g f
  one := Equiv.refl α
  inv := Equiv.symm
  mul_assoc f g h := (Equiv.trans_assoc _ _ _).symm
  one_mul := Equiv.trans_refl
  mul_one := Equiv.refl_trans
  inv_mul_cancel := Equiv.self_trans_symm

以下说明了它们的用法。

 #check Group₂.mul

 def mySquare {α : Type*} [Group₂ α] (x : α) :=
   Group₂.mul x x

 #check mySquare

 section
 variable {β : Type*} (f g : Equiv.Perm β)

 example : Group₂.mul f g = g.trans f :=
   rfl

 example : mySquare f = f.trans f :=
   rfl

 end

``#check`` 命令显示， ``Group₂.mul`` 有一个隐式参数 ``[Group₂ α]`` ，我们期望它通过类推断找到，其中 ``α`` 是 ``Group₂.mul`` 参数的类型。换句话说， ``{α ： Type*}`` 是群元素类型的隐式参数，而 ``[Group₂ α]`` 是 ``α`` 上的群结构的隐式参数。同样地，当我们为 ``Group₂`` 定义一个通用的平方函数 ``my_square`` 时，我们使用隐式参数 ``{α ： Type*}`` 来表示元素的类型，使用隐式参数 ``[Group₂ α]`` 来表示 ``α`` 上的 ``Group₂`` 结构。

在第一个示例中，当我们编写 Group₂.mul f g 时，f 和 g 的类型告诉 Lean 在 Group₂.mul 的参数 α 中必须实例化为 Equiv.Perm β 。这意味着 Lean 必须找到 Group₂ (Equiv.Perm β) 中的一个元素。前面的 instance 声明确切地告诉 Lean 如何做到这一点。问题解决了！

这种用于注册信息以便 Lean 在需要时能够找到它的简单机制非常有用。 这里有一个例子。 在 Lean 的基础中，数据类型“α”可能是空的。 然而，在许多应用中，知道一个类型至少有一个元素是有用的。 例如，函数 List.headI ，它返回列表的第一个元素，可以在列表为空时返回默认值。 为了实现这一点，Lean 库定义了一个类 Inhabited α ，它所做的只是存储一个默认值。 我们可以证明 Point 类型是其一个实例：

instance : Inhabited Point where default := ⟨0, 0, 0⟩

#check (default : Point)

example : ([] : List Point).headI = default :=
  rfl

类推断机制也用于泛型表示法。 表达式 x + y 是 Add.add x y 的缩写，你猜对了————其中 Add α 是一个存储 α 上二元函数的类。 书写 x + y 会告诉 Lean 查找已注册的 [Add.add α] 实例并使用相应的函数。 下面，我们为 Point 注册加法函数。

instance : Add Point where add := Point.add

section
variable (x y : Point)

#check x + y

example : x + y = Point.add x y :=
  rfl

end

通过这种方式，我们也可以将符号 + 用于其他类型的二元运算。 但我们还能做得更好。我们已经看到， * 可以用于任何群， + 可以用于任何加法群，而两者都可以用于任何环。 当我们在 Lean 中定义一个新的环实例时，我们不必为该实例定义 + 和 * ，因为 Lean 知道这些运算符对于每个环都是已定义的。 我们可以使用这种方法为我们的 Group₂ 类指定符号表示法：

instance hasMulGroup₂ {α : Type*} [Group₂ α] : Mul α :=
  ⟨Group₂.mul⟩

instance hasOneGroup₂ {α : Type*} [Group₂ α] : One α :=
  ⟨Group₂.one⟩

instance hasInvGroup₂ {α : Type*} [Group₂ α] : Inv α :=
  ⟨Group₂.inv⟩

section
variable {α : Type*} (f g : Equiv.Perm α)

#check f * 1 * g⁻¹

def foo : f * 1 * g⁻¹ = g.symm.trans ((Equiv.refl α).trans f) :=
  rfl

end

在这种情况下，我们必须为实例提供名称，因为Lean 很难想出好的默认值。 使这种方法奏效的是 Lean 进行递归搜索的能力。 根据我们声明的实例，Lean 可以通过找到 Group₂ (Equiv.Perm α) 的实例来找到 Mul (Equiv.Perm α) 的实例，而它能够找到 Group₂ (Equiv.Perm α) 的实例是因为我们已经提供了一个。 Lean 能够找到这两个事实并将它们串联起来。

我们刚刚给出的例子是危险的，因为 Lean 的库中也有一个 Group (Equiv.Perm α) 的实例，并且乘法在任何群上都有定义。所以，找到的是哪个实例是不明确的。实际上，除非您明确指定不同的优先级，否则 Lean 会倾向于更近的声明。此外，还有另一种方法可以告诉 Lean 一个结构是另一个结构的实例，即使用 extends 关键字。这就是 Mathlib 指定例如每个交换环都是环的方式。 您可以在 Section 7 以及 Theorem Proving in Lean 中的 关于类推断的章节 中找到更多信息。

一般来说，对于已经定义了记号的代数结构的实例，指定值为 * 是一个不好的主意。 在 Lean 中重新定义 Group 的概念是一个人为的例子。 然而，在这种情况下，群记号的两种解释都以相同的方式展开为 Equiv.trans 、 Equiv.refl 和 Equiv.symm 。

作为一项类似的构造性练习，仿照 Group₂ 定义一个名为 AddGroup₂ 的类。使用 Add 、 Neg 和 Zero 类为任何 AddGroup₂ 定义加法、取反和零的常规表示法。然后证明 Point 是 AddGroup₂ 的一个实例。尝试一下并确保加法群的表示法对 Point 的元素有效。

class AddGroup₂ (α : Type*) where
  add : α → α → α
  -- 请将剩余部分填写完整

我们上面已经为 Point 声明了实例 Add 、 Neg 和 Zero ，这并不是什么大问题。再次强调，这两种符号合成方式应该得出相同的答案。 类推断是微妙的，在使用时必须小心谨慎，因为它配置了无形中控制我们所输入表达式解释的自动化机制。然而，如果明智地使用，类推断则是一个强大的工具。正是它使得在 Lean 中进行代数推理成为可能。

6.3. 构建高斯整数

现在我们将通过构建一个重要的数学对象—— 高斯整数 ，来说明在 Lean 中代数层次结构的使用，并证明它是欧几里得域。换句话说，按照我们一直在使用的术语，我们将定义高斯整数，并证明它们是欧几里得域结构的一个实例。

在普通的数学术语中，高斯整数集 \(\Bbb{Z}[i]\) 是复数集 \(\{ a + b i \mid a, b \in \Bbb{Z}\}\)。但我们的目标不是将其定义为复数集的一个子集，而是将其定义为一种独立的数据类型。为此，我们将高斯整数表示为一对整数，分别视为其 实部 和 虚部 。

@[ext]
structure GaussInt where
  re : ℤ
  im : ℤ

我们首先证明高斯整数具有环的结构，其中 0 定义为 ⟨0, 0⟩ ， 1 定义为 ⟨1, 0⟩ ，加法按点定义。为了确定乘法的定义，记住我们希望由 ⟨0, 1⟩ 表示的元素 \(i\) 是 \(-1\) 的平方根。因此，我们希望

\[\begin{split}(a + bi) (c + di) & = ac + bci + adi + bd i^2 \\ & = (ac - bd) + (bc + ad)i.\end{split}\]

这解释了下面对 Mul 的定义。

instance : Zero GaussInt :=
  ⟨⟨0, 0⟩⟩

instance : One GaussInt :=
  ⟨⟨1, 0⟩⟩

instance : Add GaussInt :=
  ⟨fun x y ↦ ⟨x.re + y.re, x.im + y.im⟩⟩

instance : Neg GaussInt :=
  ⟨fun x ↦ ⟨-x.re, -x.im⟩⟩

instance : Mul GaussInt :=
  ⟨fun x y ↦ ⟨x.re * y.re - x.im * y.im, x.re * y.im + x.im * y.re⟩⟩

正如在 Section 6.1 中所提到的，将与某种数据类型相关的所有定义放在同名的命名空间中是个好主意。因此，在与本章相关的 Lean 文件中，这些定义是在 GaussInt 命名空间中进行的。 请注意，这里我们直接定义了符号 0 、 1 、 + 、 - 和 * 的解释，而不是将它们命名为 GaussInt.zero 之类的名称并将其分配给这些名称。通常，为定义提供一个明确的名称很有用，例如，用于与 simp 和 rewrite 一起使用。

theorem zero_def : (0 : GaussInt) = ⟨0, 0⟩ :=
  rfl

theorem one_def : (1 : GaussInt) = ⟨1, 0⟩ :=
  rfl

theorem add_def (x y : GaussInt) : x + y = ⟨x.re + y.re, x.im + y.im⟩ :=
  rfl

theorem neg_def (x : GaussInt) : -x = ⟨-x.re, -x.im⟩ :=
  rfl

theorem mul_def (x y : GaussInt) :
    x * y = ⟨x.re * y.re - x.im * y.im, x.re * y.im + x.im * y.re⟩ :=
  rfl

对计算实部和虚部的规则进行命名，并将其声明给简化器，这也是很有用的。

@[simp]
theorem zero_re : (0 : GaussInt).re = 0 :=
  rfl

@[simp]
theorem zero_im : (0 : GaussInt).im = 0 :=
  rfl

@[simp]
theorem one_re : (1 : GaussInt).re = 1 :=
  rfl

@[simp]
theorem one_im : (1 : GaussInt).im = 0 :=
  rfl

@[simp]
theorem add_re (x y : GaussInt) : (x + y).re = x.re + y.re :=
  rfl

@[simp]
theorem add_im (x y : GaussInt) : (x + y).im = x.im + y.im :=
  rfl

@[simp]
theorem neg_re (x : GaussInt) : (-x).re = -x.re :=
  rfl

@[simp]
theorem neg_im (x : GaussInt) : (-x).im = -x.im :=
  rfl

@[simp]
theorem mul_re (x y : GaussInt) : (x * y).re = x.re * y.re - x.im * y.im :=
  rfl

@[simp]
theorem mul_im (x y : GaussInt) : (x * y).im = x.re * y.im + x.im * y.re :=
  rfl

现在令人惊讶地容易证明高斯整数是交换环的一个实例。我们正在很好地利用结构概念。每个特定的高斯整数都是 GaussInt 结构的一个实例，而 GaussInt 类型本身，连同相关操作，则是 CommRing 结构的一个实例。 CommRing 结构反过来又扩展了符号结构 Zero 、 One 、 Add 、 Neg 和 Mul 。

如果您输入 instance : CommRing GaussInt := _ ，点击 VS Code 中出现的灯泡图标，然后让 Lean 自动填充结构定义的框架，您会看到大量的条目。然而，跳转到结构的定义会发现，其中许多字段都有默认定义，Lean 会自动为您填充。下面的定义中列出了关键的几个。

如果您输入 instance : CommRing GaussInt := _ ，点击 VS Code 中出现的灯泡图标，然后让 Lean 填充结构定义的骨架，您会看到令人望而生畏的条目数量。然而，跳转到该结构的定义后会发现，许多字段都有默认定义，Lean 会自动为您填充。以下定义中展示的是其中关键的部分。 nsmul 和 zsmul 是一个特殊情况，暂时可以忽略，它们将在下一章中解释。在每种情况下，相关的恒等式都是通过展开定义、使用 ext 策略将恒等式简化为其实部和虚部、进行简化，并在必要时在整数中执行相关的环计算来证明的。需要注意的是，我们本可以轻松避免重复所有这些代码，但这并不是当前讨论的主题。

instance instCommRing : CommRing GaussInt where
  zero := 0
  one := 1
  add := (· + ·)
  neg x := -x
  mul := (· * ·)
  nsmul := nsmulRec
  zsmul := zsmulRec
  add_assoc := by
    intros
    ext <;> simp <;> ring
  zero_add := by
    intro
    ext <;> simp
  add_zero := by
    intro
    ext <;> simp
  neg_add_cancel := by
    intro
    ext <;> simp
  add_comm := by
    intros
    ext <;> simp <;> ring
  mul_assoc := by
    intros
    ext <;> simp <;> ring
  one_mul := by
    intro
    ext <;> simp
  mul_one := by
    intro
    ext <;> simp
  left_distrib := by
    intros
    ext <;> simp <;> ring
  right_distrib := by
    intros
    ext <;> simp <;> ring
  mul_comm := by
    intros
    ext <;> simp <;> ring
  zero_mul := by
    intros
    ext <;> simp
  mul_zero := by
    intros
    ext <;> simp

Lean 的库将具有至少两个不同元素的类型定义为 非平凡 类型。在环的上下文中，这等同于说零不等于一。由于一些常见的定理依赖于这一事实，我们不妨现在就证明它。

instance : Nontrivial GaussInt := by
  use 0, 1
  rw [Ne, GaussInt.ext_iff]
  simp

我们现在将证明高斯整数具有一个重要的额外性质。一个 欧几里得整环（Euclidean domain） 是一个环 \(R\)，配备了一个范数函数 \(N : R \to \mathbb{N}\)，满足以下两个性质：

-对于 \(R\) 中的任意 \(a\) 和非零 \(b\)，存在 \(R\) 中的 \(q\) 和 \(r\)，使得 \(a = bq + r\)，并且要么 \(r = 0\)，要么 \(N(r) < N(b)\)。 -对于任意 \(a\) 和非零 \(b\)，\(N(a) \le N(ab)\)。 整数环 \(\Bbb{Z}\) 与范数 \(N(a) = |a|\) 是欧几里得整环的一个典型例子。在这种情况下，我们可以将 \(q\) 取为 \(a\) 除以 \(b\) 的整数除法结果，并将 \(r\) 取为余数。这些函数在 Lean 中定义，并满足以下性质：

example (a b : ℤ) : a = b * (a / b) + a % b :=
  Eq.symm (Int.ediv_add_emod a b)

example (a b : ℤ) : b ≠ 0 → 0 ≤ a % b :=
  Int.emod_nonneg a

example (a b : ℤ) : b ≠ 0 → a % b < |b| :=
  Int.emod_lt a

在任意环中，若一个元素 \(a\) 能整除 1，则称其为 单位元 。若一个非零元素 \(a\) 不能写成 \(a = bc\) 的形式，其中 \(b\) 和 \(c\) 均不是单位元，则称其为 不可约元 。在整数环中，每个不可约元 \(a\) 都是 素元 ，也就是说，每当 \(a\) 能整除乘积 \(bc\) 时，它就能整除 \(b\) 或 \(c\) 。但是 在其他环中，这一性质可能会失效。在环 \(\Bbb{Z}[\sqrt{-5}]\) 中，我们有

\[6 = 2 \cdot 3 = (1 + \sqrt{-5})(1 - \sqrt{-5}),\]

并且元素 \(2\) 、 \(3\) 、 \(1 + \sqrt{-5}\) 以及 \(1 - \sqrt{-5}\) 都是不可约的，但它们不是素元。例如， \(2\) 能整除乘积 \((1 + \sqrt{-5})(1 - \sqrt{-5})\) ，但它不能整除这两个因数中的任何一个。特别地，我们不再具有唯一分解性：数字 \(6\) 可以用不止一种方式分解为不可约元素。

相比之下，每个欧几里得域都是唯一分解域，这意味着每个不可约元素都是素元。 欧几里得域的公理意味着可以将任何非零元素表示为不可约元素的有限乘积。它们还意味着可以使用欧几里得算法找到任意两个非零元素 a 和 b 的最大公约数，即能被任何其他公因数整除的元素。这反过来又意味着，除了乘以单位元素外，分解为不可约元素是唯一的。

我们现在证明高斯整数是一个欧几里得域，其范数定义为 \(N(a + bi) = (a + bi)(a - bi) = a^2 + b^2\) 。高斯整数 \(a - bi\) 被称为 \(a + bi\) 的共轭。不难验证，对于任何复数 \(x\) 和 \(y\) ，我们都有 \(N(xy) = N(x)N(y)\) 。

要证明这个范数的定义能使高斯整数构成欧几里得域，只有第一个性质具有挑战性。假设我们想写成 \(a + bi = (c + di) q + r\) 的形式，其中 \(q\) 和 \(r\) 是合适的数。将 \(a + bi\) 和 \(c + di\) 视为复数，进行除法运算。

\[\frac{a + bi}{c + di} = \frac{(a + bi)(c - di)}{(c + di)(c-di)} = \frac{ac + bd}{c^2 + d^2} + \frac{bc -ad}{c^2+d^2} i.\]

实部和虚部可能不是整数，但我们可将其四舍五入到最接近的整数 \(u\) 和 \(v\) 。然后我们可以将右边表示为 \((u + vi) + (u' + v'i)\) ，其中 \(u' + v'i\) 是剩余的部分。请注意，我们有 \(|u'| \le 1/2\) 和 \(|v'| \le 1/2\) ，因此

\[N(u' + v' i) = (u')^2 + (v')^2 \le 1/4 + 1/4 \le 1/2.\]

乘以 \(c + di\)，我们有

\[a + bi = (c + di) (u + vi) + (c + di) (u' + v'i).\]

Setting \(q = u + vi\) and \(r = (c + di) (u' + v'i)\), we have \(a + bi = (c + di) q + r\), and we only need to bound \(N(r)\): 设 \(q = u + vi\) 以及 \(r = (c + di) (u' + v'i)\) ，则有 \(a + bi = (c + di) q + r\) ，我们只需对 \(N(r)\) 进行限制：

\[N(r) = N(c + di)N(u' + v'i) \le N(c + di) \cdot 1/2 < N(c + di).\]

我们刚刚进行的论证需要将高斯整数视为复数的一个子集。因此，在 Lean 中对其进行形式化的一种选择是将高斯整数嵌入到复数中，将整数嵌入到高斯整数中，定义从实数到整数的舍入函数，并且要非常小心地在这些数系之间进行适当的转换。 实际上，这正是 Mathlib 中所采用的方法，其中高斯整数本身是作为 二次整数 环的一个特例来构造的。 请参阅文件 GaussianInt.lean.

在这里，我们将进行一个完全在整数范围内进行的论证。 这说明了在将数学形式化时人们通常面临的一种选择。 当一个论证需要库中尚未包含的概念或工具时，人们有两个选择：要么形式化所需的这些概念或工具，要么调整论证以利用已有的概念和工具。 从长远来看，当结果可以在其他情境中使用时，第一个选择通常是对时间的良好投资。 然而，从实际角度来看，有时寻找一个更基础的证明会更有效。

整数的常规商余定理指出，对于任意整数 \(a\) 和非零整数 \(b\)，都存在整数 \(q\) 和 \(r\) 使得 \(a = b q + r\) 且 \(0 \le r < b\)。这里我们将使用以下变体，即存在整数 \(q'\) 和 \(r'\) 使得 \(a = b q' + r'\) 且 \(|r'| \le b/2\)。您可以验证，如果第一个陈述中的 \(r\) 满足 \(r \le b/2\)，则可以取 \(q' = q\) 和 \(r' = r\)，否则可以取 \(q' = q + 1\) 和 \(r' = r - b\)。我们感谢 Heather Macbeth 提出以下更优雅的方法，该方法避免了按情况定义。我们只需在除法前将 b / 2 加到 a 上，然后从余数中减去它。

def div' (a b : ℤ) :=
  (a + b / 2) / b

def mod' (a b : ℤ) :=
  (a + b / 2) % b - b / 2

theorem div'_add_mod' (a b : ℤ) : b * div' a b + mod' a b = a := by
  rw [div', mod']
  linarith [Int.ediv_add_emod (a + b / 2) b]

theorem abs_mod'_le (a b : ℤ) (h : 0 < b) : |mod' a b| ≤ b / 2 := by
  rw [mod', abs_le]
  constructor
  · linarith [Int.emod_nonneg (a + b / 2) h.ne']
  have := Int.emod_lt_of_pos (a + b / 2) h
  have := Int.ediv_add_emod b 2
  have := Int.emod_lt_of_pos b zero_lt_two
  revert this; intro this -- 待修复，这应该是不必要的
  linarith

请注意我们老朋友 linarith 的使用。我们还需要用 div' 来表示 mod' 。

theorem mod'_eq (a b : ℤ) : mod' a b = a - b * div' a b := by linarith [div'_add_mod' a b]

我们将使用这样一个事实，即 \(x^2 + y^2\) 等于零当且仅当 \(x\) 和 \(y\) 都为零。作为练习，我们要求您证明在任何有序环中都成立。

theorem sq_add_sq_eq_zero {α : Type*} [LinearOrderedRing α] (x y : α) :
    x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0 := by
  sorry

我们将本节中剩余的所有定义和定理都放在 GaussInt 命名空间中。 首先，我们定义 norm 函数，并请您证明其部分性质。 这些证明都很简短。

def norm (x : GaussInt) :=
  x.re ^ 2 + x.im ^ 2

@[simp]
theorem norm_nonneg (x : GaussInt) : 0 ≤ norm x := by
  sorry
theorem norm_eq_zero (x : GaussInt) : norm x = 0 ↔ x = 0 := by
  sorry
theorem norm_pos (x : GaussInt) : 0 < norm x ↔ x ≠ 0 := by
  sorry
theorem norm_mul (x y : GaussInt) : norm (x * y) = norm x * norm y := by
  sorry

接下来我们定义共轭函数：

def conj (x : GaussInt) : GaussInt :=
  ⟨x.re, -x.im⟩

@[simp]
theorem conj_re (x : GaussInt) : (conj x).re = x.re :=
  rfl

@[simp]
theorem conj_im (x : GaussInt) : (conj x).im = -x.im :=
  rfl

theorem norm_conj (x : GaussInt) : norm (conj x) = norm x := by simp [norm]

最后，我们为高斯整数定义除法运算，记作 x / y ，将复数商四舍五入到最近的高斯整数。为此我们使用自定义的 Int.div' 。 正如我们上面计算的那样，如果 x 是 \(a + bi\)，而 y 是 \(c + di\)，那么 x / y 的实部和虚部分别是如下式子最近的整数

\[\frac{ac + bd}{c^2 + d^2} \quad \text{和} \quad \frac{bc -ad}{c^2+d^2},\]

这里分子是 \((a + bi) (c - di)\) 的实部和虚部，而分母都等于 \(c + di\) 的范数。

instance : Div GaussInt :=
  ⟨fun x y ↦ ⟨Int.div' (x * conj y).re (norm y), Int.div' (x * conj y).im (norm y)⟩⟩

定义了 x / y 之后，我们定义 x % y 为余数，即 x - (x / y) * y 。同样地，我们将这些定义记录在定理 div_def 和 mod_def 中，以便使用 simp 和 rewrite 。

instance : Mod GaussInt :=
  ⟨fun x y ↦ x - y * (x / y)⟩

theorem div_def (x y : GaussInt) :
    x / y = ⟨Int.div' (x * conj y).re (norm y), Int.div' (x * conj y).im (norm y)⟩ :=
  rfl

theorem mod_def (x y : GaussInt) : x % y = x - y * (x / y) :=
  rfl

这些定义立即得出对于每个 x 和 y 都有 x = y * (x / y) + x % y ，所以我们需要做的就是证明当 y 不为零时， x % y 的范数小于 y 的范数。

我们刚刚将 x / y 的实部和虚部分别定义为 div' (x * conj y).re (norm y) and div' (x * conj y).im (norm y) 。 计算得出，我们有

(x % y) * conj y = (x - x / y * y) * conj y = x * conj y - x / y * (y * conj y)

右侧实部和虚部恰好为 mod' (x * conj y).re (norm y) 和 mod' (x * conj y).im (norm y) 。 根据 div' 和 mod' 的性质，可以保证它们都小于或等于 norm y / 2 。 因此我们有

norm ((x % y) * conj y) ≤ (norm y / 2)^2 + (norm y / 2)^2 ≤ (norm y / 2) * norm y .

另一方面，我们有

norm ((x % y) * conj y) = norm (x % y) * norm (conj y) = norm (x % y) * norm y .

两边同时除以 norm y ，我们得到 norm（x % y）≤（norm y）/ 2 < norm y ，如所要求的那样。

这个杂乱的计算将在接下来的证明中进行。我们鼓励您仔细查看细节，看看能否找到更简洁的论证方法。

theorem norm_mod_lt (x : GaussInt) {y : GaussInt} (hy : y ≠ 0) :
    (x % y).norm < y.norm := by
  have norm_y_pos : 0 < norm y := by rwa [norm_pos]
  have H1 : x % y * conj y = ⟨Int.mod' (x * conj y).re (norm y), Int.mod' (x * conj y).im (norm y)⟩
  · ext <;> simp [Int.mod'_eq, mod_def, div_def, norm] <;> ring
  have H2 : norm (x % y) * norm y ≤ norm y / 2 * norm y
  · calc
      norm (x % y) * norm y = norm (x % y * conj y) := by simp only [norm_mul, norm_conj]
      _ = |Int.mod' (x.re * y.re + x.im * y.im) (norm y)| ^ 2
          + |Int.mod' (-(x.re * y.im) + x.im * y.re) (norm y)| ^ 2 := by simp [H1, norm, sq_abs]
      _ ≤ (y.norm / 2) ^ 2 + (y.norm / 2) ^ 2 := by gcongr <;> apply Int.abs_mod'_le _ _ norm_y_pos
      _ = norm y / 2 * (norm y / 2 * 2) := by ring
      _ ≤ norm y / 2 * norm y := by gcongr; apply Int.ediv_mul_le; norm_num
  calc norm (x % y) ≤ norm y / 2 := le_of_mul_le_mul_right H2 norm_y_pos
    _ < norm y := by
        apply Int.ediv_lt_of_lt_mul
        · norm_num
        · linarith

我们即将完成。我们的 norm 函数将高斯整数映射到非负整数。我们需要一个将高斯整数映射到自然数的函数，我们通过将 norm 与将整数映射到自然数的函数 Int.natAbs 组合来获得它。 接下来的两个引理中的第一个确立了将范数映射到自然数然后再映射回整数不会改变其值。 第二个引理重新表述了范数递减这一事实。

theorem coe_natAbs_norm (x : GaussInt) : (x.norm.natAbs : ℤ) = x.norm :=
  Int.natAbs_of_nonneg (norm_nonneg _)

theorem natAbs_norm_mod_lt (x y : GaussInt) (hy : y ≠ 0) :
    (x % y).norm.natAbs < y.norm.natAbs := by
  apply Int.ofNat_lt.1
  simp only [Int.natCast_natAbs, abs_of_nonneg, norm_nonneg]
  apply norm_mod_lt x hy

我们还需要确立范数函数在欧几里得域上的第二个关键性质。

theorem not_norm_mul_left_lt_norm (x : GaussInt) {y : GaussInt} (hy : y ≠ 0) :
    ¬(norm (x * y)).natAbs < (norm x).natAbs := by
  apply not_lt_of_ge
  rw [norm_mul, Int.natAbs_mul]
  apply le_mul_of_one_le_right (Nat.zero_le _)
  apply Int.ofNat_le.1
  rw [coe_natAbs_norm]
  exact Int.add_one_le_of_lt ((norm_pos _).mpr hy)

现在我们可以将其整合起来，证明高斯整数是欧几里得域的一个实例。我们使用已定义的商和余数函数。 Mathlib 中欧几里得域的定义比上面的更通用，因为它允许我们证明余数相对于任何良基度量都是递减的。 比较返回自然数的范数函数的值是只需这样一个度量的一个实例，在这种情况下，所需的性质就是定理 natAbs_norm_mod_lt 和 not_norm_mul_left_lt_norm 。

instance : EuclideanDomain GaussInt :=
  { GaussInt.instCommRing with
    quotient := (· / ·)
    remainder := (· % ·)
    quotient_mul_add_remainder_eq :=
      fun x y ↦ by simp only; rw [mod_def, add_comm] ; ring
    quotient_zero := fun x ↦ by
      simp [div_def, norm, Int.div']
      rfl
    r := (measure (Int.natAbs ∘ norm)).1
    r_wellFounded := (measure (Int.natAbs ∘ norm)).2
    remainder_lt := natAbs_norm_mod_lt
    mul_left_not_lt := not_norm_mul_left_lt_norm }

一个直接的好处是，我们现在知道，在高斯整数中，素数和不可约数的概念是一致的。

example (x : GaussInt) : Irreducible x ↔ Prime x :=
  irreducible_iff_prime