深入 Lean 13：有限组合与数论片段

Mathlib4 提供了一套完整的有限集合与大算子（BigOperators）机制，使得组合数学和初等数论的形式化证明可以在接近数学原文的符号层面进行。Finset 表示有限集合，Fintype 约束类型的有限性，BigOperators 引入求和与连乘的紧凑记号，Nat.Prime 与 Nat.factors 覆盖自然数素数理论的基本引理。本篇在此基础上，进一步介绍 decide tactic 在有限域穷举中的作用，以及 Decidable 类型类的内部逻辑。

前置阅读：02 Term-mode 与 Tactic-mode 切换心法（tactic 基础）；04 核心 tactic 精讲（rfl、ring、omega 等基础 tactic）；05 simp 与 norm_num（自动化 tactic）。

Finset 与 Fintype

Finset 的数据表示

Finset α 是 Mathlib4 中对有限集合的主要表示，定义于 Mathlib.Data.Finset.Basic：

structure Finset (α : Type*) where
  val : Multiset α
  nodup : val.Nodup

内部存储用 Multiset（无序列表的等价类），同时附带无重复元素的证明 nodup。这使得元素属于某个 Finset 的判断 a ∈ s 是可计算的，前提是 α 上有 DecidableEq 实例。

常用构造方式：

-- 空集
#check (∅ : Finset ℕ)
-- Finset.empty : Finset ℕ

-- 单元素集合
#check ({42} : Finset ℕ)

-- 区间 {0, 1, ..., n-1}
#check Finset.range 10
-- Finset.range 10 : Finset ℕ

-- 从列表构造（自动去重）
#eval [1, 2, 2, 3].toFinset
-- {1, 2, 3}

Finset.range n 是最常用的有限自然数集合，等价于数学中的 {0, 1, …, n−1}，许多组合恒等式的证明都以它为基础。

Fintype 类型类

Fintype α 约束某个类型 α 只有有限多个居民（inhabitants）：

class Fintype (α : Type*) where
  elems : Finset α
  complete : ∀ x : α, x ∈ elems

elems 是包含 α 全部元素的 Finset，complete 保证没有遗漏。Lean 4 对大量标准类型自动推导出 Fintype 实例：

-- 布尔类型
#check (Fintype.elems : Finset Bool)
-- {false, true}

-- Fin n：类型层面的有限集合 {0, ..., n-1}
#check (Fintype.elems : Finset (Fin 5))
-- {0, 1, 2, 3, 4}

-- 乘积类型若两个因子均有 Fintype 则自动生成
example : Fintype (Fin 3 × Fin 4) := inferInstance

Finset.univ 是访问当前上下文中全域有限集合的标准写法：

#check @Finset.univ (Fin 5) _
-- Finset.univ : Finset (Fin 5)

Fintype.card α 返回 α 的元素个数，类型为 ℕ：

#eval Fintype.card (Fin 7)   -- 7
#eval Fintype.card Bool      -- 2
#eval Fintype.card (Fin 3 × Fin 4)  -- 12

DecidableEq 与成员判定

Finset 的大多数操作（∈、∪、∩、filter 等）要求元素类型具有 DecidableEq 实例，即对任意两个元素 a b : α，可以计算地判定 a = b 是否成立。

Lean 4 对 ℕ、ℤ、Bool、Fin n、String 等内置类型均提供了 DecidableEq 实例。自定义结构体若字段全部具有 DecidableEq，可用 deriving DecidableEq 自动生成：

structure Point where
  x : ℕ
  y : ℕ
  deriving DecidableEq

example : ({⟨1, 2⟩, ⟨3, 4⟩} : Finset Point).card = 2 := by decide

---

BigOperators 记号

启用记号

使用 BigOperators 记号前需要打开命名空间：

import Mathlib.Algebra.BigOperators.Basic
open BigOperators

启用后，以下两种记号可用：

