6. 离散数学

离散数学是研究有限集、离散对象和离散结构的学科。 我们可以数出有限集中的元素个数，计算元素的有限和或有限积，可以求出这些元素的最大值和最小值，等等。 我们还可以研究某些生成函数所产生的对象，这些对象是经过多次应用这些函数而构造出来的。可以通过结构递归定义函数，使用结构归纳法证明定理。 本章将讲述这些内容中Mathlib支持的部分。

6.1. 有限集合和有限类型

在 Mathlib 中处理有限集合和有限类型可能会令人困惑，因为库提供了多种处理方式。在这一节中，我们将讨论最常见的方法。

我们已经在 Section 5.2 和 Section 5.3 中遇到了类型 Finset。 顾名思义，类型 Finset α 的元素是类型 α 的元素的有限集合。 我们将这些称为”有限集合”。 Finset 数据类型设计为具有计算解释， Finset α 的许多基本操作都假设 α 具有可判定的相等性， 这保证了有一个算法可以测试 a : α 是否是有限集合 s 的元素。

section
variable {α : Type*} [DecidableEq α] (a : α) (s t : Finset α)

#check a ∈ s
#check s ∩ t

end

如果你删除声明 [DecidableEq α]，Lean 会在 #check s ∩ t 这一行报错， 因为它无法计算交集。 然而，所有你应该能够计算的数据类型都具有可判定的相等性， 如果你通过打开 Classical 命名空间并声明 noncomputable section 来进行经典推理， 你可以对任何类型的元素的有限集合进行推理。

有限集合支持集合论的大部分运算：

open Finset

variable (a b c : Finset ℕ)
variable (n : ℕ)

#check a ∩ b
#check a ∪ b
#check a \ b
#check (∅ : Finset ℕ)

example : a ∩ (b ∪ c) = (a ∩ b) ∪ (a ∩ c) := by
  ext x; simp only [mem_inter, mem_union]; tauto

example : a ∩ (b ∪ c) = (a ∩ b) ∪ (a ∩ c) := by rw [inter_union_distrib_left]

请注意，我们已经打开了 Finset 命名空间， 在这里可以找到特定于有限集合的定理。 如果你逐步执行下面的最后一个例子，你会看到应用 ext 后跟 simp 将恒等式简化为命题逻辑的问题。 作为练习，你可以尝试证明 第 4 章 中的一些集合恒等式， 并将它们转换为有限集合。

你已经见过记法 Finset.range n 表示自然数的有限集合 \(\{ 0, 1, \ldots, n-1 \}\)。 Finset 还允许你通过枚举元素来定义有限集合：

#check ({0, 2, 5} : Finset Nat)

def example1 : Finset ℕ := {0, 1, 2}

有多种方式可以让 Lean 识别出以这种方式呈现的集合中元素的顺序和重复 项都无关紧要。

example : ({0, 1, 2} : Finset ℕ) = {1, 2, 0} := by decide

example : ({0, 1, 2} : Finset ℕ) = {0, 1, 1, 2} := by decide

example : ({0, 1} : Finset ℕ) = {1, 0} := by rw [Finset.pair_comm]

example (x : Nat) : ({x, x} : Finset ℕ) = {x} := by simp

example (x y z : Nat) : ({x, y, z, y, z, x} : Finset ℕ) = {x, y, z} := by
  ext i; simp [or_comm, or_assoc, or_left_comm]

example (x y z : Nat) : ({x, y, z, y, z, x} : Finset ℕ) = {x, y, z} := by
  ext i; simp; tauto

你可以使用 insert 向 Finset 中添加单个元素，使用 Finset.erase 删除单个元素。 请注意，erase 在 Finset 命名空间中，但 insert 在根命名空间中。

example (s : Finset ℕ) (a : ℕ) (h : a ∉ s) : (insert a s |>.erase a) = s :=
  Finset.erase_insert h

example (s : Finset ℕ) (a : ℕ) (h : a ∈ s) : insert a (s.erase a) = s :=
  Finset.insert_erase h

