5. 初等数论

在这一章中，我们将向您展示如何将数论中的一些基本结果形式化。 随着我们处理更复杂的数学内容，证明会变得更长、更复杂， 但会建立在您已经掌握的技能之上。

5.1. 无理数根

让我们从古希腊人已知的一个事实开始，即根号 2 是无理数。如果我们假设并非如此，那么我们可以将根号 2 写成最简分数形式 \(\sqrt{2} = a / b\) 。两边平方得到 \(a^2 = 2 b^2\) ，这表明 a 是偶数。如果设 a = 2c ，则有 \(4c^2 = 2 b^2\) ，从而得出 \(b^2 = 2 c^2\) 。这表明 b 也是偶数，与我们假设 a / b 已化为最简形式相矛盾。

说 \(a / b\) 是最简分数意味着 \(a\) 和 \(b\) 没有公因数，也就是说，它们是 互质 的。 Mathlib 定义谓词 Nat.Coprime m n 为 Nat.gcd m n = 1 。 使用 Lean 的匿名投影符号，如果 s 和 t 是类型为 Nat 的表达式，我们可以写 s.Coprime t 而不是 Nat.Coprime s t ，对于 Nat.gcd 也是如此。 和往常一样，Lean 通常会在必要时自动展开 Nat.Coprime 的定义，但我们也可以通过重写或简化使用标识符 Nat.Coprime 来手动进行。

norm_num 策略足够聪明，可以计算出具体的值。

#print Nat.Coprime

example (m n : Nat) (h : m.Coprime n) : m.gcd n = 1 :=
  h

example (m n : Nat) (h : m.Coprime n) : m.gcd n = 1 := by
  rw [Nat.Coprime] at h
  exact h

example : Nat.Coprime 12 7 := by norm_num

example : Nat.gcd 12 8 = 4 := by norm_num

我们在 Section 2.4 中已经遇到过 gcd 函数。对于整数也有一个 gcd 版本；我们将在下面讨论不同数系之间的关系。甚至还有适用于一般代数结构类别的通用 gcd 函数以及通用的 Prime 和 Coprime 概念。在下一章中，我们将了解 Lean 是如何处理这种通用性的。与此同时，在本节中，我们将把注意力限制在自然数上。

我们还需要素数的概念，即 Nat.Prime 。 定理 Nat.prime_def_lt 提供了一个常见的特征描述， 而 Nat.Prime.eq_one_or_self_of_dvd 则提供了另一种。

#check Nat.prime_def_lt

example (p : ℕ) (prime_p : Nat.Prime p) : 2 ≤ p ∧ ∀ m : ℕ, m < p → m ∣ p → m = 1 := by
  rwa [Nat.prime_def_lt] at prime_p

#check Nat.Prime.eq_one_or_self_of_dvd

example (p : ℕ) (prime_p : Nat.Prime p) : ∀ m : ℕ, m ∣ p → m = 1 ∨ m = p :=
  prime_p.eq_one_or_self_of_dvd

example : Nat.Prime 17 := by norm_num

-- commonly used
example : Nat.Prime 2 :=
  Nat.prime_two

example : Nat.Prime 3 :=
  Nat.prime_three

在自然数中，素数具有不能写成非平凡因数乘积的性质。 在更广泛的数学背景下，具有这种性质的环中的元素被称为 不可约元 。 如果一个环中的元素在它整除某个乘积时，就整除其中一个因数，那么这个元素被称为 素元 。 自然数的一个重要性质是，在这种情况下这两个概念是重合的，从而产生了定理 Nat.Prime.dvd_mul 。 我们可以利用这一事实来确立上述论证中的一个关键性质： 如果一个数的平方是偶数，那么这个数本身也是偶数。 Mathlib 在 Algebra.Group.Even 中定义了谓词 Even ，但出于下文将要阐明的原因， 我们将简单地使用 2 ∣ m 来表示 m 是偶数。

#check Nat.Prime.dvd_mul
#check Nat.Prime.dvd_mul Nat.prime_two
#check Nat.prime_two.dvd_mul

theorem even_of_even_sqr {m : ℕ} (h : 2 ∣ m ^ 2) : 2 ∣ m := by
  rw [pow_two, Nat.prime_two.dvd_mul] at h
  cases h <;> assumption

example {m : ℕ} (h : 2 ∣ m ^ 2) : 2 ∣ m :=
  Nat.Prime.dvd_of_dvd_pow Nat.prime_two h

在接下来的学习过程中，您需要熟练掌握查找所需事实的方法。 请记住，如果您能猜出名称的前缀并且已导入相关库，您可以使用制表符补全（有时需要按 Ctrl + Tab ）来找到您要查找的内容。 您可以在任何标识符上按 Ctrl + 点击 跳转到其定义所在的文件，这使您能够浏览附近的定义和定理。 您还可以使用 Lean 社区网页 上的搜索引擎，如果其他方法都行不通，不要犹豫，在 Zulip 上提问。

