第7章结构 - 深度伴读

本章定位

本章是理解 Mathlib 的基石。你将学到：

structure 定义和字段访问

@[ext] 扩展性原理

class / instance 类型类系统

Subtype 和 Sigma 类型

完整的代数结构实例（高斯整数）

7.1 Defining Structures

核心洞见

结构体 = 命名的元组 + 可能有的约束。Lean 用结构体打包数据和属性。

基本结构体

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

@[ext] 让 Lean 自动生成扩展性定理：两个 Point 相等当且仅当所有字段相等。

#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        -- 扩展性：要证 a = b，只需证各字段相等
  repeat' assumption

的作用

没有 @[ext]，证明 a = b 会很麻烦。有了它，只需 ext 即可分解为字段相等。

三种构造方式

-- 方式1：命名字段（最清晰）
def myPoint1 : Point where
  x := 2
  y := -1
  z := 4
 
-- 方式2：匿名构造器 ⟨⟩（最简洁）
def myPoint2 : Point := ⟨2, -1, 4⟩
 
-- 方式3：显式构造函数
#check Point.mk 2 (-1) 4

也可以自定义构造函数名：

structure Point' where build ::
  x : ℝ
  y : ℝ
 
#check Point'.build 2 3

定义函数和操作

namespace Point
 
def add (a b : Point) : Point :=
  ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩
 
-- 匿名投影符号：a.add b 等价于 Point.add a b
#check myPoint1.add myPoint2
 
-- 证明性质
protected theorem add_comm (a b : Point) : add a b = add b a := by
  rw [add, add]
  ext <;> dsimp  -- <;> 对 ext 生成的所有子目标应用 dsimp
  repeat' apply add_comm
 
-- 有时等式是定义上成立的（definitional equality）
theorem add_x (a b : Point) : (a.add b).x = a.x + b.x := rfl
 
end Point

protected 关键字

protected 让定理全名保持为 Point.add_comm，即使 namespace 已 open。避免与全局 add_comm 冲突。

模式匹配定义

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₂⟩

模式匹配的缺点

rw [addAlt] 后 Goal 窗口会显示 match 语句，可读性较差。推荐使用 where 或 := ⟨...⟩ 风格。

带约束的结构体

结构体不仅可以包含数据，还可以包含 Prop 类型的约束字段：

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

这是数学中常见的”带约束的对象”。证明构造时需要提供数据和约束证明：

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]

参数化结构体

结构体可以依赖参数：

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

Fin n 是一个有 n 个元素的类型。这使得我们可以定义任意维度的标准单形。

结构体 vs 其他类型构造

-- 乘积类型（等价于 Point，但字段无名称）
def Point'' := ℝ × ℝ × ℝ
 
-- 只包含约束的结构体（无数据）
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
 
-- 用简单合取也可以，但结构体更好
 def IsLinear' (f : ℝ → ℝ) :=
   (∀ x y, f (x + y) = f x + f y) ∧ ∀ x c, f (c * x) = c * f x

为什么用结构体？

抽象表示：底层实现可改，接口不变

自定义字段名：a.x 比 a.1.1 清晰

扩展性：容易构建层级（见第8章）

Subtype 类型

Subtype 是 Lean 中将数据 + 属性打包的核心机制：