∑ i in s, f i     -- 对 s : Finset α 上的所有 i 求 f i 之和
∏ i in s, f i     -- 对 s : Finset α 上的所有 i 求 f i 之积

这两个记号是宏糖，展开为 Finset.sum s f 和 Finset.prod s f。

Finset.sum 与 Finset.prod 的签名

#check @Finset.sum
-- Finset.sum : {β : Type u_1} → {α : Type u_2} →
--   [inst : AddCommMonoid β] → Finset α → (α → β) → β

#check @Finset.prod
-- Finset.prod : {β : Type u_1} → {α : Type u_2} →
--   [inst : CommMonoid β] → Finset α → (α → β) → β

求和要求值类型是 AddCommMonoid，连乘要求 CommMonoid。ℕ、ℤ、ℝ 均满足，多项式环 R[X] 亦然。

常用引理：

-- 空集求和为零
#check Finset.sum_empty
-- Finset.sum_empty : ∑ x in ∅, f x = 0

-- 单元素集合
#check Finset.sum_singleton
-- Finset.sum_singleton : ∑ x in {a}, f x = f a

-- 并集（不相交时）
#check Finset.sum_union
-- Finset.sum_union : Disjoint s t → ∑ x in s ∪ t, f x = ∑ x in s, f x + ∑ x in t, f x

-- 常数函数
#check Finset.sum_const
-- Finset.sum_const : ∑ x in s, c = s.card • c

-- filter 分拆
#check Finset.sum_filter

对 range 求和

对 Finset.range n 的求和是最典型的场景：

open BigOperators

-- 前 n 个自然数之和
example (n : ℕ) : ∑ i in Finset.range n, i = n * (n - 1) / 2 := by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [Finset.sum_range_succ]
    omega

Finset.sum_range_succ 是关键引理：

#check Finset.sum_range_succ
-- Finset.sum_range_succ : ∑ x in Finset.range (n + 1), f x =
--   ∑ x in Finset.range n, f x + f n

---

组合恒等式的形式化证明

二项式系数之和

数学中有恒等式 ∑_{k=0}^{n} C(n,k) = 2^n，即 n 元集合的子集总数为 2^n。Mathlib 中的对应定理：

#check Finset.sum_pow_eq_pow_sum  -- 可供参考的方向
#check Nat.sum_range_choose
-- Nat.sum_range_choose : ∀ (n : ℕ),
--   ∑ i in Finset.range (n + 1), n.choose i = 2 ^ n

下面手动验证小规模情形，同时展示 simp 和 norm_num 的协作：

open BigOperators Nat

example : ∑ i in Finset.range 4, (3).choose i = 2 ^ 3 := by
  simp [Finset.sum_range_succ, Nat.choose]
  norm_num

完整归纳证明版本：

open BigOperators

theorem sum_choose_eq_two_pow (n : ℕ) :
    ∑ i in Finset.range (n + 1), n.choose i = 2 ^ n := by
  exact Nat.sum_range_choose n

这里直接引用 Mathlib 中已有定理。了解它的存在比重新证明更重要，而 #check 是定位这类引理的入口。

连乘的单调性示例

open BigOperators

-- 前 n 个正整数的连乘即 n!
example (n : ℕ) : ∏ i in Finset.range n, (i + 1) = n.factorial := by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [Finset.prod_range_succ, ih]
    ring

Finset.prod_range_succ 的结构与 sum_range_succ 对称：

#check Finset.prod_range_succ
-- Finset.prod_range_succ : ∏ x in Finset.range (n + 1), f x =
--   ∏ x in Finset.range n, f x * f n

---

Nat.Prime 与初等数论

Prime 的定义与基本引理

Mathlib4 中 Nat.Prime p 的定义等价于：p ≥ 2 且 p 的因子只有 1 和 p 自身。

#check Nat.Prime
-- Nat.Prime : ℕ → Prop