example (a b c : Nat) (h : a * b = a * c) (h' : a ≠ 0) : b = c :=
  -- apply? suggests the following:
  (mul_right_inj' h').mp h

我们证明根号二为无理数的核心在于以下定理。 试着用 even_of_even_sqr 和定理 Nat.dvd_gcd 来完善证明概要。

example {m n : ℕ} (coprime_mn : m.Coprime n) : m ^ 2 ≠ 2 * n ^ 2 := by
  intro sqr_eq
  have : 2 ∣ m := by
    sorry
  obtain ⟨k, meq⟩ := dvd_iff_exists_eq_mul_left.mp this
  have : 2 * (2 * k ^ 2) = 2 * n ^ 2 := by
    rw [← sqr_eq, meq]
    ring
  have : 2 * k ^ 2 = n ^ 2 :=
    sorry
  have : 2 ∣ n := by
    sorry
  have : 2 ∣ m.gcd n := by
    sorry
  have : 2 ∣ 1 := by
    sorry
  norm_num at this

实际上，只需稍作改动，我们就可以用任意素数替换 2 。在下一个示例中试一试。 在证明的最后，您需要从 p ∣ 1 推导出矛盾。 您可以使用 Nat.Prime.two_le ，它表明任何素数都大于或等于 2，以及 Nat.le_of_dvd 。

example {m n p : ℕ} (coprime_mn : m.Coprime n) (prime_p : p.Prime) : m ^ 2 ≠ p * n ^ 2 := by
  sorry

让我们考虑另一种方法。 这里有一个快速证明：如果 \(p\) 是质数，那么 \(m^2 \ne p n^2\) ：假设 \(m^2 = p n^2\) 并考虑 \(m\) 和 \(n\) 分解成质数的情况，那么方程左边 \(p\) 出现的次数为偶数，而右边为奇数，这与假设相矛盾。 请注意，此论证要求 \(n\) 以及因此 \(m\) 不为零。 下面的形式化证明确认了这一假设是足够的。 唯一分解定理指出，除了零以外的任何自然数都可以唯一地表示为素数的乘积。Mathlib 包含此定理的形式化版本，用函数 Nat.primeFactorsList 来表示，该函数返回一个数的素因数列表，且这些素因数按非递减顺序排列。该库证明了 Nat.primeFactorsList n 中的所有元素都是素数，任何大于零的 n 都等于其素因数的乘积，并且如果 n 等于另一组素数的乘积，那么这组素数就是 Nat.primeFactorsList n 的一个排列。

#check Nat.primeFactorsList
#check Nat.prime_of_mem_primeFactorsList
#check Nat.prod_primeFactorsList
#check Nat.primeFactorsList_unique

您可以浏览这些定理以及附近的其他定理，尽管我们尚未讨论列表成员、乘积或排列。 对于当前的任务，我们不需要这些内容。 相反，我们将使用这样一个事实：Mathlib 有一个函数 Nat.factorization ，它表示与函数相同的数据。 具体来说， Nat.factorization n p ，我们也可以写成 n.factorization p ，返回 p 在 n 的质因数分解中的重数。我们将使用以下三个事实。

theorem factorization_mul' {m n : ℕ} (mnez : m ≠ 0) (nnez : n ≠ 0) (p : ℕ) :
    (m * n).factorization p = m.factorization p + n.factorization p := by
  rw [Nat.factorization_mul mnez nnez]
  rfl

theorem factorization_pow' (n k p : ℕ) :
    (n ^ k).factorization p = k * n.factorization p := by
  rw [Nat.factorization_pow]
  rfl

theorem Nat.Prime.factorization' {p : ℕ} (prime_p : p.Prime) :
    p.factorization p = 1 := by
  rw [prime_p.factorization]
  simp

实际上，在 Lean 中， n.factorization 被定义为一个有限支撑的函数，这解释了在您逐步查看上述证明时会看到的奇怪符号。现在不必担心这个问题。就我们此处的目的而言，可以将上述三个定理当作黑箱来使用。 下一个示例表明，化简器足够智能，能够将 n^2 ≠ 0 替换为 n ≠ 0 。策略 simpa 仅调用 simp 后再调用 assumption 。 看看你能否利用上面的恒等式来补全证明中缺失的部分。

example {m n p : ℕ} (nnz : n ≠ 0) (prime_p : p.Prime) : m ^ 2 ≠ p * n ^ 2 := by
  intro sqr_eq
  have nsqr_nez : n ^ 2 ≠ 0 := by simpa
  have eq1 : Nat.factorization (m ^ 2) p = 2 * m.factorization p := by
    sorry
  have eq2 : (p * n ^ 2).factorization p = 2 * n.factorization p + 1 := by
    sorry
  have : 2 * m.factorization p % 2 = (2 * n.factorization p + 1) % 2 := by
    rw [← eq1, sqr_eq, eq2]
  rw [add_comm, Nat.add_mul_mod_self_left, Nat.mul_mod_right] at this
  norm_num at this

这个证明的一个妙处在于它还能推广。这里的 2 没有什么特殊之处；稍作改动，该证明就能表明，无论何时我们写出 m^k = r * n^k ，那么在 r 中任何素数 p 的幂次都必须是 k 的倍数。 要使用 Nat.count_factors_mul_of_pos 来处理 r * n^k ，我们需要知道 r 是正数。但当 r 为零时，下面的定理是显然成立的，并且很容易通过简化器证明。所以证明是分情况来进行的。 rcases r with _ | r 这一行将目标替换为两个版本：一个版本中 r 被替换为 0 ，另一个版本中 r 被替换为 r + 1 。在第二种情况下，我们可以使用定理 r.succ_ne_zero ，它表明 r + 1 ≠ 0 （ succ 表示后继）。 还要注意，以 have : npow_nz 开头的那行提供了 n^k ≠ 0 的简短证明项证明。 要理解其工作原理，可以尝试用策略证明替换它，然后思考这些策略是如何描述证明项的。 试着补全下面证明中缺失的部分。 在最后，你可以使用 Nat.dvd_sub' 和 Nat.dvd_mul_right 来完成证明。 请注意，此示例并未假定 p 为素数，但当 p 不是素数时结论是显而易见的，因为根据定义此时 r.factorization p 为零，而且无论如何该证明在所有情况下都成立。

example {m n k r : ℕ} (nnz : n ≠ 0) (pow_eq : m ^ k = r * n ^ k) {p : ℕ} :
    k ∣ r.factorization p := by
  rcases r with _ | r
  · simp
  have npow_nz : n ^ k ≠ 0 := fun npowz ↦ nnz (pow_eq_zero npowz)
  have eq1 : (m ^ k).factorization p = k * m.factorization p := by
    sorry
  have eq2 : ((r + 1) * n ^ k).factorization p =
      k * n.factorization p + (r + 1).factorization p := by
    sorry
  have : r.succ.factorization p = k * m.factorization p - k * n.factorization p := by
    rw [← eq1, pow_eq, eq2, add_comm, Nat.add_sub_cancel]
  rw [this]
  sorry

我们或许想要通过多种方式改进这些结果。首先，关于根号二为无理数的证明应当提及根号二，这可以理解为实数或复数中的一个元素。并且，声称其为无理数应当说明有理数的情况，即不存在任何有理数与之相等。此外，我们应当将本节中的定理推广到整数。尽管从数学角度显而易见，如果能将根号二写成两个整数的商，那么也能写成两个自然数的商，但正式证明这一点仍需付出一定努力。 在 Mathlib 中，自然数、整数、有理数、实数和复数分别由不同的数据类型表示。将注意力限制在不同的域上通常是有帮助的：我们会看到对自然数进行归纳很容易，而且在不考虑实数的情况下，关于整数的可除性进行推理是最简单的。但在不同域之间进行转换是一件令人头疼的事，这是我们必须应对的问题。我们将在本章后面再次讨论这个问题。 我们还应当能够将最后一个定理的结论加强，即表明数字 r 是 k 的幂，因为其 k 次方根恰好是每个整除 r 的素数的 r 中该素数的幂次除以 k 后的乘积。要做到这一点，我们需要更好的方法来处理有限集合上的乘积和求和问题，这也是我们之后会再次探讨的一个主题。 事实上，本节中的所有结果在 Mathlib 的 Data.Real.Irrational 中都有更广泛的证明。对于任意交换幺半群，都定义了 重数（multiplicity） 这一概念，其取值范围为扩展自然数 enat ，即在自然数的基础上增加了无穷大这一值。在下一章中，我们将开始探讨 Lean 如何支持这种泛化的方法。

5.2. 归纳与递归

自然数集 \(\mathbb{N} = \{ 0, 1, 2, \ldots \}\) 不仅本身具有根本的重要性，而且在新数学对象的构建中也起着核心作用。 Lean 的基础允许我们声明 归纳类型 ，这些类型由给定的 构造子 列表归纳生成。 在 Lean 中，自然数是这样声明的。

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

您可以在库中通过输入 #check Nat 然后 Ctrl + 点击 标识符 Nat 来找到它。该命令指定了 Nat 是由两个构造函数 zero ： Nat 和 succ ： Nat → Nat 自然且归纳地生成的数据类型。当然，库中为 nat 和 zero 分别引入了记号 ℕ 和 0 。（数字会被转换为二进制表示，但现在我们不必担心这些细节。）

对于数学工作者而言，“自然”意味着类型 Nat 有一个元素 zero 以及一个单射的后继函数 succ ，其值域不包含 zero 。

example (n : Nat) : n.succ ≠ Nat.zero :=
  Nat.succ_ne_zero n

example (m n : Nat) (h : m.succ = n.succ) : m = n :=
  Nat.succ.inj h

对于数学工作者而言，“归纳”这个词意味着自然数附带有一个归纳证明原则和一个递归定义原则。本节将向您展示如何使用这些原则。

以下是一个阶乘函数的递归定义示例。

def fac : ℕ → ℕ
  | 0 => 1
  | n + 1 => (n + 1) * fac n

这种语法需要一些时间来适应。 请注意第一行没有 := 。 接下来的两行提供了递归定义的基础情况和归纳步骤。 这些等式是定义性成立的，但也可以通过将名称 fac 给予 simp 或 rw 来手动使用。

example : fac 0 = 1 :=
  rfl

example : fac 0 = 1 := by
  rw [fac]

example : fac 0 = 1 := by
  simp [fac]

example (n : ℕ) : fac (n + 1) = (n + 1) * fac n :=
  rfl

example (n : ℕ) : fac (n + 1) = (n + 1) * fac n := by
  rw [fac]

example (n : ℕ) : fac (n + 1) = (n + 1) * fac n := by
  simp [fac]

阶乘函数实际上已经在 Mathlib 中定义为 Nat.factorial 。您可以通过输入 #check Nat.factorial 并使用 Ctrl + 点击 跳转到它。为了便于说明，我们在示例中将继续使用 fac 。定义 Nat.factorial 前面的注释 @[simp] 指定定义方程应添加到简化的默认等式数据库中。 归纳法原理指出，我们可以通过证明某个关于自然数的一般性陈述对 0 成立，并且每当它对某个自然数 \(n\) 成立时，它对 \(n + 1\) 也成立，从而证明该一般性陈述。因此，在下面的证明中，行 induction' n with n ih 会产生两个目标：在第一个目标中，我们需要证明 0 < fac 0 ；在第二个目标中，我们有额外的假设 ih : 0 < fac n ，并且需要证明 0 < fac (n + 1) 。短语 with n ih 用于为归纳假设命名变量和假设，您可以为它们选择任何名称。

theorem fac_pos (n : ℕ) : 0 < fac n := by
  induction' n with n ih
  · rw [fac]
    exact zero_lt_one
  rw [fac]
  exact mul_pos n.succ_pos ih

该 induction 策略足够智能，能够将依赖于归纳变量的假设作为归纳假设的一部分包含进来。 接下来，我们可以逐步执行一个示例，以具体说明这一过程。

theorem dvd_fac {i n : ℕ} (ipos : 0 < i) (ile : i ≤ n) : i ∣ fac n := by
  induction' n with n ih
  · exact absurd ipos (not_lt_of_ge ile)
  rw [fac]
  rcases Nat.of_le_succ ile with h | h
  · apply dvd_mul_of_dvd_right (ih h)
  rw [h]
  apply dvd_mul_right

以下示例为阶乘函数提供了一个粗略的下界。 结果发现，从分情况证明入手会更容易些，这样证明的其余部分就从 \(n = 1\) 的情况开始。 尝试使用 pow_succ 或 pow_succ' 通过归纳法完成论证。

theorem pow_two_le_fac (n : ℕ) : 2 ^ (n - 1) ≤ fac n := by
  rcases n with _ | n
  · simp [fac]
  sorry

归纳法常用于证明涉及有限和与乘积的恒等式。 Mathlib 定义了表达式 Finset.sum s f ，其中 s : Finset α 是类型为 α 的元素的有限集合，而 f 是定义在 α 上的函数。

f 的值域可以是任何支持交换、结合加法运算且具有零元素的类型。

如果您导入 Algebra.BigOperators.Basic 并执行命令 open BigOperators ，则可以使用更直观的符号 ∑ x in s, f x 。当然，对于有限乘积也有类似的运算和符号。

我们将在下一节以及稍后的章节中讨论 Finset 类型及其支持的操作。目前，我们仅使用 Finset.range n ，它表示小于 n 的自然数的有限集合。

variable {α : Type*} (s : Finset ℕ) (f : ℕ → ℕ) (n : ℕ)

#check Finset.sum s f
#check Finset.prod s f

open BigOperators
open Finset

example : s.sum f = ∑ x in s, f x :=
  rfl

example : s.prod f = ∏ x in s, f x :=
  rfl

example : (range n).sum f = ∑ x in range n, f x :=
  rfl

example : (range n).prod f = ∏ x in range n, f x :=
  rfl

事实 Finset.sum_range_zero 和 Finset.sum_range_succ 为求和至 \(n\) 提供了递归描述，乘积的情况也是如此。

example (f : ℕ → ℕ) : ∑ x in range 0, f x = 0 :=
  Finset.sum_range_zero f

example (f : ℕ → ℕ) (n : ℕ) : ∑ x in range n.succ, f x = ∑ x in range n, f x + f n :=
  Finset.sum_range_succ f n

example (f : ℕ → ℕ) : ∏ x in range 0, f x = 1 :=
  Finset.prod_range_zero f

example (f : ℕ → ℕ) (n : ℕ) : ∏ x in range n.succ, f x = (∏ x in range n, f x) * f n :=
  Finset.prod_range_succ f n

每对中的第一个恒等式是定义性的，也就是说，您可以将证明替换为 rfl 。

以下表达的是我们定义为乘积形式的阶乘函数。

example (n : ℕ) : fac n = ∏ i in range n, (i + 1) := by
  induction' n with n ih
  · simp [fac, prod_range_zero]
  simp [fac, ih, prod_range_succ, mul_comm]

我们将 mul_comm 作为简化规则包含在内这一事实值得评论。 使用恒等式 x * y = y * x 进行简化似乎很危险，因为这通常会导致无限循环。 不过，Lean 的简化器足够聪明，能够识别这一点，并且仅在结果项在某些固定但任意的项排序中具有较小值的情况下应用该规则。 下面的示例表明，使用 mul_assoc 、 mul_comm 和 mul_left_comm 这三条规则进行简化，能够识别出括号位置和变量顺序不同但实质相同的乘积。

example (a b c d e f : ℕ) : a * (b * c * f * (d * e)) = d * (a * f * e) * (c * b) := by
  simp [mul_assoc, mul_comm, mul_left_comm]

大致来说，这些规则的作用是将括号向右推移，然后重新排列两边的表达式，直到它们都遵循相同的规范顺序。利用这些规则以及相应的加法规则进行简化，是个很实用的技巧。

回到求和恒等式，我们建议按照以下证明步骤来证明自然数之和（从 1 加到 n）等于 \(n (n + 1) / 2\)。 证明的第一步是消去分母。 这在形式化恒等式时通常很有用，因为涉及除法的计算通常会有附加条件。 （同样，在可能的情况下避免在自然数上使用减法也是有用的。）

theorem sum_id (n : ℕ) : ∑ i in range (n + 1), i = n * (n + 1) / 2 := by
  symm; apply Nat.div_eq_of_eq_mul_right (by norm_num : 0 < 2)
  induction' n with n ih
  · simp
  rw [Finset.sum_range_succ, mul_add 2, ← ih]
  ring

我们鼓励您证明类似的平方和恒等式，以及您在网上能找到的其他恒等式。

theorem sum_sqr (n : ℕ) : ∑ i in range (n + 1), i ^ 2 = n * (n + 1) * (2 * n + 1) / 6 := by
  sorry

在 Lean 的核心库中，加法和乘法本身是通过递归定义来定义的，并且它们的基本性质是通过归纳法来确立的。 如果您喜欢思考诸如基础性的话题，您可能会喜欢证明乘法和加法的交换律和结合律以及乘法对加法的分配律。 您可以在自然数的副本上按照下面的提纲进行操作。 请注意，我们可以对 MyNat 使用 induction 策略； Lean 足够聪明，知道要使用相关的归纳原理（当然，这与 Nat 的归纳原理相同）。

我们先从加法的交换律讲起。 一个不错的经验法则是，由于加法和乘法都是通过在第二个参数上递归定义的，所以通常在证明中对处于该位置的变量进行归纳证明是有利的。 在证明结合律时，决定使用哪个变量有点棘手。

在没有通常的零、一、加法和乘法符号的情况下书写内容可能会令人困惑。 稍后我们将学习如何定义此类符号。 在命名空间 MyNat 中工作意味着我们可以写 zero 和 succ 而不是 MyNat.zero 和 MyNat.succ ， 并且这些名称的解释优先于其他解释。 在命名空间之外，例如下面定义的 add 的完整名称是 MyNat.add 。

如果您发现自己确实喜欢这类事情，不妨试着定义截断减法和幂运算，并证明它们的一些性质。 请记住，截断减法在结果为零时会停止。 要定义截断减法，定义一个前驱函数 pred 会很有用，该函数对任何非零数减一，并将零固定不变。 函数 pred 可以通过简单的递归实例来定义。

inductive MyNat where
  | zero : MyNat
  | succ : MyNat → MyNat

namespace MyNat

def add : MyNat → MyNat → MyNat
  | x, zero => x
  | x, succ y => succ (add x y)

def mul : MyNat → MyNat → MyNat
  | x, zero => zero
  | x, succ y => add (mul x y) x

theorem zero_add (n : MyNat) : add zero n = n := by
  induction' n with n ih
  · rfl
  rw [add, ih]

theorem succ_add (m n : MyNat) : add (succ m) n = succ (add m n) := by
  induction' n with n ih
  · rfl
  rw [add, ih]
  rfl

theorem add_comm (m n : MyNat) : add m n = add n m := by
  induction' n with n ih
  · rw [zero_add]
    rfl
  rw [add, succ_add, ih]

theorem add_assoc (m n k : MyNat) : add (add m n) k = add m (add n k) := by
  sorry
theorem mul_add (m n k : MyNat) : mul m (add n k) = add (mul m n) (mul m k) := by
  sorry
theorem zero_mul (n : MyNat) : mul zero n = zero := by
  sorry
theorem succ_mul (m n : MyNat) : mul (succ m) n = add (mul m n) n := by
  sorry
theorem mul_comm (m n : MyNat) : mul m n = mul n m := by
  sorry
end MyNat

5.3. 无穷多个素数

让我们继续探讨归纳法和递归法，这次以另一个数学标准为例：证明存在无穷多个素数。一种表述方式是：对于每一个自然数 \(n\) ，都存在一个大于 \(n\) 的素数。要证明这一点，设 \(p\) 是 \(n！ + 1\) 的任意一个素因数。如果 \(p\) 小于或等于 \(n\) ，那么它能整除 \(n！\) 。由于它也能整除 \(n！ + 1\) ，所以它能整除 1 ，这与事实相悖。因此 \(p\) 大于 \(n\) 。

要使该证明形式化，我们需要证明任何大于或等于 2 的数都有一个质因数。 要做到这一点，我们需要证明任何不等于 0 或 1 的自然数都大于或等于 2。 这让我们看到了形式化的一个奇特之处： 往往正是像这样的简单陈述最难形式化。 这里我们考虑几种实现方式。

首先，我们可以使用 cases 策略以及后继函数在自然数上保持顺序这一事实。

theorem two_le {m : ℕ} (h0 : m ≠ 0) (h1 : m ≠ 1) : 2 ≤ m := by
  cases m; contradiction
  case succ m =>
    cases m; contradiction
    repeat apply Nat.succ_le_succ
    apply zero_le

另一种策略是使用 interval_cases 这一策略，它会在所讨论的变量处于自然数或整数的某个区间内时，自动将目标分解为多个情况。请记住，您可以将鼠标悬停在它上面以查看其文档说明。

example {m : ℕ} (h0 : m ≠ 0) (h1 : m ≠ 1) : 2 ≤ m := by
  by_contra h
  push_neg at h
  interval_cases m <;> contradiction

回想一下， interval_cases m 后面的分号表示接下来的策略将应用于它生成的每个情况。另一个选择是使用 decide 策略，它尝试找到一个决策过程来解决问题。Lean 知道，对于以有界量词 ∀ x, x < n → ... 或 ∃ x, x < n ∧ ... 开头的陈述，可以通过决定有限多个实例来确定其真值。

example {m : ℕ} (h0 : m ≠ 0) (h1 : m ≠ 1) : 2 ≤ m := by
  by_contra h
  push_neg at h
  revert h0 h1
  revert h m
  decide

有了 two_le 这个定理，让我们先证明每个大于 2 的自然数都有一个素数因子。 Mathlib 包含一个函数 Nat.minFac ，它会返回最小的素数因子，但为了学习库的新部分，我们将避免使用它，直接证明这个定理。

在这里，普通的归纳法不够用。 我们想用 强归纳法 ，它允许我们通过证明对于每个自然数 \(n\) ，如果 \(P\) 对所有小于 \(n\) 的值都成立，那么 \(P\) 在 \(n\) 处也成立，从而证明每个自然数 \(n\) 都具有性质 \(P\) 。 在 Lean 中，这个原理被称为 Nat.strong_induction_on ，我们可以使用 using 关键字告诉归纳法策略使用它。 请注意，当我们这样做时，就没有了基本情况；它被包含在一般的归纳步骤中。

论证过程很简单。假设 \(n ≥ 2\) ，如果 \(n\) 是质数，那么证明就完成了。如果不是，那么根据质数的定义之一，它有一个非平凡因子 \(m\) ，此时我们可以对这个因子应用归纳假设。步进证明，看看具体是如何进行的。

theorem exists_prime_factor {n : Nat} (h : 2 ≤ n) : ∃ p : Nat, p.Prime ∧ p ∣ n := by
  by_cases np : n.Prime
  · use n, np
  induction' n using Nat.strong_induction_on with n ih
  rw [Nat.prime_def_lt] at np
  push_neg at np
  rcases np h with ⟨m, mltn, mdvdn, mne1⟩
  have : m ≠ 0 := by
    intro mz
    rw [mz, zero_dvd_iff] at mdvdn
    linarith
  have mgt2 : 2 ≤ m := two_le this mne1
  by_cases mp : m.Prime
  · use m, mp
  · rcases ih m mltn mgt2 mp with ⟨p, pp, pdvd⟩
    use p, pp
    apply pdvd.trans mdvdn

现在我们可以证明我们定理的以下表述形式。 看看你能否完善这个概要。 你可以使用 Nat.factorial_pos 、 Nat.dvd_factorial 和 Nat.dvd_sub' 。

theorem primes_infinite : ∀ n, ∃ p > n, Nat.Prime p := by
  intro n
  have : 2 ≤ Nat.factorial (n + 1) + 1 := by
    sorry
  rcases exists_prime_factor this with ⟨p, pp, pdvd⟩
  refine ⟨p, ?_, pp⟩
  show p > n
  by_contra ple
  push_neg  at ple
  have : p ∣ Nat.factorial (n + 1) := by
    sorry
  have : p ∣ 1 := by
    sorry
  show False
  sorry

让我们考虑上述证明的一个变体，其中不使用阶乘函数，而是假设我们得到一个有限集合 \(\{ p_1， \ldots， p_n \}\) ，并考虑 \(\prod_{i = 1}^n p_i + 1\) 的一个质因数。该质因数必须与每个 \(p_i\) 都不同，这表明不存在包含所有质数的有限集合。

要将此论证形式化，我们需要对有限集合进行推理。在 Lean 中，对于任何类型 α ，类型 Finset α 表示类型为 α 的元素的有限集合。从计算角度对有限集合进行推理需要有一个在 α 上测试相等性的过程，这就是下面代码片段包含假设 [DecidableEq α] 的原因。对于像 ℕ 、 ℤ 和 ℚ 这样的具体数据类型，该假设会自动满足。在对实数进行推理时，可以使用经典逻辑并放弃计算解释来满足该假设。

我们使用命令 open Finset 来使用相关定理的更短名称。与集合的情况不同，涉及有限集的大多数等价关系并非定义上的成立，因此需要手动使用诸如 Finset.subset_iff 、 Finset.mem_union 、 Finset.mem_inter 和 Finset.mem_sdiff 这样的等价关系来展开。不过， ext 策略仍然可以用于通过证明一个有限集的每个元素都是另一个有限集的元素来证明两个有限集相等。

open Finset

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

example : r ∩ (s ∪ t) ⊆ r ∩ s ∪ r ∩ t := by
  rw [subset_iff]
  intro x
  rw [mem_inter, mem_union, mem_union, mem_inter, mem_inter]
  tauto

example : r ∩ (s ∪ t) ⊆ r ∩ s ∪ r ∩ t := by
  simp [subset_iff]
  intro x
  tauto

example : r ∩ s ∪ r ∩ t ⊆ r ∩ (s ∪ t) := by
  simp [subset_iff]
  intro x
  tauto

example : r ∩ s ∪ r ∩ t = r ∩ (s ∪ t) := by
  ext x
  simp
  tauto

end

我们使用了一个新技巧： tauto 策略（还有一个更强的 tauto！ ，这个使用经典逻辑）可以用来省去命题逻辑中的重言式。 看看你能否用这些方法证明下面的两个例子。

example : (r ∪ s) ∩ (r ∪ t) = r ∪ s ∩ t := by
  sorry
example : (r \ s) \ t = r \ (s ∪ t) := by
  sorry

定理 Finset.dvd_prod_of_mem 告诉我们，如果一个数 n 是有限集合 s 的一个元素，那么 n 能整除 ∏ i in s, i 。

example (s : Finset ℕ) (n : ℕ) (h : n ∈ s) : n ∣ ∏ i in s, i :=
  Finset.dvd_prod_of_mem _ h

我们还需要知道，在 n 为素数且 s 为素数集合的情况下，其逆命题也成立。要证明这一点，我们需要以下引理，您应该能够使用定理 Nat.Prime.eq_one_or_self_of_dvd 来证明它。

theorem _root_.Nat.Prime.eq_of_dvd_of_prime {p q : ℕ}
      (prime_p : Nat.Prime p) (prime_q : Nat.Prime q) (h : p ∣ q) :
    p = q := by
  sorry

我们可以利用这个引理来证明，如果一个素数 p 整除有限个素数的乘积，那么它就等于其中的一个素数。 Mathlib 提供了一个关于有限集合的有用归纳原理：要证明某个性质对任意有限集合 s 成立，只需证明其对空集成立，并证明当向集合 s 中添加一个新元素 a ∉ s 时该性质仍成立。 这个原理被称为 Finset.induction_on 。当我们告诉归纳策略使用它时，还可以指定名称 a 和 s ，以及归纳步骤中假设 a ∉ s 的名称和归纳假设的名称。 表达式 Finset.insert a s 表示集合 s 与单元素集合 a 的并集。 恒等式 Finset.prod_empty 和 Finset.prod_insert 则提供了乘积相关的重写规则。 在下面的证明中，第一个 simp 应用了 Finset.prod_empty 。 逐步查看证明的开头部分，以了解归纳过程的展开，然后完成证明。

theorem mem_of_dvd_prod_primes {s : Finset ℕ} {p : ℕ} (prime_p : p.Prime) :
    (∀ n ∈ s, Nat.Prime n) → (p ∣ ∏ n in s, n) → p ∈ s := by
  intro h₀ h₁
  induction' s using Finset.induction_on with a s ans ih
  · simp at h₁
    linarith [prime_p.two_le]
  simp [Finset.prod_insert ans, prime_p.dvd_mul] at h₀ h₁
  rw [mem_insert]
  sorry

我们需要有限集合的一个最后性质。 给定一个元素 s : Set α 和一个关于 α 的谓词 P ，在 第 4 章 中，我们用 { x ∈ s | P x } 表示集合 s 中满足 P 的元素。 对于 s ： Finset α ，类似的概念写作 s.filter P 。

example (s : Finset ℕ) (x : ℕ) : x ∈ s.filter Nat.Prime ↔ x ∈ s ∧ x.Prime :=
  mem_filter

我们现在证明关于存在无穷多个素数的另一种表述，即对于任意的 s : Finset ℕ ，都存在一个素数 p 不属于 s 。 为了得出矛盾，我们假设所有的素数都在 s 中，然后缩小到一个只包含素数的集合 s' 。 将该集合的元素相乘，加一，然后找到结果的一个素因数，这将得出我们所期望的矛盾。 看看你能否完成下面的概要。 在第一个 have 的证明中，你可以使用 Finset.prod_pos 。

theorem primes_infinite' : ∀ s : Finset Nat, ∃ p, Nat.Prime p ∧ p ∉ s := by
  intro s
  by_contra h
  push_neg at h
  set s' := s.filter Nat.Prime with s'_def
  have mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime := by
    intro n
    simp [s'_def]
    apply h
  have : 2 ≤ (∏ i in s', i) + 1 := by
    sorry
  rcases exists_prime_factor this with ⟨p, pp, pdvd⟩
  have : p ∣ ∏ i in s', i := by
    sorry
  have : p ∣ 1 := by
    convert Nat.dvd_sub' pdvd this
    simp
  show False
  sorry

因此，我们看到了两种表述素数有无穷多个的方式：一种是说它们不受任何 n 的限制，另一种是说它们不在任何有限集合 s 中。下面的两个证明表明这两种表述是等价的。在第二个证明中，为了形成 s.filter Q ，我们必须假设存在一个判定 Q 是否成立的程序。Lean 知道存在一个判定 Nat.Prime 的程序。一般来说，如果我们通过写 open Classical 来使用经典逻辑，就可以省去这个假设。 在 Mathlib 中， Finset.sup s f 表示当 x 遍历 s 时 f x 的上确界，如果 s 为空且 f 的值域为 ℕ ，则返回 0 。在第一个证明中，我们使用 s.sup id``来表示 ``s 中的最大值，其中 id 是恒等函数。

theorem bounded_of_ex_finset (Q : ℕ → Prop) :
    (∃ s : Finset ℕ, ∀ k, Q k → k ∈ s) → ∃ n, ∀ k, Q k → k < n := by
  rintro ⟨s, hs⟩
  use s.sup id + 1
  intro k Qk
  apply Nat.lt_succ_of_le
  show id k ≤ s.sup id
  apply le_sup (hs k Qk)

theorem ex_finset_of_bounded (Q : ℕ → Prop) [DecidablePred Q] :
    (∃ n, ∀ k, Q k → k ≤ n) → ∃ s : Finset ℕ, ∀ k, Q k ↔ k ∈ s := by
  rintro ⟨n, hn⟩
  use (range (n + 1)).filter Q
  intro k
  simp [Nat.lt_succ_iff]
  exact hn k

对证明存在无穷多个素数的第二种方法稍作修改，即可证明存在无穷多个模 4 余 3 的素数。论证过程如下。 首先，注意到如果两个数 \(m\) 和 \(n\) 的乘积模 4 余 3，那么这两个数中必有一个模 4 余 3。毕竟，这两个数都必须是奇数，如果它们都模 4 余 1，那么它们的乘积也模 4 余 1。 利用这一观察结果，我们可以证明，如果某个大于 2 的数模 4 余 3，那么这个数有一个模 4 余 3 的素因数。 现在假设只有有限个形如 4n + 3 的素数，设为 \(p_1, \ldots, p_k\) 。不失一般性，我们可以假设 \(p_1 = 3\) 。考虑乘积 \(4 \prod_{i = 2}^k p_i + 3\) 。显然，这个数除以 4 的余数为 3，所以它有一个形如 4n + 3 的素因数 \(p\) 。\(p\) 不可能等于 3；因为 \(p\) 整除 \(4 \prod_{i = 2}^k p_i + 3\) ，如果 \(p\) 等于 3，那么它也会整除 \(\prod_{i = 2}^k p_i\) ，这意味着 \(p\) 等于 \(p_i\) 中的一个（i = 2， …， k），但我们已将 3 排除在该列表之外。所以 \(p\) 必须是其他 \(p_i\) 中的一个。但在这种情况下，\(p\) 会整除 \(4 \prod_{i = 2}^k p_i\) 以及 3，这与 \(p\) 不是 3 这一事实相矛盾。 在 Lean 中，记号 n % m ，读作 n 模 m ，表示 n 除以 m 的余数。

example : 27 % 4 = 3 := by norm_num

然后我们可以将“ n 除以 4 余 3”这一表述写成 n % 4 = 3 。下面的示例和定理总结了我们接下来需要用到的关于此函数的事实。第一个命名定理是通过少量情况推理的又一示例。在第二个命名定理中，请记住分号表示后续的策略块应用于前面策略生成的所有目标。

example (n : ℕ) : (4 * n + 3) % 4 = 3 := by
  rw [add_comm, Nat.add_mul_mod_self_left]

theorem mod_4_eq_3_or_mod_4_eq_3 {m n : ℕ} (h : m * n % 4 = 3) : m % 4 = 3 ∨ n % 4 = 3 := by
  revert h
  rw [Nat.mul_mod]
  have : m % 4 < 4 := Nat.mod_lt m (by norm_num)
  interval_cases m % 4 <;> simp [-Nat.mul_mod_mod]
  have : n % 4 < 4 := Nat.mod_lt n (by norm_num)
  interval_cases n % 4 <;> simp

theorem two_le_of_mod_4_eq_3 {n : ℕ} (h : n % 4 = 3) : 2 ≤ n := by
  apply two_le <;>
    · intro neq
      rw [neq] at h
      norm_num at h

我们还需要以下事实，即如果 m 是 n 的非平凡因数，那么 n / m 也是。试着用 Nat.div_dvd_of_dvd 和 Nat.div_lt_self 完成证明。

theorem aux {m n : ℕ} (h₀ : m ∣ n) (h₁ : 2 ≤ m) (h₂ : m < n) : n / m ∣ n ∧ n / m < n := by
  sorry

现在把所有部分整合起来，证明任何模 4 余 3 的数都有一个具有相同性质的素因数。

theorem exists_prime_factor_mod_4_eq_3 {n : Nat} (h : n % 4 = 3) :
    ∃ p : Nat, p.Prime ∧ p ∣ n ∧ p % 4 = 3 := by
  by_cases np : n.Prime
  · use n
  induction' n using Nat.strong_induction_on with n ih
  rw [Nat.prime_def_lt] at np
  push_neg at np
  rcases np (two_le_of_mod_4_eq_3 h) with ⟨m, mltn, mdvdn, mne1⟩
  have mge2 : 2 ≤ m := by
    apply two_le _ mne1
    intro mz
    rw [mz, zero_dvd_iff] at mdvdn
    linarith
  have neq : m * (n / m) = n := Nat.mul_div_cancel' mdvdn
  have : m % 4 = 3 ∨ n / m % 4 = 3 := by
    apply mod_4_eq_3_or_mod_4_eq_3
    rw [neq, h]
  rcases this with h1 | h1
  . sorry
  . sorry

我们已接近尾声。给定一个素数集合 s ，我们需要讨论从该集合中移除 3（如果存在的话）的结果。函数 Finset.erase 可以处理这种情况。

example (m n : ℕ) (s : Finset ℕ) (h : m ∈ erase s n) : m ≠ n ∧ m ∈ s := by
  rwa [mem_erase] at h

example (m n : ℕ) (s : Finset ℕ) (h : m ∈ erase s n) : m ≠ n ∧ m ∈ s := by
  simp at h
  assumption

我们现在准备证明存在无穷多个模 4 余 3 的素数。 请补全下面缺失的部分。 我们的解法会用到 Nat.dvd_add_iff_left 和 Nat.dvd_sub' 。

theorem primes_mod_4_eq_3_infinite : ∀ n, ∃ p > n, Nat.Prime p ∧ p % 4 = 3 := by
  by_contra h
  push_neg at h
  rcases h with ⟨n, hn⟩
  have : ∃ s : Finset Nat, ∀ p : ℕ, p.Prime ∧ p % 4 = 3 ↔ p ∈ s := by
    apply ex_finset_of_bounded
    use n
    contrapose! hn
    rcases hn with ⟨p, ⟨pp, p4⟩, pltn⟩
    exact ⟨p, pltn, pp, p4⟩
  rcases this with ⟨s, hs⟩
  have h₁ : ((4 * ∏ i in erase s 3, i) + 3) % 4 = 3 := by
    sorry
  rcases exists_prime_factor_mod_4_eq_3 h₁ with ⟨p, pp, pdvd, p4eq⟩
  have ps : p ∈ s := by
    sorry
  have pne3 : p ≠ 3 := by
    sorry
  have : p ∣ 4 * ∏ i in erase s 3, i := by
    sorry
  have : p ∣ 3 := by
    sorry
  have : p = 3 := by
    sorry
  contradiction

如果您成功完成了证明，恭喜您！这是一项了不起的形式化成就。

5.4. 更多归纳

在 Section 5.2 中，我们看到了如何在自然数上通过递归定义阶乘函数。

def fac : ℕ → ℕ
  | 0 => 1
  | n + 1 => (n + 1) * fac n

我们还看到了如何使用 induction' 策略证明定理。

theorem fac_pos (n : ℕ) : 0 < fac n := by
  induction' n with n ih
  · rw [fac]
    exact zero_lt_one
  rw [fac]
  exact mul_pos n.succ_pos ih

没有单引号的 induction 策略允许更清晰的语法结构

example (n : ℕ) : 0 < fac n := by
  induction n
  case zero =>
    rw [fac]
    exact zero_lt_one
  case succ n ih =>
    rw [fac]
    exact mul_pos n.succ_pos ih

example (n : ℕ) : 0 < fac n := by
  induction n with
  | zero =>
    rw [fac]
    exact zero_lt_one
  | succ n ih =>
    rw [fac]
    exact mul_pos n.succ_pos ih

As usual, you can hover over the keyword induction to read the documentation. The names of the cases zero , and succ , are taken from the definition of the type ℕ.

Notice that the case succ allows you to choose whatever names you want for the induction variable and the inductive hypothesis, here n and ih . You can even prove a theorem with the same notation used to

define a recursive function. …

与往常一样，您可以将鼠标悬停在关键词 induction 上以查看相关文档（？）。 case zero 和 succ 的名称源自类型ℕ的定义。 请注意，case succ 允许您为归纳变量和归纳假设选择任意名称，此处为 n 和 ih 。 您甚至可以使用证明递归函数时使用过的符号来证明定理。（？）

theorem fac_pos' : ∀ n, 0 < fac n
  | 0 => by
    rw [fac]
    exact zero_lt_one
  | n + 1 => by
    rw [fac]
    exact mul_pos n.succ_pos (fac_pos' n)

注意，这里省略了 := 。且额外添加了冒号后的 ∀ n 、每一个case 结尾的 by 以及对 fac_pos' n 的归纳调用，就好像这个定理是一个 n 的递归函数，并在归纳步骤中进行了递归调用。 （译注：这个证明与上面相同，但它没有使用 by 引导的策略模式，而是使用了函数式编程风格的模式匹配写法）

This style of definition is remarkably flexible. Lean’s designers have built in elaborate means of defining recursive functions, and these extend to doing proofs by induction. For example, we can define the Fibonacci function with multiple base cases.

这个定义方式极其灵活。Lean的设计者们内置了复杂递归函数的定义方法（？），并且将这些手段扩展到了归纳法。 举个例子，我们可以以多种基础条件定义斐波纳契数列。

@[simp] def fib : ℕ → ℕ
  | 0 => 0
  | 1 => 1
  | n + 2 => fib n + fib (n + 1)

The @[simp] annotation means that the simplifier will use the defining equations. You can also apply them by writing rw [fib] . Below it will be helpful to give a name to the n + 2 case.

theorem fib_add_two (n : ℕ) : fib (n + 2) = fib n + fib (n + 1) := rfl

example (n : ℕ) : fib (n + 2) = fib n + fib (n + 1) := by rw [fib]

Using Lean’s notation for recursive functions, you can carry out proofs by induction on the natural numbers that mirror the recursive definition of . The following example provides an explicit formula for the nth Fibonacci number in terms of the golden mean, , and its conjugate, . We have to tell Lean that we don’t expect our definitions to generate code because the arithmetic operations on the real numbers are not computable.``fib`` φ φ'

noncomputable section

def phi  : ℝ := (1 + √5) / 2
def phi' : ℝ := (1 - √5) / 2

theorem phi_sq : phi^2 = phi + 1 := by
  field_simp [phi, add_sq]; ring

theorem phi'_sq : phi'^2 = phi' + 1 := by
  field_simp [phi', sub_sq]; ring

theorem fib_eq : ∀ n, fib n = (phi^n - phi'^n) / √5
  | 0   => by simp
  | 1   => by field_simp [phi, phi']
  | n+2 => by field_simp [fib_eq, pow_add, phi_sq, phi'_sq]; ring

end

Induction proofs involving the Fibonacci function do not have to be of that form. Below we reproduce the proof that consecutive Fibonacci numbers are coprime.``Mathlib``

theorem fib_coprime_fib_succ (n : ℕ) : Nat.Coprime (fib n) (fib (n + 1)) := by
  induction n with
  | zero => simp
  | succ n ih =>
    simp only [fib, Nat.coprime_add_self_right]
    exact ih.symm

Using Lean’s computational interpretation, we can evaluate the Fibonacci numbers.

#eval fib 6
#eval List.range 20 |>.map fib

fib n The straightforward implementation of is computationally inefficient. In fact, it runs in time exponential in its argument. (You should think about why.) In Lean, we can implement the following tail-recursive version, whose running time is linear in , and prove that it computes the same function.

def fib' (n : Nat) : Nat :=
  aux n 0 1
where aux
  | 0,   x, _ => x
  | n+1, x, y => aux n y (x + y)

theorem fib'.aux_eq (m n : ℕ) : fib'.aux n (fib m) (fib (m + 1)) = fib (n + m) := by
  induction n generalizing m with
  | zero => simp [fib'.aux]
  | succ n ih => rw [fib'.aux, ←fib_add_two, ih, add_assoc, add_comm 1]

theorem fib'_eq_fib : fib' = fib := by
  ext n
  erw [fib', fib'.aux_eq 0 n]; rfl

#eval fib' 10000

generalizing fib'.aux_eq ∀ m m m + 1 Notice the keyword in the proof of . It serves to insert a in front of the inductive hypothesis, so that in the induction step, can take a different value. You can step through the proof and check that in this case, the quantifier needs to be instantiated to in the inductive step.

erw rw fib’.aux_eq fib 0 fib 1 0 1 erw rw erw Notice also the use of (for “extended rewrite”) instead of . This is used because to rewrite the goal , and have to be reduced to and , respectively. The tactic is more aggressive than in unfolding definitions to match parameters. This isn’t always a good idea; it can waste a lot of time in some cases, so use sparingly.

generalizing Mathlib Here is another example of the keyword in use, in the proof of another identity that is found in . An informal proof of the identity can be found here. We provide two variants of the formal proof.

theorem fib_add (m n : ℕ) : fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1) := by
  induction n generalizing m with
  | zero => simp
  | succ n ih =>
    specialize ih (m + 1)
    rw [add_assoc m 1 n, add_comm 1 n] at ih
    simp only [fib_add_two, Nat.succ_eq_add_one, ih]
    ring

theorem fib_add' : ∀ m n, fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)
  | _, 0     => by simp
  | m, n + 1 => by
    have := fib_add' (m + 1) n
    rw [add_assoc m 1 n, add_comm 1 n] at this
    simp only [fib_add_two, Nat.succ_eq_add_one, this]
    ring

fib_add 代码第二三句似乎多余了（？） As an exercise, use to prove the following.

example (n : ℕ): (fib n) ^ 2 + (fib (n + 1)) ^ 2 = fib (2 * n + 1) := by sorry
example (n : ℕ): (fib n) ^ 2 + (fib (n + 1)) ^ 2 = fib (2 * n + 1) := by
  rw [two_mul, fib_add, pow_two, pow_two]

n ≠ 1 n Nat Lean’s mechanisms for defining recursive functions are flexible enough to allow arbitrary recursive calls, as long the complexity of the arguments decrease according to some well-founded measure. In the next example, we show that every natural number has a prime divisor, using the fact that if is nonzero and not prime, it has a smaller divisor. (You can check that Mathlib has a theorem of the same name in the namespace, though it has a different proof than the one we give here.)

#check (@Nat.not_prime_iff_exists_dvd_lt :
  ∀ {n : ℕ}, 2 ≤ n → (¬Nat.Prime n ↔ ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n))

theorem ne_one_iff_exists_prime_dvd : ∀ {n}, n ≠ 1 ↔ ∃ p : ℕ, p.Prime ∧ p ∣ n
  | 0 => by simpa using Exists.intro 2 Nat.prime_two
  | 1 => by simp [Nat.not_prime_one]
  | n + 2 => by
    have hn : n+2 ≠ 1 := by omega
    simp only [Ne, not_false_iff, true_iff, hn]
    by_cases h : Nat.Prime (n + 2)
    · use n+2, h
    · have : 2 ≤ n + 2 := by omega
      rw [Nat.not_prime_iff_exists_dvd_lt this] at h
      rcases h with ⟨m, mdvdn, mge2, -⟩
      have : m ≠ 1 := by omega
      rw [ne_one_iff_exists_prime_dvd] at this
      rcases this with ⟨p, primep, pdvdm⟩
      use p, primep
      exact pdvdm.trans mdvdn

rw [ne_one_iff_exists_prime_dvd] at this m n + 2 m < n + 2`` n The line is like a magic trick: we are using the very theorem we are proving in its own proof. What makes it work is that the inductive call is instantiated at , the current case is , and the context has . Lean can find the hypothesis and use it to show that the induction is well-founded. Lean is pretty good at figuring out what is decreasing; in this case, the choice of in the statement of the theorem and the less-than relation is obvious. In more complicated cases, Lean provides mechanisms to provide this information explicitly. See the section on well-founded recursion in the Lean Reference Manual. n cases rcases Sometimes, in a proof, you need to split on cases depending on whether a natural number is zero or a successor, without requiring an inductive hypothesis in the successor case. For that, you can use the and tactics.

theorem zero_lt_of_mul_eq_one (m n : ℕ) : n * m = 1 → 0 < n ∧ 0 < m := by
  cases n <;> cases m <;> simp

example (m n : ℕ) : n*m = 1 → 0 < n ∧ 0 < m := by
  rcases m with (_ | m); simp
  rcases n with (_ | n) <;> simp

n n n n + 1 This is a useful trick. Often you have a theorem about a natural number for which the zero case is easy. If you case on and take care of the zero case quickly, you are left with the original goal with replaced by .