【学习笔记】Lean4 定理证明 ing

概述

Lean证明是指在Lean环境中，通过编写代码来构造和验证数学定理的过程。Lean使用一种称为依赖类型理论的数学基础，这使得它能够表达复杂的数学概念，并确保证明的正确性。

依赖类型: Lean 所依据的依赖类型论对简单类型论的其中一项升级是，类型本身（如 Nat 和 Bool 这些东西）也是对象，因此也具有类型。简单地说，类型可以依赖于参数。你已经看到了一个很好的例子：类型List α 依赖于参数 α，而这种依赖性是区分 List Nat 和 List Bool 的关键。

Lean4 定理证明初探

Lean的核心思想是将数学证明转化为计算机可以理解和验证的形式化证明。

Lean 证明的基本结构

• 定义：定义数学对象或概念。
• 定理声明：声明要证明的定理。
• 证明构造：通过一系列步骤构造证明。

示例：证明 1 + 1 = 2

-- 定义加法
def add : Nat → Nat → Nat| Nat.zero, n => n| Nat.succ m, n => Nat.succ (add m n)-- 定理声明, 定理的声明通常使用 theorem 关键字
theorem one_plus_one_eq_two : add (Nat.succ Nat.zero) (Nat.succ Nat.zero) = Nat.succ (Nat.succ Nat.zero) :=-- 证明构造rfl

我们首先定义了自然数 Nat 加法函数 add。然后，我们声明了一个定理 one_plus_one_eq_two（类型是 Prop），并使用 rfl（自反性）来证明它。

备注：rfl 是 Lean 中的一个内置策略，用于证明两个表达式在定义上相等。