-- 2 是素数
#check Nat.prime_def_lt_dvd
-- 可以用 norm_num 直接验证小素数：
example : Nat.Prime 2 := by norm_num
example : Nat.Prime 17 := by norm_num
example : Nat.Prime 97 := by norm_num

常用引理：

-- 素数大于等于 2
#check Nat.Prime.two_le
-- Nat.Prime.two_le : Nat.Prime p → 2 ≤ p

-- 素数不等于 1
#check Nat.Prime.one_lt
-- Nat.Prime.one_lt : Nat.Prime p → 1 < p

-- 素数整除乘积则整除某个因子
#check Nat.Prime.dvd_mul
-- Nat.Prime.dvd_mul : Nat.Prime p → (p ∣ m * n ↔ p ∣ m ∨ p ∣ n)

-- 整除判定
#check Nat.dvd_antisymm

Nat.factors 分解

Nat.factors n 返回 n 的素因子列表（升序，含重复）：

#eval Nat.factors 12   -- [2, 2, 3]
#eval Nat.factors 100  -- [2, 2, 5, 5]
#eval Nat.factors 1    -- []
#eval Nat.factors 0    -- []

关键性质由以下引理刻画：

-- factors 的乘积等于原数
#check Nat.factors_prod
-- Nat.factors_prod : 0 < n → (Nat.factors n).prod = n

-- factors 中每个元素都是素数
#check Nat.prime_of_mem_factors
-- Nat.prime_of_mem_factors : p ∈ n.factors → Nat.Prime p

-- factors 是有序的
#check Nat.factors_sorted

实际证明中，可以用 decide 验证具体数的分解：

example : Nat.factors 30 = [2, 3, 5] := by decide
example : (Nat.factors 12).length = 4 := by decide

欧几里得定理的局部形式

素数无穷多这一结论在 Mathlib 中由 Nat.infinite_primes 给出，其核心是构造性的。可以验证前若干个素数的存在：

open BigOperators

-- 100 以内的素数个数
#eval (Finset.range 100).filter Nat.Prime |>.card
-- 25

-- 验证小于 20 的素数集合
#eval (Finset.range 20).filter Nat.Prime
-- {2, 3, 5, 7, 11, 13, 17, 19}

下面用 BigOperators 写出「前若干个素数之积加一仍然不被小素数整除」的可计算验证：

-- 2*3*5*7 + 1 = 211，用 decide 验证 211 不被 2,3,5,7 中任何数整除
example : ∀ p ∈ ({2, 3, 5, 7} : Finset ℕ), ¬ p ∣ (2 * 3 * 5 * 7 + 1) := by
  decide

---

decide tactic 与可判定命题

Decidable 类型类

Decidable p 是 Lean 4 中对命题 p : Prop 的可计算判定能力的类型类编码：

class Decidable (p : Prop) where
  decide : Bool
  proof  : decide = true ↔ p

实际定义略有不同，但语义等价：

inductive Decidable (p : Prop) : Type
  | isFalse : ¬p → Decidable p
  | isTrue  :  p → Decidable p

当 Decidable p 有实例时，decide tactic 可以直接通过计算核验 p 是否为真。若计算结果为 true，核（kernel）检查通过，证明完成；若为 false，tactic 失败并报错。

decide 的适用场景

decide 本质上是把命题的证明归约为一次布尔函数求值，因此：

• 命题必须具有 Decidable 实例
• 求值必须在合理时间内终止
• 适合有限域穷举、具体数值验证、小规模组合命题

-- 基础算术
example : 7 * 8 = 56 := by decide
example : ¬ (13 ∣ 100) := by decide

-- 有限类型穷举
example : ∀ b : Bool, b || !b = true := by decide

-- Fin 上的命题
example : ∀ x : Fin 5, x.val < 5 := by decide

-- 有限集合中的性质
example : ∀ x ∈ ({2, 3, 5, 7} : Finset ℕ), Nat.Prime x := by decide

decide 与 norm_num 的边界