实际上，{0, 1, 2} 只是 insert 0 (insert 1 (singleton 2)) 的记法。

set_option pp.notation false in
#check ({0, 1, 2} : Finset ℕ)

给定一个有限集合 s 和一个谓词 P，我们可以使用集合构造记法 {x ∈ s | P x} 来 定义 s 中满足 P 的元素的集合。 这是 Finset.filter P s 的记法，也可以写作 s.filter P。

example : {m ∈ range n | Even m} = (range n).filter Even := rfl
example : {m ∈ range n | Even m ∧ m ≠ 3} = (range n).filter (fun m ↦ Even m ∧ m ≠ 3) := rfl

example : {m ∈ range 10 | Even m} = {0, 2, 4, 6, 8} := by decide

Mathlib 知道有限集合在函数下的像是有限集合。

#check (range 5).image (fun x ↦ x * 2)

example : (range 5).image (fun x ↦ x * 2) = {x ∈ range 10 | Even x} := by decide

Lean 也知道两个有限集合的笛卡尔积 s ×ˢ t 是有限集合， 以及有限集合的幂集是有限集合。（请注意，记法 s ×ˢ t 也适用于集合。）

#check s ×ˢ t
#check s.powerset

根据有限集合的元素来定义运算是很棘手的，因为任何这样的定义都必须 与元素呈现的顺序无关。 当然，你总是可以通过组合现有的运算来定义函数。 你还可以做的另一件事是使用 Finset.fold 对元素进行二元运算的折叠， 前提是运算具有结合律和交换律， 因为这些性质保证了结果与运算应用的顺序无关。有限和、有限积和有限并都是这样定义的。 在下面的最后一个例子中，biUnion 表示”有界索引并”。 用传统的数学记法，这个表达式会写作 \(\bigcup_{i ∈ s} g(i)\)。

#check Finset.fold

def f (n : ℕ) : Int := (↑n)^2

#check (range 5).fold (fun x y : Int ↦ x + y) 0 f
#eval (range 5).fold (fun x y : Int ↦ x + y) 0 f

#check ∑ i ∈ range 5, i^2
#check ∏ i ∈ range 5, i + 1

variable (g : Nat → Finset Int)

#check (range 5).biUnion g

有限集合有一个自然的归纳原理：要证明每个有限集合都有某个性质， 需要证明空集有这个性质，并且当我们向有限集合中添加一个新元素时， 这个性质得到保持。（在下一个例子的归纳步骤中，@insert 中的 @ 符号是必需的， 用于给参数 a 和 s 命名，因为它们被标记为隐式参数。）

#check Finset.induction

example {α : Type*} [DecidableEq α] (f : α → ℕ)  (s : Finset α) (h : ∀ x ∈ s, f x ≠ 0) :
    ∏ x ∈ s, f x ≠ 0 := by
  induction s using Finset.induction_on with
  | empty => simp
  | @insert a s anins ih =>
    rw [prod_insert anins]
    apply mul_ne_zero
    · apply h; apply mem_insert_self
    apply ih
    intros x xs
    exact h x (mem_insert_of_mem xs)

如果 s 是有限集合，Finset.Nonempty s 定义为 ∃ x, x ∈ s。 你可以使用经典选择来从非空有限集合中选择一个元素。类似地， 库定义了 Finset.toList s，它使用选择按某种顺序选择 s 的元素。

noncomputable example (s : Finset ℕ) (h : s.Nonempty) : ℕ := Classical.choose h

example (s : Finset ℕ) (h : s.Nonempty) : Classical.choose h ∈ s := Classical.choose_spec h

noncomputable example (s : Finset ℕ) : List ℕ := s.toList

example (s : Finset ℕ) (a : ℕ) : a ∈ s.toList ↔ a ∈ s := mem_toList

