第2章基础 - 深度伴读

本章定位

第2章是”动手”章节，核心目标是掌握：

rw 重写（等式证明的基石）

calc 计算链（结构化证明）

ring 自动化（代数恒等式）

apply/exact（定理应用）

本章分为三节，从具体计算逐步过渡到抽象代数。

2.1 Calculating

核心思想

计算就是证明。每一步计算都需要理由，Lean 会强制你给出。

rw 战术：重写

rw 是最基本的证明工具，工作原理：

当前目标：a * b * c = b * (a * c)
    ↓
rw [mul_comm a b]  -- 用 a*b = b*a 替换
    ↓
新目标：b * a * c = b * (a * c)
    ↓
rw [mul_assoc b a c]  -- 用 b*a*c = b*(a*c) 替换
    ↓
目标解决！

mul_comm 和 mul_assoc 是什么？

mul_comm a b 是定理 a * b = b * a（乘法交换律）

mul_assoc a b c 是定理 a * b * c = a * (b * c)（乘法结合律）

这些是 Lean 中已注册的引理，可直接在 rw 中使用

rw 的三种用法

-- 1. 完全指定参数
rw [mul_comm a b]      -- 只替换涉及 a 和 b 的项
 
-- 2. 部分指定
rw [mul_comm a]        -- 匹配 a * ? → ? * a
 
-- 3. 不指定
rw [mul_comm]          -- 自动匹配第一个找到的模式

反向重写

rw [← mul_assoc] 中的 ← 表示反向使用等式。如果 mul_assoc : a * b * c = a * (b * c)，那么 rw [← mul_assoc] 会把 a * (b * c) 替换成 a * b * c。

注意：← 是关于等式方向，不是关于目标的左右边！

多重重写