def PReal := { y : ℝ // 0 < y }
--              ↑ 数据   ↑ 属性
 
section
variable (x : PReal)
 
#check x.val        -- 数据部分：ℝ
#check x.property   -- 属性部分：0 < x.val
#check x.1          -- 同 x.val
#check x.2          -- 同 x.property
end

Subtype 语法

{ x : α // P x } 表示”满足性质 P 的 α 的元素”。注意 // 不是注释，是 Subtype 语法。

可以用 Subtype 重新定义带约束的结构：

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

但结构体版本（有命名字段）更友好。

Sigma 类型

Sigma 类型是”有序对”的推广，其中第二分量的类型依赖于第一分量：

def StdSimplex := Σ n : ℕ, StandardSimplex n
 
section
variable (s : StdSimplex)
 
#check s.fst   -- ℕ：维度
#check s.snd   -- StandardSimplex s.fst：该维度的单形
end

Sigma 类型与 Subtype 的区别：

Subtype：第二分量是 Prop（证明）
Sigma：第二分量是任意 Type（数据）

7.2 Algebraic Structures

核心洞见

代数结构 = 数据 + 公理。Lean 用 class 定义，instance 注册。

为什么要用代数结构？

原文列举了7个例子（偏序集、群、格、环、有序环、度量空间、拓扑空间）。核心需求：

泛化推理：证明一个定理，自动适用于所有实例
统一符号：+、* 在所有实例中通用
继承：交换环也是环，所有环定理对交换环成立

定义群结构

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

为什么 mul_inv_cancel 不需要？

从 inv_mul_cancel（左逆）和其他公理可以推出 mul_inv_cancel（右逆）。

构造实例：置换群

Equiv α β 表示 α 和 β 之间的双射：

variable (α β γ : Type*)
variable (f : α ≃ β) (g : β ≃ γ)
 
#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 (f.symm : β ≃ α)       -- 逆
#check (f.trans g : α ≃ γ)    -- 复合

置换群（Equiv.Perm α = α ≃ α）在复合下形成群：

def permGroup {α : Type*} : Group₁ (Equiv.Perm α) where
  mul f g := Equiv.trans g f    -- 注意：mul f g = 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

乘法方向

mul f g = g.trans f 意味着 mul f g 的 forward 函数是 f ∘ g（先 g 后 f）。这与数学中常见的群乘法方向一致。

类型类系统：class 和 instance

上面的 Group₁ 用 structure 定义，但每次使用都需要显式提供群结构参数。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
 
-- 注册实例：Lean 会自动找到
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

class 和 instance 的组合让 Lean 自动推断结构：

#check Group₂.mul  -- 有隐式的 [Group₂ α] 参数
 
def mySquare {α : Type*} [Group₂ α] (x : α) :=
  Group₂.mul x x
 
-- 使用：Lean 自动找到 Equiv.Perm β 的 Group₂ 实例
example {β : Type*} (f g : Equiv.Perm β) : Group₂.mul f g = g.trans f := rfl

Coercion：自动转换

Lean 可以自动将 Equiv α β 强制转换为函数 α → β：

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

这是通过 CoeFun 类型类实现的。类似地，你可以定义自己的 coercion：

instance : Add Point where add := Point.add
 
section
variable (x y : Point)
#check x + y        -- 现在 Point 支持 + 运算
example : x + y = Point.add x y := rfl
end

为 Group₂ 注册标准符号

instance {α : Type*} [Group₂ α] : Mul α := ⟨Group₂.mul⟩
instance {α : Type*} [Group₂ α] : One α := ⟨Group₂.one⟩
instance {α : Type*} [Group₂ α] : Inv α := ⟨Group₂.inv⟩
 
variable {α : Type*} (f g : Equiv.Perm α)
#check f * 1 * g⁻¹   -- 使用标准群符号！
 
def foo : f * 1 * g⁻¹ = g.symm.trans ((Equiv.refl α).trans f) := rfl

类型类推断的核心机制

Logic：定义和定理接受类型和结构作为参数

Implicit arguments：参数隐式，Lean 自动填充

Type class inference：Lean 递归搜索已注册的 instance

7.3 Building the Gaussian Integers

核心目标

从零构造高斯整数 ℤ[i]，证明它是欧几里得域。

高斯整数的定义

@[ext]
structure GaussInt where
  re : ℤ   -- 实部
  im : ℤ   -- 虚部

定义运算

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⟩⟩
 
-- 乘法：(a + bi)(c + di) = (ac - bd) + (bc + ad)i
instance : Mul GaussInt :=
  ⟨fun x y ↦ ⟨x.re * y.re - x.im * y.im, x.re * y.im + x.im * y.re⟩⟩

乘法定义的来源

设 i² = -1，展开 (a + bi)(c + di)：

实部：ac + bd·i² = ac - bd

虚部：ad·i + bc·i = (ad + bc)i

显式定理名

为了能用 simp 和 rw，给运算定义显式定理：

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 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 add_re (x y : GaussInt) : (x + y).re = x.re + y.re := rfl
@[simp]
theorem mul_re (x y : GaussInt) : (x * y).re = x.re * y.re - x.im * y.im := rfl
-- ... 类似定义 im 版本

的作用

标记 simp 策略会自动使用的简化规则。

证明交换环

instance instCommRing : CommRing GaussInt where
  zero := 0; one := 1; add := (· + ·); neg x := -x; mul := (· ·)
  nsmul := nsmulRec; zsmul := zsmulRec  -- 默认实现：n • x = x + x + ... + x（n 次）
  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

ext <;> simp <;> ring 模式

ext：扩展到字段级别（需证 re 和 im 分别相等）

simp：展开定义

ring：证明整数环中的恒等式

证明非平凡性

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

欧几里得域

目标：证明 ℤ[i] 是欧几里得域。

定义范数（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_mul (x y : GaussInt) : norm (x * y) = norm x * norm y := by sorry

定义共轭：

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

关键性质：N(xy) = N(x)N(y)，这来自 x·x̄ = N(x)。

除法算法

在复数中做除法：

(a+bi)/(c+di) = [(a+bi)(c-di)] / (c²+d²)
              = [(ac+bd) + (bc-ad)i] / N(c+di)

对实部和虚部分别四舍五入到最近整数，得到商 q，余数 r = x - y·q。

def div' (a b : ℤ) := (a + b / 2) / b
def mod' (a b : ℤ) := (a + b / 2) % b - b / 2
 
-- 关键性质：|mod' a b| ≤ b/2
theorem abs_mod'_le (a b : ℤ) (h : 0 < b) : |mod' a b| ≤ b / 2 := by sorry

用这些定义高斯整数的除法：

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

证明余数范数严格小于除数范数：

theorem norm_mod_lt (x : GaussInt) {y : GaussInt} (hy : y ≠ 0) :
    (x % y).norm < y.norm := by
  -- 核心不等式：N(x % y)·N(y) ≤ N(y)/2·N(y)
  -- 所以 N(x % y) ≤ N(y)/2 < N(y)
  sorry

最后注册欧几里得域实例：

instance : EuclideanDomain GaussInt :=
  { GaussInt.instCommRing with
    quotient := (· / ·)
    remainder := (· % ·)
    quotient_mul_add_remainder_eq := fun x y ↦ by rw [mod_def, add_comm]; ring
    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

本章核心概念总结

概念	用途	示例
`structure`	打包数据	`Point`, `GaussInt`
`@[ext]`	自动生成扩展性	`ext` 证明结构相等
`class`	类型类（自动推断）	`Group₂`, `CommRing`
`instance`	注册实例	`CommRing GaussInt`
`CoeFun`	函数强制转换	`f x` 对 `Equiv`
`Subtype`	数据+属性	`{x : ℝ // 0 < x}`
`Sigma`	依赖有序对	`Σ n, StandardSimplex n`
`nsmulRec`/`zsmulRec`	默认标量乘（n • x = x+…+x）	CommRing 实例中

关键学习策略

1. 证明结构相等 = ext + 字段证明

example (a b : Point) : a = b := by
  ext        -- 分解为 a.x = b.x, a.y = b.y, a.z = b.z
  all_goals  -- 对所有剩余目标
    sorry    -- 分别证明

2. 代数结构实例的构造模式

instance : MyStructure MyType where
  field1 := ...
  field2 := ...
  -- 对证明字段：
  axiom1 := by ext <;> simp <;> ring

3. 类型类推断的调试

当 Lean 找不到实例时：

-- 查看当前有哪些实例
#synth Group (Equiv.Perm α)
 
-- 显式指定（临时调试）
example : mySquare (α := Equiv.Perm β) f = f.trans f := rfl

预告：第8章会学到什么

第8章深入层级结构：

extends 的深层机制（自动解决字段重叠）
to_additive 自动生成加法版本
diamond problem 和 forgetful inheritance
DFunLike / SetLike 抽象层
子对象和商结构

自测问题

@[ext] 做了什么？为什么有用？

class 和 structure 有什么区别？

Subtype 和 Sigma 有什么区别？

高斯整数的范数为什么满足 N(xy) = N(x)N(y)？

欧几里得域的两个关键性质是什么？

伴读文档 - 第7章完

我的博客

探索

Ch7 结构 - 深度伴读

第7章结构 - 深度伴读

7.1 Defining Structures

基本结构体

三种构造方式

定义函数和操作

模式匹配定义

带约束的结构体

参数化结构体

结构体 vs 其他类型构造

Subtype 类型

Sigma 类型

7.2 Algebraic Structures

为什么要用代数结构？

定义群结构

构造实例：置换群

类型类系统：class 和 instance

Coercion：自动转换

为 Group₂ 注册标准符号

7.3 Building the Gaussian Integers

高斯整数的定义

定义运算

显式定理名

证明交换环

证明非平凡性

欧几里得域

除法算法

本章核心概念总结

关键学习策略

1. 证明结构相等 = ext + 字段证明

2. 代数结构实例的构造模式

3. 类型类推断的调试

预告：第8章会学到什么

关系图谱

目录

反向链接

我的博客

探索

Ch7 结构 - 深度伴读

第7章 结构 - 深度伴读

7.1 Defining Structures

基本结构体

三种构造方式

定义函数和操作

模式匹配定义

带约束的结构体

参数化结构体

结构体 vs 其他类型构造

Subtype 类型

Sigma 类型

7.2 Algebraic Structures

为什么要用代数结构？

定义群结构

构造实例：置换群

类型类系统：class 和 instance

Coercion：自动转换

为 Group₂ 注册标准符号

7.3 Building the Gaussian Integers

高斯整数的定义

定义运算

显式定理名

证明交换环

证明非平凡性

欧几里得域

除法算法

本章核心概念总结

关键学习策略

1. 证明结构相等 = ext + 字段证明

2. 代数结构实例的构造模式

3. 类型类推断的调试

预告：第8章会学到什么

关系图谱

目录

反向链接

第7章结构 - 深度伴读