你可以使用 Finset.min 和 Finset.max 来选择线性序的有限集合中的最小或最大元素， 类似地，你可以对格的有限集合使用 Finset.inf 和 Finset.sup，但有一个问题。 空有限集合的最小元素应该是什么？ 你可以检查下面函数的带撇版本添加了有限集合非空的前提条件。 不带撇的版本 Finset.min 和 Finset.max 分别向输出类型添加一个顶元素或底元素， 以处理有限集合为空的情况。 不带撇的版本 Finset.inf 和 Finset.sup 假设格分别配备了顶元素或底元素。

#check Finset.min
#check Finset.min'
#check Finset.max
#check Finset.max'
#check Finset.inf
#check Finset.inf'
#check Finset.sup
#check Finset.sup'

example : Finset.Nonempty {2, 6, 7} := ⟨6, by trivial⟩
example : Finset.min' {2, 6, 7} ⟨6, by trivial⟩ = 2 := by trivial

每个有限集合 s 都有一个有限的基数 Finset.card s，当 Finset 命名空间打开时， 可以写作 #s。

#check Finset.card

#eval (range 5).card

example (s : Finset ℕ) : s.card = #s := by rfl

example (s : Finset ℕ) : s.card = ∑ i ∈ s, 1 := by rw [card_eq_sum_ones]

example (s : Finset ℕ) : s.card = ∑ i ∈ s, 1 := by simp

下一节完全是关于对基数的推理。

在形式化数学时，人们经常需要决定是用集合还是用类型来表达 定义和定理。 使用类型通常简化记法和证明，但使用类型的子集可能更灵活。 有限集合的基于类型的对应物是 有限类型，即某个 α 的类型 Fintype α。 根据定义，有限类型只是一个数据类型，它配备了一个包含所有其元素的有限集合 univ。

variable {α : Type*} [Fintype α]

example : ∀ x : α, x ∈ Finset.univ := by
  intro x; exact mem_univ x

Fintype.card α 等于相应有限集合的基数。

example : Fintype.card α = (Finset.univ : Finset α).card := rfl

我们已经见过有限类型的一个原型例子，即对每个 n 的类型 Fin n。 Lean 识别出有限类型在像积运算这样的运算下是封闭的。

example : Fintype.card (Fin 5) = 5 := by simp
example : Fintype.card ((Fin 5) × (Fin 3)) = 15 := by simp

Finset α 的任何元素 s 都可以强制转换为类型 (↑s : Finset α)， 即包含在 s 中的 α 的元素的子类型。

variable (s : Finset ℕ)

