Ch6 离散数学 - 深度伴读

第6章 离散数学 - 深度伴读

本章定位

本章介绍有限集合和计数，核心概念：

1. 有限集合 Finset
2. 有限类型 Fintype
3. 计数论证

---

6.1 Finsets and Fintypes

核心洞见

• Fintype α：类型 α 是有限的（可以列出所有元素）
• Finset α：类型 α 的有限子集

Fintype：有限类型

-- Fintype α 表示 α 是有限类型
variable [Fintype α]
 
-- 可以列出所有元素
#check (Finset.univ : Finset α)  -- 所有元素的有限集
 
-- 计算元素个数
#check (Fintype.card α : ℕ)

Finset：有限集合

-- Finset α 是 α 的有限子集
variable (s : Finset α)
 
-- 基本操作
s ∩ t      -- 交集
s ∪ t      -- 并集
s.card     -- 元素个数
x ∈ s      -- 成员关系

Finset vs Set

Finset	Set
有限子集	任意子集
可计算	不可计算
有 .card	无 .card
需要 [Fintype α]	不需要

计数论证

-- 鸽巢原理
example (s : Finset α) (f : α → β) :
  s.card ≤ (s.image f).card * ... := by sorry
 
-- 双计数
example : ∑ x in s, f x = ∑ y in t, g y := by sorry

---

6.2 Counting Arguments

核心思想

用有限集合的性质证明组合恒等式。

常用定理

-- 元素个数
Finset.card_univ    -- |univ| = Fintype.card α
Finset.card_image   -- |f '' s| ≤ |s|
Finset.card_union   -- |s ∪ t| = |s| + |t| - |s ∩ t|
 
-- 求和
Finset.sum_const    -- ∑ x in s, c = c * s.card
Finset.sum_add_distrib  -- ∑ x in s, (f x + g x) = ∑ f + ∑ g

证明模式

example : ∑ k in Finset.range (n + 1), k = n * (n + 1) / 2 := by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [Finset.sum_range_succ]
    omega

---

6.3 Inductive Structures

核心思想

用 inductive 定义新的数据结构。

定义归纳类型

-- 二叉树
inductive BinaryTree (α : Type*)
  | leaf : BinaryTree α
  | node : BinaryTree α → α → BinaryTree α → BinaryTree α
 
-- 使用
def tree : BinaryTree ℕ :=
  .node (.node .leaf 1 .leaf) 2 (.node .leaf 3 .leaf)

结构归纳

-- 对二叉树的归纳
def size : BinaryTree α → ℕ
  | .leaf => 0
  | .node l _ r => size l + 1 + size r

---

本章核心 Tactic 总结

Tactic	用途	场景
simp	简化	Finset 操作
omega	线性算术	计数
induction	归纳	结构归纳
decide	可判定	有限情况

---

预告：第7章会学到什么

第7章进入结构化数学：

• 定义结构体
• 代数结构
• 高斯整数

自测问题

1. Finset 和 Set 有什么区别？
2. Fintype.card 返回什么？
3. 如何定义归纳类型？

---

伴读文档 - 第6章完