自反性：定义来自集合A的元素x、y的 “关系” 如下：令C={（x,y）|x、y属于A}，设D是C的某非空子集，如果（x，y）属于D，则称x，y有（由D规定的）关系，记为x ~ y。(符号（,）表示两者组成的有序对）。如果（x，x）属于D总成立，则称那个由D规定的关系具有自反性。

示例：证明 2 * (x + y) = 2 * x + 2 * y

section
variable (x y : Nat)def double := x + x#check double y
#check double (2 * x)attribute [local simp] Nat.add_assoc Nat.add_comm Nat.add_left_comm-- 证明: 2 * (x + y) = 2 * x + 2 * y
theorem t1 : double (x + y) = double x + double y := bysimp [double]#check t1 y
#check t1 (2 * x)-- 证明: 2 * (x * y) = 2 * x * y 
theorem t2 : double (x * y) = double x * y:= bysimp [double, Nat.add_mul]end

by 表示采用策略编写证明，simp 策略，即「化简（Simplify）」的缩写，是 Lean 证明的主力。

Lean4 定理证明基础

命题与定理

命题（Proposition）

命题（Proposition） 是一个可以被判断为真或假的陈述。例如，“2 + 2 = 4”是一个命题，因为它可以被明确地判断为真。在Lean中，命题通常表示为类型为 Prop 的表达式。

-- Implies p q  蕴含概念 等价于 p → q
def Implies (p q : Prop) : Prop := p → q#check And     -- And (a b : Prop) : Prop
#check Or      -- Or (a b : Prop) : Prop
#check Not     -- Not (a : Prop) : Prop
#check Impliesvariable (p q r : Prop)
#check And p q                      -- Prop
#check Or (And p q) r               -- Prop
#check Implies (And p q) (And q p)  -- Prop-- 引入一个结构体 Proof，包含一个 proof 的证明（类型是 p）
structure Proof (p : Prop) : Type whereproof : p#check Proof-- axiom: 公理
axiom andcomm (p q : Prop) : Proof (Implies (And p q) (And q p))variable (p q : Prop)
#check andcomm p q     -- Proof (Implies (p ∧ q) (q ∧ p))-- 公理：如果能证明 Implies p q 和 p，则能证明 q。
axiom modus_ponens : (p q : Prop) → Proof (Implies p q) → Proof p → Proof q-- 公理：当假设 p 成立时，如果我们能证明 q. 则我们能证明 Implies p q.
axiom implies_intro : (p q : Prop) → (Proof p → Proof q) → Proof (Implies p q)

在 Lean 中，命题即是类型。

定义一个命题 is_even 表示 n 是否为偶数：

def is_even (n : Nat) : Prop := n % 2 = 0

使用 def 关键字来定义一个命题 is_even ，它接受一个自然数 n 并返回一个 Prop 类型的值，表示 n 是否为偶数。

定义一个命题 is_prime，表示一个数是否为素数

def is_prime (n : Nat) : Prop :=n > 1 ∧ ∀ m : Nat, m ∣ n → m = 1 ∨ m = n-- m∣n: 表示存在一些 c，使得 n = m * c。

这个命题表示 n 大于1，并且对于所有能整除 n 的数 m，m 要么是1，要么是 n 本身。

∀ 是一个表示“全称量词”的符号，读作“对于所有”或“任意”。它用于表示某个命题对指定范围内的所有元素都成立。例如，当我们说“∀x”，意味着对于所有的x，后面的表达式都是成立的。

∀ {p q : Prop}, p → q → p。我们可以把它理解为「对于每一对命题 p q，我们都有 p → q → p」

有两种将命题作为类型来思考的方法

• 构造角度：命题 p 代表了一种数据类型，即构成证明的数据类型的说明。p 的证明就是正确类型的对象 t : p。
• 非构造角度：对于每个命题p，我们关联一个类型，如果 p 为假，则该类型为空，如果 p 为真，则有且只有一个元素，比如 *，也可以说(与之相关的类型)p 被占据（inhabited）。t : p 告诉我们 p 确实是正确的。你可以把 p 的占据者想象成「p 为真」的事实。对 p → q 的证明使用「p 是真的」这个事实来得到「q 是真的」这个事实。

如果 p : Prop 是任何命题，Lean 将 t1 t2 : p 看作定义相等，它们除了 p 是真的这一事实之外，没有其他信息。

定理（Theorem）

定理（Theorem） 是一个已经被证明为真的命题。
在Lean中，定理是通过构造一个证明来定义的。定理的证明是一个类型为命题的函数，它展示了命题为真的证据。

variable {p : Prop}
variable {q : Prop}-- 对 p → q → p 的证明，假设 p 和 q 为真，并使用第一个假设(平凡地)建立结论 p 为真
-- hp : p 读作 hp  是 p 的证明
theorem t1 : p → q → p := fun hp : p => fun hq : q => hptheorem t2 (hp: p) (hq : q) :p := hp-- 定义一个定理 t1，对于命题 p和 q，可通过 `fun {p q} hp hq => hp` 证明 `p → q → p` 命题是成立的
#print t1 -- theorem t1 : ∀ {p q : Prop}, p → q → p := fun {p q} hp hq => hp-- show 语句明确指定最后一个项 hp 的类型
theorem t3 : p → q → p :=fun hp : p =>fun hq : q =>show p from hp

axiom 声明一个公理

variable {p : Prop}
variable {q : Prop}-- t1: p → q → p
theorem t1 (hp : p) (hq : q) : p := hp-- 声明「公理」hp : p 等同于声明 p 为真
axiom hp : p-- 应用定理 t1 : p → q → p 到事实 hp : p（也就是 p 为真）得到定理 t1 hp : q → p。
theorem t2 : q → p := t1 hp

example 命令声明了一个没有名字也不会永久保存的定理。本质上，它只是检查给定项是否具有指定的类型。

variable (p q : Prop)-- 表达式And.intro h1 h2 是 p ∧ q 的证明
example (hp : p) (hq : q) : p ∧ q := And.intro hp hq
example (h : p ∧ q) : p := And.left h
example (h : p ∧ q) : q := And.right h

sorry 命令声明一个缺失证明的临时占位符（Lean会警告）用于保持语法结构正确。

variable (p q r : Prop)--  ∧ 和 ∨ 的交换律
example : p ∧ q ↔ q ∧ p := sorry
example : p ∨ q ↔ q ∨ p := sorry

组合命题

variable (p q r s : Prop)theorem t2 (h₁ : q → r) (h₂ : p → q) : p → r :=fun h₃ : p =>show r from h₁ (h₂ h₃)

have 关键字用于引入一个新的局部假设或结论。使用 have 可以在证明中声明一个中间步骤，这个步骤可以在后续的证明中被引用。

variable (p q : Prop)example (h : p ∧ q) : q ∧ p :=have hp : p := h.lefthave hq : q := h.rightshow q ∧ p from And.intro hq hp-- suffices: 足以说明某某
example (h : p ∧ q) : q ∧ p :=have hp : p := h.leftsuffices hq : q from And.intro hq hpshow q from And.right h

费马大定理：当整数n>2时，不存在三个正整数x、y、z满足方程xⁿ+yⁿ=zⁿ

-- 声明一个命题
def FermatLastTheorem :=∀ x y z n : Nat, n > 2 ∧ x * y * z ≠ 0 → x ^ n + y ^ n ≠ z ^ n-- 未证明的定理：构造一个 叫 hard 的 FermatLastTheorem  类型的定理，但未给出证明（使用 sorry 是作弊）
theorem hard : FermatLastTheorem :=sorry#check hard

费马大定理 （Fermat’s Last Theorem）是数学史上的著名未解问题，由法国数学家 皮埃尔·德·费马 （Pierre de Fermat）于1637年提出。
该命题长期困扰数学家，直至1994年由英国数学家 安德鲁·怀尔斯 （Andrew Wiles）通过 椭圆曲线 和 模形式 等现代数学工具完成严格证明。 ‌
怀尔斯的证明融合了 伽罗瓦理论 、 代数几何 等多个数学分支的理论，最终确认当n>2时，上述方程无正整数解。这一证明被视为现代数学发展的重要里程碑

量词

全称量词 ∀ x : α, p x 表示，对于每一个 x : α，p x 成立（p x 表示断言 p 在 x 上成立。）。

对于 p : α → Prop，给定 x : α， p x 表示断言 p 在 x 上成立。

对于 r : α → α → Prop ，给定 x y : α，r x y 表示断言 x 与 y 相关。

计算式证明
个计算式证明是指一串使用诸如等式的 传递性等基本规则 得到的中间结果。计算式证明从关键字 calc 开始，语法如下：

-- 每个 <proof>_i 是 <expr>_{i-1} op_i <expr>_i 的证明
calc<expr>_0  'op_1'  <expr>_1  ':='  <proof>_1'_'       'op_2'  <expr>_2  ':='  <proof>_2...'_'       'op_n'  <expr>_n  ':='  <proof>_n

variable (a b c d e : Nat)theorem T(h1 : a = b)(h2 : b = c + 1)(h3 : c = d)(h4 : e = 1 + d) :a = e :=calca = b      := h1_ = c + 1  := h2_ = d + 1  := congrArg Nat.succ h3_ = 1 + d  := Nat.add_comm d 1_ = e      := Eq.symm h4-- T 等价于 T2
theorem T2(h1 : a = b)(h2 : b = c + 1)(h3 : c = d)(h4 : e = 1 + d) :a = e :=calca = b      := h1b = c + 1  := h2c + 1 = d + 1  := congrArg Nat.succ h3d + 1 = 1 + d  := Nat.add_comm d 11 + d = e      := Eq.symm h4

下划线 _ 作为占位符，告诉 Lean 该参数是隐式的，应该自动填充。

策略

构建证明的方法有两种

• 「项式」(term-style)证明：
• 「策略式」(tactic-style)证明

我们将把由策略序列组成的证明描述为 「策略式」(tactic-style)证明，前面的证明我们称为 「项式」(term-style)证明，每种风格都有自己的优点和缺点。例如，项式证明可能更难读，因为它们要求读者预测或猜测每条指令的结果。但它们一般更短，更容易写。此外，策略提供了一个使用 Lean 自动化的途径，因为自动化程序本身就是策略。

策略（Tactic），证明通常使用策略（Tactic）来编写，而非直接提供证据。策略是为命题构建证据的小程序。

要使用策略编写证明，请以 by 开始定义。编写 by 会将 Lean 置于策略模式，直到下一个缩进块的末尾。

theorem onePlusOneIsTwo : 1 + 1 = 2 := bysimp

simp 策略，即「化简（Simplify）」的缩写，是 Lean 证明的主力。它将目标重写为尽可能简单的形式，处理足够小的证明部分。特别是，它用于证明简单的相等陈述。

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := byapply And.introexact hpapply And.introexact hqexact hp

apply 策略应用于一个表达式，被视为表示一个有零或多个参数的函数。
在上面的例子中，命令 apply And.intro 产生了两个子目标：

    case leftp q : Prophp : phq : q⊢ pcase rightp q : Prophp : phq : q⊢ q ∧ p

第一个目标是通过 exact hp 命令来实现的。exact 命令只是 apply 的一个变体，它表示所给的表达式应该准确地填充目标。