example : (↑s : Type) = {x : ℕ // x ∈ s} := rfl
example : Fintype.card ↑s = s.card := by simp

Lean 和 Mathlib 使用 类型类推断 来追踪有限类型上的附加结构， 即包含所有元素的通用有限集合。 换句话说，你可以将有限类型看作是配备了额外数据的代数结构。 第 7 章 解释了这是如何工作的。

6.2. 计数论证

计数的艺术是组合学的核心部分。 Mathlib 包含了几个用于计数有限集合元素的基本恒等式：

open Finset

variable {α β : Type*} [DecidableEq α] [DecidableEq β] (s t : Finset α) (f : α → β)

example : #(s ×ˢ t) = #s * #t := by rw [card_product]
example : #(s ×ˢ t) = #s * #t := by simp

example : #(s ∪ t) = #s + #t - #(s ∩ t) := by rw [card_union]

example (h : Disjoint s t) : #(s ∪ t) = #s + #t := by rw [card_union_of_disjoint h]
example (h : Disjoint s t) : #(s ∪ t) = #s + #t := by simp [h]

example (h : Function.Injective f) : #(s.image f) = #s := by rw [card_image_of_injective _ h]

example (h : Set.InjOn f s) : #(s.image f) = #s := by rw [card_image_of_injOn h]

打开 Finset 命名空间允许我们使用记法 #s 表示 s.card， 以及使用简化的名称如 card_union 等。

Mathlib 也可以计数有限类型的元素：

open Fintype

variable {α β : Type*} [Fintype α] [Fintype β]

example : card (α × β) = card α * card β := by simp

example : card (α ⊕ β) = card α + card β := by simp

example (n : ℕ) : card (Fin n → α) = (card α)^n := by simp

variable {n : ℕ} {γ : Fin n → Type*} [∀ i, Fintype (γ i)]

example : card ((i : Fin n) → γ i) = ∏ i, card (γ i) := by simp

example : card (Σ i, γ i) = ∑ i, card (γ i) := by simp

当 Fintype 命名空间未打开时，我们必须使用 Fintype.card 而不是 card。

以下是计算有限集合基数的例子，即 range n 与 range n 的一个副本（已向右偏移超过 n）的并集。 这个计算需要证明并集中的两个集合是不相交的； 证明的第一行产生了副条件 Disjoint (range n) (image (fun i ↦ m + i) (range n))， 这在证明的末尾得到了建立。 Disjoint 谓词过于一般，无法直接对我们有用，但定理 disjoint_iff_ne 将它转换为我们可以使用的形式。

#check Disjoint

example (m n : ℕ) (h : m ≥ n) :
    card (range n ∪ (range n).image (fun i ↦ m + i)) = 2 * n := by
  rw [card_union_of_disjoint, card_range, card_image_of_injective, card_range]; omega
  . apply add_right_injective
  . simp [disjoint_iff_ne]; omega

在这一节中，omega 将是我们处理算术计算和不等式的主力工具。

这里有一个更有趣的例子。考虑 \(\{0, \ldots, n\} \times \{0, \ldots, n\}\) 的子集， 它由满足 \(i < j\) 的对 \((i, j)\) 组成。如果你将这些看作坐标平面中的格点， 它们构成了顶点为 \((0, 0)\) 和 \((n, n)\) 的正方形的上三角形， 不包括对角线。完整正方形的基数是 \((n + 1)^2\)，去掉对角线的大小并将结果减半， 显示三角形的基数是 \(n (n + 1) / 2\)。

或者，我们注意到三角形的行的大小是 \(0, 1, \ldots, n\)， 所以基数是前 \(n\) 个自然数的和。下面证明的第一个 have 将三角形描述为行的并集，其中第 \(j\) 行由与 \(j\) 配对的数字 \(0, 1, ..., j - 1\) 组成。 在下面的证明中，记法 (., j) 缩写了函数 fun i ↦ (i, j)。 证明的其余部分只是有限集合基数的计算。

def triangle (n : ℕ) : Finset (ℕ × ℕ) := {p ∈ range (n+1) ×ˢ range (n+1) | p.1 < p.2}

example (n : ℕ) : #(triangle n) = (n + 1) * n / 2 := by
  have : triangle n = (range (n+1)).biUnion (fun j ↦ (range j).image (., j)) := by
    ext p
    simp only [triangle, mem_filter, mem_product, mem_range, mem_biUnion, mem_image]
    constructor
    . rintro ⟨⟨hp1, hp2⟩, hp3⟩
      use p.2, hp2, p.1, hp3
    . rintro ⟨p1, hp1, p2, hp2, rfl⟩
      omega
  rw [this, card_biUnion]; swap
  · -- take care of disjointness first
    intro x _ y _ xney
    simp [disjoint_iff_ne, xney]
  -- continue the calculation
  transitivity (∑ i ∈ range (n + 1), i)
  · congr; ext i
    rw [card_image_of_injective, card_range]
    intros i1 i2; simp
  rw [sum_range_id]; rfl

下面的证明变体使用有限类型而不是有限集合进行计算。 类型 α ≃ β 是 α 和 β 之间的等价类型， 由正向映射、反向映射以及证明这两个映射互为逆映射的证明组成。 证明中的第一个 have 显示 triangle n 等价于 Fin i 的不相交并集， 其中 i 在 Fin (n + 1) 上变化。有趣的是，正向函数和反向函数是用策略构造的， 而不是显式写出的。由于它们只是移动数据和信息，rfl 建立了它们是互逆的。

之后，rw [←Fintype.card_coe] 将 #(triangle n) 重写为子类型 { x // x ∈ triangle n } 的基数，证明的其余部分是计算。

example (n : ℕ) : #(triangle n) = (n + 1) * n / 2 := by
  have : triangle n ≃ Σ i : Fin (n + 1), Fin i.val :=
    { toFun := by
        rintro ⟨⟨i, j⟩, hp⟩
        simp [triangle] at hp
        exact ⟨⟨j, hp.1.2⟩, ⟨i, hp.2⟩⟩
      invFun := by
        rintro ⟨i, j⟩
        use ⟨j, i⟩
        simp [triangle]
        exact j.isLt.trans i.isLt
      left_inv := by intro i; rfl
      right_inv := by intro i; rfl }
  rw [←Fintype.card_coe]
  trans; apply (Fintype.card_congr this)
  rw [Fintype.card_sigma, sum_fin_eq_sum_range]
  convert Finset.sum_range_id (n + 1)
  simp_all

这里是另一种方法。下面证明的第一行将问题简化为证明 2 * #(triangle n) = (n + 1) * n。 我们可以通过证明三角形的两个副本恰好填充矩形 range n ×ˢ range (n + 1) 来做到这一点。 作为练习，看看你能否填写计算的步骤。 在解答中，我们在倒数第二步中广泛依赖 omega， 但不幸的是，我们必须手动完成相当多的工作。

example (n : ℕ) : #(triangle n) = (n + 1) * n / 2 := by
  apply Nat.eq_div_of_mul_eq_right (by norm_num)
  let turn (p : ℕ × ℕ) : ℕ × ℕ := (n - 1 - p.1, n - p.2)
  calc 2 * #(triangle n)
      = #(triangle n) + #(triangle n) := by
          sorry
    _ = #(triangle n) + #(triangle n |>.image turn) := by
          sorry
    _ = #(range n ×ˢ range (n + 1)) := by
          sorry
    _ = (n + 1) * n := by
          sorry

你可以说服自己，如果我们将 triangle 定义中的 n 替换为 n + 1， 将 < 替换为 ≤，我们会得到同样的三角形，只是向下平移了。 下面的练习要求你使用这个事实来证明两个三角形有相同的大小。

def triangle' (n : ℕ) : Finset (ℕ × ℕ) := {p ∈ range n ×ˢ range n | p.1 ≤ p.2}

example (n : ℕ) : #(triangle' n) = #(triangle n) := by sorry

让我们用一个来自 Bhavik Mehta 在 2023 年 Lean for the Curious Mathematician 上 关于组合学的教程 中的一个例子和一个练习来结束这一节。 假设我们有一个二部图，顶点集为 s 和 t，使得对于 s 中的每个 a， 至少有三条边离开 a，对于 t 中的每个 b，最多有一条边进入 b。 那么图中的边的总数至少是 s 的基数的三倍，最多是 t 的基数， 由此可得 s 的基数的三倍最多是 t 的基数。 下面的定理实现了这个论证，其中我们使用关系 r 来表示图的边。 证明是一个优雅的计算。

open Classical
variable (s t : Finset Nat) (a b : Nat)

theorem doubleCounting {α β : Type*} (s : Finset α) (t : Finset β)
    (r : α → β → Prop)
    (h_left : ∀ a ∈ s, 3 ≤ #{b ∈ t | r a b})
    (h_right : ∀ b ∈ t, #{a ∈ s | r a b} ≤ 1) :
    3 * #(s) ≤ #(t) := by
  calc 3 * #(s)
      = ∑ a ∈ s, 3                               := by simp [sum_const_nat, mul_comm]
    _ ≤ ∑ a ∈ s, #({b ∈ t | r a b})              := sum_le_sum h_left
    _ = ∑ a ∈ s, ∑ b ∈ t, if r a b then 1 else 0 := by simp
    _ = ∑ b ∈ t, ∑ a ∈ s, if r a b then 1 else 0 := sum_comm
    _ = ∑ b ∈ t, #({a ∈ s | r a b})              := by simp
    _ ≤ ∑ b ∈ t, 1                               := sum_le_sum h_right
    _ ≤ #(t)                                     := by simp

下面的练习也取自 Mehta 的教程。假设 A 是 range (2 * n) 的一个有 n + 1 个元素的子集。 很容易看出 A 必须包含两个连续的整数，因此包含两个互质的元素。 如果你观看教程，你会看到花费了相当大的努力来建立以下事实， 现在 omega 可以自动证明。

example (m k : ℕ) (h : m ≠ k) (h' : m / 2 = k / 2) : m = k + 1 ∨ k = m + 1 := by omega

Mehta 练习的解答使用了鸽笼原理，以 exists_lt_card_fiber_of_mul_lt_card_of_maps_to 的形式， 来证明 A 中存在两个不同的元素 m 和 k 使得 m / 2 = k / 2。 看看你能否完成这个事实的证明，然后用它来完成证明。

example {n : ℕ} (A : Finset ℕ)
    (hA : #(A) = n + 1)
    (hA' : A ⊆ range (2 * n)) :
    ∃ m ∈ A, ∃ k ∈ A, Nat.Coprime m k := by
  have : ∃ t ∈ range n, 1 < #({u ∈ A | u / 2 = t}) := by
    apply exists_lt_card_fiber_of_mul_lt_card_of_maps_to
    · sorry
    · sorry
  rcases this with ⟨t, ht, ht'⟩
  simp only [one_lt_card, mem_filter] at ht'
  sorry

6.3. 归纳定义的类型

Lean 的基础允许我们定义归纳类型，即从底向上生成实例的数据类型。 例如，元素类型为 α 的列表的数据类型 List α 是通过从空列表 nil 开始生成的， 并且通过依次将元素添加到列表的前面。 下面我们将定义一个二叉树的类型 BinTree，其元素是通过从空树开始生成的， 然后通过将新节点附加到两个现有树来构建新树。

在 Lean 中，可以定义对象为无限的归纳类型，如可数分支的良基树。 但是，有限的归纳定义通常用于离散数学， 特别是在与计算机科学相关的离散数学分支中。 Lean 不仅提供了定义这种类型的方法，还提供了归纳和递归定义的原理。 例如，数据类型 List α 是归纳定义的：

namespace MyListSpace

inductive List (α : Type*) where
  | nil  : List α
  | cons : α → List α → List α

end MyListSpace

归纳定义说 List α 的每个元素要么是 nil``（空列表）， 要么是 ``cons a as，其中 a 是 α 的元素，as 是 α 的元素的列表。 构造子正确地命名为 List.nil 和 List.cons， 但当 List 命名空间打开时，你可以使用更短的记法。 当 List 命名空间 未 打开时，你可以在 Lean 期望列表的任何地方写 .nil 和 .cons a as， Lean 会自动插入 List 限定符。 在这一节中，我们将把临时定义放在像 MyListSpace 这样的独立命名空间中， 以避免与标准库的冲突。在临时命名空间外，我们回到使用标准库定义。

Lean 为 nil 定义了记法 []，为 cons 定义了记法 ::， 你可以为 a :: b :: c :: [] 写 [a, b, c]。 append 和 map 函数如下递归定义：

def append {α : Type*} : List α → List α → List α
  | [],      bs => bs
  | a :: as, bs => a :: (append as bs)

def map {α β : Type*} (f : α → β) : List α → List β
  | []      => []
  | a :: as => f a :: map f as

#eval append [1, 2, 3] [4, 5, 6]
#eval map (fun n => n^2) [1, 2, 3, 4, 5]

注意有一个基本情况和一个递归情况。 在每种情况下，两个定义子句都成立：

theorem nil_append {α : Type*} (as : List α) : append [] as = as := rfl

theorem cons_append {α : Type*} (a : α) (as : List α) (bs : List α) :
    append (a :: as) bs = a :: (append as bs) := rfl

theorem map_nil {α β : Type*} (f : α → β) : map f [] = [] := rfl

theorem map_cons {α β : Type*} (f : α → β) (a : α) (as : List α) :
    map f (a :: as) = f a :: map f as := rfl

函数 append 和 map 在标准库中定义，append as bs 可以写作 as ++ bs。

Lean 允许你按照定义的结构写出归纳证明。

variable {α β γ : Type*}
variable (as bs cs : List α)
variable (a b c : α)

open List

theorem append_nil : ∀ as : List α, as ++ [] = as
  | [] => rfl
  | a :: as => by rw [cons_append, append_nil as]

theorem map_map (f : α → β) (g : β → γ) :
    ∀ as : List α, map g (map f as) = map (g ∘ f) as
  | [] => rfl
  | a :: as => by rw [map_cons, map_cons, map_cons, map_map f g as]; rfl

你也可以使用 induction' 策略。

当然，这些定理已经在标准库中了。作为练习， 尝试在 MyListSpace3 命名空间中定义一个函数 reverse``（以避免与标准的 ``List.reverse 冲突）， 该函数反转列表。 你可以使用 #eval reverse [1, 2, 3, 4, 5] 来测试它。 reverse 的最直接定义需要二次时间，但不要担心这个。 你可以跳转到标准库中 List.reverse 的定义，看看线性时间的实现。 尝试证明 reverse (as ++ bs) = reverse bs ++ reverse as 和 reverse (reverse as) = as。 你可以使用 cons_append 和 append_assoc，但你可能需要想出辅助引理并证明它们。

def reverse : List α → List α := sorry

theorem reverse_append (as bs : List α) : reverse (as ++ bs) = reverse bs ++ reverse as := by
  sorry

theorem reverse_reverse (as : List α) : reverse (reverse as) = as := by sorry

作为另一个例子，考虑以下二叉树的归纳定义，以及计算二叉树大小和深度的函数。

inductive BinTree where
  | empty : BinTree
  | node  : BinTree → BinTree → BinTree

namespace BinTree

def size : BinTree → ℕ
  | empty    => 0
  | node l r => size l + size r + 1

def depth : BinTree → ℕ
  | empty    => 0
  | node l r => max (depth l) (depth r) + 1

将空二叉树计算为大小为 0 和深度为 0 的二叉树是方便的。 在文献中，这种数据类型有时被称为 扩展二叉树。 包含空树意味着，例如，我们可以定义树 node empty (node empty empty)， 它由一个根节点、一个空的左子树和一个由单个节点组成的右子树组成。

这里是一个关于大小和深度的重要不等式：

theorem size_le : ∀ t : BinTree, size t ≤ 2^depth t - 1
  | empty    => Nat.zero_le _
  | node l r => by
    simp only [depth, size]
    calc l.size + r.size + 1
      ≤ (2^l.depth - 1) + (2^r.depth - 1) + 1 := by
          gcongr <;> apply size_le
    _ ≤ (2 ^ max l.depth r.depth - 1) + (2 ^ max l.depth r.depth - 1) + 1 := by
          gcongr <;> simp
    _ ≤ 2 ^ (max l.depth r.depth + 1) - 1 := by
          have : 0 < 2 ^ max l.depth r.depth := by simp
          omega

尝试证明下面的不等式，这相对容易些。 记住，如果你像前面的定理一样做归纳证明，你必须删除 := by。

theorem depth_le_size : ∀ t : BinTree, depth t ≤ size t := by sorry

还要定义二叉树上的 flip 运算，它递归地交换左右子树。

def flip : BinTree → BinTree := sorry

如果你做对了，下面的证明应该是 rfl。

example: flip  (node (node empty (node empty empty)) (node empty empty)) =
    node (node empty empty) (node (node empty empty) empty) := sorry

证明下面的内容：

theorem size_flip : ∀ t, size (flip t) = size t := by sorry

我们以一些形式逻辑来结束这一节。 下面是命题公式的归纳定义。

inductive PropForm : Type where
  | var (n : ℕ)           : PropForm
  | fls                   : PropForm
  | conj (A B : PropForm) : PropForm
  | disj (A B : PropForm) : PropForm
  | impl (A B : PropForm) : PropForm

每个命题公式要么是变量 var n，要么是常数假 fls， 要么是形式为 conj A B、disj A B 或 impl A B 的复合公式。 用普通的数学记法，这些通常写作 \(p_n\)、\(\bot\)、\(A \wedge B\)、 \(A \vee B\) 和 \(A \to B\)。 其他命题连接词可以用这些来定义；例如，我们可以 将 \(\neg A\) 定义为 \(A \to \bot\)，将 \(A \leftrightarrow B\) 定义为 \((A \to B) \wedge (B \to A)\)。

定义了命题公式的数据类型后，我们定义了相对于 变量的布尔真值赋值 v 来求值命题公式的含义。

def eval : PropForm → (ℕ → Bool) → Bool
  | var n,    v => v n
  | fls,      _ => false
  | conj A B, v => A.eval v && B.eval v
  | disj A B, v => A.eval v || B.eval v
  | impl A B, v => ! A.eval v || B.eval v

下一个定义指定了公式中出现的变量的集合， 随后的定理显示了在两个在公式变量上一致的真值赋值下求值公式会得到相同的值。

def vars : PropForm → Finset ℕ
  | var n    => {n}
  | fls      => ∅
  | conj A B => A.vars ∪ B.vars
  | disj A B => A.vars ∪ B.vars
  | impl A B => A.vars ∪ B.vars

theorem eval_eq_eval : ∀ (A : PropForm) (v1 v2 : ℕ → Bool),
    (∀ n ∈ A.vars, v1 n = v2 n) → A.eval v1 = A.eval v2
  | var n, v1, v2, h    => by simp_all [vars, eval, h]
  | fls, v1, v2, h      => by simp_all [eval]
  | conj A B, v1, v2, h => by
      simp_all [vars, eval, eval_eq_eval A v1 v2, eval_eq_eval B v1 v2]
  | disj A B, v1, v2, h => by
      simp_all [vars, eval, eval_eq_eval A v1 v2, eval_eq_eval B v1 v2]
  | impl A B, v1, v2, h => by
      simp_all [vars, eval, eval_eq_eval A v1 v2, eval_eq_eval B v1 v2]

注意到重复，我们可以聪明地使用自动化。

theorem eval_eq_eval' (A : PropForm) (v1 v2 : ℕ → Bool) (h : ∀ n ∈ A.vars, v1 n = v2 n) :
    A.eval v1 = A.eval v2 := by
  cases A <;> simp_all [eval, vars, fun A => eval_eq_eval' A v1 v2]

函数 subst A m C 描述了在公式 A 中用公式 C 替换变量 var m 的每次出现的结果。

def subst : PropForm → ℕ → PropForm → PropForm
  | var n,    m, C => if n = m then C else var n
  | fls,      _, _ => fls
  | conj A B, m, C => conj (A.subst m C) (B.subst m C)
  | disj A B, m, C => disj (A.subst m C) (B.subst m C)
  | impl A B, m, C => impl (A.subst m C) (B.subst m C)

作为例子，证明为一个不在公式中出现的变量进行替换不会有任何效果：

theorem subst_eq_of_not_mem_vars :
    ∀ (A : PropForm) (n : ℕ) (C : PropForm), n ∉ A.vars → A.subst n C = A := sorry

下面的定理说了一些更微妙和有趣的事情：在真值赋值 v 下求值 A.subst n C 与在将 C 的值赋给 var n 的真值赋值下求值 A 是一样的。 看看你能否证明它。

theorem subst_eval_eq : ∀ (A : PropForm) (n : ℕ) (C : PropForm) (v : ℕ → Bool),
  (A.subst n C).eval v = A.eval (fun m => if m = n then C.eval v else v m) := sorry