-- 可以一次写多个重写
rw [h', ← mul_assoc, h, mul_assoc]
-- 等价于依次执行四个 rw

在假设中重写

rw [hyp'] at hyp   -- 在假设 hyp 中重写，不改变目标

何时用 at

当你需要先改造假设，再用改造后的假设证明目标时

典型模式：rw [...] at hyp → exact hyp

Goal 窗口解读

1 goal
x y : ℕ,          -- 变量
h₁ : Prime x,     -- 假设
h₂ : ¬Even x,
h₃ : y > x
⊢ y ≥ 4           -- 目标（需要证明的东西）

关键符号：

⊢ 表示”需要证明”
假设可以是等式、不等式、否定等任何命题
变量和假设都有名字，可以在证明中引用

calc 证明链

calc 让你写出结构化的计算步骤：

variable (a b : ℝ)
 
example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
  calc
    (a + b) * (a + b) = a * a + b * a + (a * b + b * b) := by
      rw [mul_add, add_mul, add_mul]
    -- mul_add : (a + b) * c = a * c + b * c
    -- add_mul : a * (b + c) = a * b + a * c
    _ = a * a + (b * a + a * b) + b * b := by
      rw [← add_assoc, add_assoc (a * a)]
    -- add_assoc : (x + y) + z = x + (y + z)，调整括号位置
    _ = a * a + 2 * (a * b) + b * b := by
      rw [mul_comm b a, ← two_mul]
    -- mul_comm b a : b * a = a * b
    -- two_mul : 2 * x = x + x，所以 a * b + a * b = 2 * (a * b)

calc 的语法要点

开头不写 by：calc 本身是一个证明项，不是 tactic

下划线 _：表示”上一行的右边”

对齐很重要：Lean 用缩进来判断结构

每步都要有 := 和证明

calc 的调试技巧

先用 sorry 占位，确保骨架正确：

calc
  lhs = step1 := by sorry
  _ = step2 := by sorry
  _ = rhs := by sorry

确认 Lean 接受后，再逐个填充证明。

ring 战术：自动代数

ring 能自动证明交换环中的恒等式：

example : c * b * a = b * (a * c) := by ring
example : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by ring

ring 的限制
只处理纯代数恒等式

不能使用局部假设（context 中的 h）

只适用于交换环（CommRing）

如果需要使用假设，先 rw 再 ring：
variable (a b c d : ℝ)
 
example (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := by
  rw [hyp, hyp']   -- 代入 c 和 b：d*a + a*d = 2*a*d
  ring             -- 自动整理

nth_rw：指定位置重写

当表达式中有多个相同子表达式时：

example (a b c : ℕ) (h : a + b = c) : (a + b) * (a + b) = a * c + b * c := by
  nth_rw 2 [h]   -- 只替换第二个 (a + b)
  rw [add_mul]

2.2 Proving Identities in Algebraic Structures

核心思想

从具体（ℝ）到抽象（Ring）。Lean 的强大之处在于泛化推理。

环的公理

variable (R : Type*) [Ring R]
 
-- 加法公理
#check (add_assoc : ∀ a b c : R, a + b + c = a + (b + c))
#check (add_comm : ∀ a b : R, a + b = b + a)
#check (zero_add : ∀ a : R, 0 + a = a)
#check (neg_add_cancel : ∀ a : R, -a + a = 0)
 
-- 乘法公理
#check (mul_assoc : ∀ a b c : R, a * b * c = a * (b * c))
#check (mul_one : ∀ a : R, a * 1 = a)
#check (one_mul : ∀ a : R, 1 * a = a)
 
-- 分配律
#check (mul_add : ∀ a b c : R, a * (b + c) = a * b + a * c)
#check (add_mul : ∀ a b c : R, (a + b) * c = a * c + b * c)

泛化的力量

-- 在任意交换环中成立
variable (R : Type*) [CommRing R]
example (a b : R) : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by ring
 
-- 自动适用于 ℤ, ℚ, ℂ, 矩阵环等
-- CommRing 的实例：ℤ, ℚ, ℂ
-- Ring 但非 CommRing 的实例：n×n 矩阵

namespace 的使用

namespace MyRing
  -- 在这里定义的定理全名是 MyRing.xxx
  theorem my_lemma : ... := by ...
end MyRing
 
-- 出了 namespace，用全名访问
#check MyRing.my_lemma

为什么用 namespace

避免和 Mathlib 中已有的定理名冲突。在练习中，你可以用 namespace 标记”这是我自己的版本”。

have 战术：分解证明

-- add_left_cancel：若 a + b = a + c，则 b = c（加法消去律）
#check (add_left_cancel : a + b = a + c → b = c)
 
theorem mul_zero (a : R) : a * 0 = 0 := by
  have h : a * 0 + a * 0 = a * 0 + 0 := by
    rw [← mul_add, add_zero, add_zero]
  rw [add_left_cancel h]  -- 消去两边的 a * 0，得 a * 0 = 0

工作流程：

have h : P := by ... 引入一个新目标 P
在缩进块中证明 P
证明完成后，h 可以作为假设使用
回到原来的证明

have 的使用场景

当直接证明目标太难时，先证明一个中间结论

当需要复用某个事实时

让证明更模块化和可读

隐式参数

-- 花括号表示隐式参数
theorem add_left_cancel {a b c : R} (h : a + b = a + c) : b = c := by ...
 
-- 使用时不需要提供 a, b, c
add_left_cancel h   -- Lean 从 h 的类型推断出 a, b, c

隐式 vs 显式

(a : R) 显式：调用时必须提供

{a : R} 隐式：Lean 自动推断

选择原则：如果参数能从其他参数推断，就用隐式

rfl：定义相等

-- 在 ℝ 上，减法定义为加负数
example (a b : ℝ) : a - b = a + -b := rfl
 
-- rfl 能证明"定义上相等"的等式
-- Lean 会展开定义检查两边是否相同

2.3 Using Theorems and Lemmas

核心思想

不只是等式，不等式、蕴含、存在都需要 apply 和 exact。

apply vs exact

先看两个核心定理的含义：

#check (le_refl : ∀ a, a ≤ a)              -- ≤ 的自反性：任何数 ≤ 自己
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)  -- ≤ 的传递性

exact 用于直接提供完整证明，apply 用于匹配结论、拆分目标：

variable (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z)
 
-- exact：提供的项完全匹配目标，直接关闭
example : x ≤ x := by exact le_refl x  -- le_refl x 的类型正好是 x ≤ x
 
-- apply：匹配结论，剩余前提成为新目标
example : x ≤ z := by
  apply le_trans      -- le_trans 的结论是 a ≤ c，匹配 x ≤ z
                      -- 剩余两个前提 a ≤ b 和 b ≤ c 成为子目标
  · exact h₀          -- 证明 x ≤ y
  · exact h₁          -- 证明 y ≤ z

战术	行为	使用场景
`exact`	完全匹配，直接关闭目标	你有完整的证明
`apply`	匹配结论，剩余成新目标	需要分步证明

圆点 `·` 聚焦

apply le_trans
· apply h₀    -- 聚焦第一个目标
· apply h₁    -- 聚焦第二个目标

圆点让当前块只看到一个目标，提高可读性。

常用不等式定理

#check (le_refl : ∀ a, a ≤ a)                    -- a ≤ a
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)        -- 传递性
#check (lt_of_le_of_lt : a ≤ b → b < c → a < c)  -- 混合传递
#check (lt_trans : a < b → b < c → a < c)         -- < 传递性

add_le_add：加法保持不等式

-- add_le_add：若 a ≤ b 且 c ≤ d，则 a + c ≤ b + d
#check (add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d)
 
variable (a b c : ℝ) (h : b ≤ c)
 
example : a + Real.exp b ≤ a + Real.exp c := by
  apply add_le_add (le_refl a)  -- a ≤ a 来自自反性
  apply Real.exp_le_exp.mpr     -- exp 单调增：b ≤ c ↔ exp b ≤ exp c
  exact h

.mp 和 .mpr

对于双蕴含 P ↔ Q：

.mp 是 P → Q（正向）

.mpr 是 Q → P（反向）

类似地，对于等式 a = b：

Eq.symm 是 b = a

本章核心 Tactic 总结

Tactic	用途	示例
`rw`	重写目标	`rw [mul_comm a b]`
`rw ... at h`	重写假设	`rw [h'] at hyp`
`←`	反向重写	`rw [← mul_assoc]`
`calc`	计算链	见上文
`ring`	自动代数	`ring`
`apply`	应用定理	`apply le_trans`
`exact`	精确匹配	`exact le_refl x`
`have`	中间结论	`have h : P := by ...`
`·`	聚焦目标	见上文
`nth_rw`	指定位置重写	`nth_rw 2 [h]`

本章练习策略

必做练习

rw 基础：用 rw 证明 c * b * a = b * (a * c)
calc 练习：用 calc 证明 (a + b) * (c + d) = ...
have 分解：证明 mul_zero 和 zero_mul
不等式：用 apply le_trans 证明传递性

练习技巧

遇到卡住的练习

先用 sorry 占位，确保类型正确

用 #check 查看定理的类型

用 _ 让 Lean 提示缺失的部分

查看 solutions/ 目录对比

预告：第3章会学到什么

第3章进入逻辑层面：

intro 引入假设
apply 应用蕴含
constructor 分解合取
rcases 模式匹配
use 提供存在见证

自测问题

rw 和 calc 各自适合什么场景？

ring 能使用局部假设吗？为什么？

apply 和 exact 有什么区别？

隐式参数 {a} 和显式参数 (a) 有什么区别？

伴读文档 - 第2章完

我的博客

探索

Ch2 基础 - 深度伴读

第2章基础 - 深度伴读

2.1 Calculating

rw 战术：重写

rw 的三种用法

多重重写

在假设中重写

Goal 窗口解读

calc 证明链

calc 的调试技巧

ring 战术：自动代数

nth_rw：指定位置重写

2.2 Proving Identities in Algebraic Structures

环的公理

泛化的力量

namespace 的使用

have 战术：分解证明

隐式参数

rfl：定义相等

2.3 Using Theorems and Lemmas

apply vs exact

圆点 `·` 聚焦

常用不等式定理

add_le_add：加法保持不等式

本章核心 Tactic 总结

本章练习策略

必做练习

练习技巧

预告：第3章会学到什么

关系图谱

目录

反向链接

我的博客

探索

Ch2 基础 - 深度伴读

第2章 基础 - 深度伴读

2.1 Calculating

rw 战术：重写

rw 的三种用法

多重重写

在假设中重写

Goal 窗口解读

calc 证明链

calc 的调试技巧

ring 战术：自动代数

nth_rw：指定位置重写

2.2 Proving Identities in Algebraic Structures

环的公理

泛化的力量

namespace 的使用

have 战术：分解证明

隐式参数

rfl：定义相等

2.3 Using Theorems and Lemmas

apply vs exact

圆点 · 聚焦

常用不等式定理

add_le_add：加法保持不等式

本章核心 Tactic 总结

本章练习策略

必做练习

练习技巧

预告：第3章会学到什么

关系图谱

目录

反向链接

第2章基础 - 深度伴读

圆点 `·` 聚焦