norm_num 和 decide 都能验证具体数值命题，但侧重不同：

• norm_num 专门处理数值表达式，内置高效的算术算法，可处理非常大的数；
• decide 通用性更强，适用于任何有 Decidable 实例的命题，但对大规模计算会超时。

-- norm_num 更适合大数验证
example : Nat.Prime 999983 := by norm_num

-- decide 适合小规模有限穷举
example : ∀ n : Fin 10, n.val ^ 2 < 100 := by decide

DecidableEq 与 Finset 操作

DecidableEq α 是 ∀ a b : α, Decidable (a = b) 的缩写，是 Finset 大多数操作的前提条件：

-- filter 需要 DecidablePred
#check @Finset.filter
-- Finset.filter : (p : α → Prop) → [DecidablePred p] → Finset α → Finset α

-- 用 filter 筛选 Finset.range 中的偶数
#eval (Finset.range 10).filter (fun n => n % 2 == 0)
-- {0, 2, 4, 6, 8}

-- 对筛选结果求和
#eval ((Finset.range 10).filter (fun n => n % 2 == 0)).sum id
-- 20

在 tactic 证明中，filter 与 decide 经常配合使用：

open BigOperators

-- 10 以内偶数之和等于 20
example : ∑ i in (Finset.range 10).filter (· % 2 == 0), i = 20 := by decide

---

term-mode 与 tactic-mode 的对比

同一个有限集合命题，可以用 tactic 模式写，也可以用 term 模式写，两者在 Lean 4 中等价。

tactic 模式

open BigOperators

theorem sum_range_four : ∑ i in Finset.range 5, i = 10 := by
  simp [Finset.sum_range_succ]

term 模式

open BigOperators

theorem sum_range_four' : ∑ i in Finset.range 5, i = 10 :=
  by native_decide

或者完全展开（用于理解 Finset.sum 的计算路径）：

theorem sum_range_four'' : ∑ i in Finset.range 5, i = 10 := rfl

rfl 能工作是因为两边在定义展开后规约到相同的 ℕ 字面量，Lean 4 的 kernel 通过 definitional equality 自动确认。

InfoView 的使用

在编写 BigOperators 证明时，InfoView 是不可缺少的工具。把光标放在 tactic 行上，可以看到当前证明目标。例如，在下面的证明中：

theorem prod_range_three : ∏ i in Finset.range 3, (i + 1) = 6 := by
  rw [Finset.prod_range_succ]   -- 光标放这里
  rw [Finset.prod_range_succ]
  simp

第一次 rw 后，InfoView 显示：

⊢ (∏ x in Finset.range 2, (x + 1)) * (2 + 1) = 6

这让用户确认 prod_range_succ 的展开方向和剩余目标，而不必在脑中推演整个展开过程。

---

完整示例：Finset.card 与容斥

容斥原理的形式化

容斥原理的基本形式在 Mathlib 中由 Finset.card_union_add_card_inter 给出：

#check Finset.card_union_add_card_inter
-- Finset.card_union_add_card_inter :
--   (s ∪ t).card + (s ∩ t).card = s.card + t.card

下面验证一个具体的容斥计算：

-- s = {1,2,3,4}, t = {3,4,5,6}
-- s ∪ t = {1,2,3,4,5,6}, s ∩ t = {3,4}
-- |s ∪ t| + |s ∩ t| = 6 + 2 = 8 = |s| + |t| = 4 + 4
example :
    let s : Finset ℕ := {1, 2, 3, 4}
    let t : Finset ℕ := {3, 4, 5, 6}
    (s ∪ t).card + (s ∩ t).card = s.card + t.card := by
  decide

decide 对这类命题非常干净，无需手动拆解集合操作。

filter 与 card

用 filter 计算满足条件的元素个数：

open BigOperators

-- 1 到 30 中，既被 2 整除又被 3 整除的数的个数
example : ((Finset.range 31).filter (fun n => 2 ∣ n ∧ 3 ∣ n)).card = 5 := by
  decide
-- {0, 6, 12, 18, 24, 30} 中去掉 0，共 5 个正整数 (6,12,18,24,30)

注意 Finset.range 31 包含 0，上述命题包含 0，所以结果为 6（含 0）。调整为仅正整数：

example : ((Finset.range 31).filter (fun n => n > 0 ∧ 2 ∣ n ∧ 3 ∣ n)).card = 5 := by
  decide

---

数论应用：素数的有限验证

验证 Goldbach 猜想的小规模情形

Goldbach 猜想（每个大于 2 的偶数都是两个素数之和）尚未被完全证明，但有限范围内可以穷举验证：

-- 验证 [4, 100] 内的所有偶数都能写成两个素数之和
-- 这是一个有限命题，decide 可以处理
example : ∀ n ∈ (Finset.range 49).image (· * 2 + 4),
    ∃ p ∈ (Finset.range n).filter Nat.Prime,
    ∃ q ∈ (Finset.range n).filter Nat.Prime,
    p + q = n := by
  decide

这个 decide 调用会穷举所有目标偶数和所有候选素数对，计算量随范围增大而增长，对较大范围需要改用 native_decide（调用本机编译后的代码而非 Lean 的 kernel 解释器）：

-- native_decide 比 decide 快得多，适合较大有限域
example : ∀ n ∈ (Finset.range 200).image (· * 2 + 4),
    ∃ p ∈ (Finset.range (n + 1)).filter Nat.Prime,
    ∃ q ∈ (Finset.range (n + 1)).filter Nat.Prime,
    p + q = n := by
  native_decide

梅森素数的具体验证

梅森数 M_p = 2^p - 1，当 M_p 是素数时称为梅森素数：

-- 验证前几个梅森素数
example : Nat.Prime (2 ^ 2 - 1) := by norm_num   -- M_2 = 3
example : Nat.Prime (2 ^ 3 - 1) := by norm_num   -- M_3 = 7
example : Nat.Prime (2 ^ 5 - 1) := by norm_num   -- M_5 = 31
example : Nat.Prime (2 ^ 7 - 1) := by norm_num   -- M_7 = 127

-- M_4 = 15 不是素数
example : ¬ Nat.Prime (2 ^ 4 - 1) := by norm_num  -- 15 = 3 × 5

---

练习

练习 1：Finset 求和恒等式

证明前 n 个奇数之和等于 n²：

open BigOperators

-- ∑ i in Finset.range n, (2*i + 1) = n^2
theorem sum_odd_eq_sq (n : ℕ) :
    ∑ i in Finset.range n, (2 * i + 1) = n ^ 2 := by
  sorry  -- 提示：对 n 归纳，使用 Finset.sum_range_succ 和 ring

练习 2：素数筛选

用 Finset.filter 写出"100 以内有多少个素数"的计算，并用 decide 证明结果等于 25：

-- 补全以下定理的证明
theorem prime_count_lt_100 :
    ((Finset.range 100).filter Nat.Prime).card = 25 := by
  sorry  -- 提示：直接用 decide 即可

练习 3：连乘与阶乘

证明 ∏ i in Finset.range n, (i + 1) = n!（Lean 4 中记作 n.factorial）：

open BigOperators

theorem prod_succ_eq_factorial (n : ℕ) :
    ∏ i in Finset.range n, (i + 1) = n.factorial := by
  sorry  -- 提示：归纳，使用 Finset.prod_range_succ，以及 Nat.factorial 的递归定义

---

参考资料

• Mathlib4 文档：Finset
• Mathlib4 文档：BigOperators
• Mathlib4 文档：Nat.Prime
• Lean 4 / Mathlib4 教程：Mathematics in Lean（MIL）第 5 章
• Decidable 类型类文档
• 本系列 04 核心 tactic 精讲
• 本系列 05 simp 与 norm_num