Some content in this article was created with AI assistance. Please verify as needed.

mathlib 为数值计算、多项式、线性不等式和离散算术分别提供了专用 tactic。使用前先判断目标属于哪套理论；连续试命令通常只会掩盖缺少的前提或转换步骤。

1
import Mathlib

数值类型与代数自动化

常见数系

Lean 类型 数学对象 备注
ℕ / Nat 自然数 减法截断到零
ℤ / Int 整数 可使用负数
ℚ / Rat 有理数 精确分数
ℝ / Real 实数 非可计算的数学实数
ℂ / Complex 复数 实部、虚部为实数

同一个字面量会根据上下文解释：

1
2
3
4
#check (2 : ℕ)
#check (2 : ℤ)
#check (2 : ℚ)
#check (2 : ℝ)

自然数减法尤其需要注意：

1
2
#eval (3 - 5 : Nat) -- 0
#eval (3 - 5 : Int) -- -2

若证明需要普通环中的减法，过早停留在 Nat 往往会增加额外分类讨论。

norm_num

norm_num 处理具体数值计算和简单数值不等式：

1
2
3
4
5
6
7
8
example : (123 : ℤ) + 456 = 579 := by
  norm_num

example : (3 : ℝ) / 4 < 1 := by
  norm_num

example : Nat.Prime 97 := by
  norm_num

它不是通用代数求解器。目标中有大量变量时，应考虑 ring 或 linarith。

ring

ring 证明交换半环或交换环中的多项式恒等式：

1
2
example (x y : ℝ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
  ring

ring_nf 把目标和前提正规化，而不是只尝试关闭目标：

1
2
3
example (x y : ℚ) (h : x + y = 10) : 2 * x + 2 * y = 20 := by
  ring_nf at h ⊢
  linarith

ring 不会使用不等式前提，也不会自动处理除以变量的表达式。

linarith

linarith 组合线性等式和不等式：

1
2
3
4
5
example (x y : ℝ) (h1 : x ≤ y) (h2 : y < 10) : x < 10 := by
  linarith

example (x y : ℝ) (h : x + y = 7) : 2 * x + 2 * y = 14 := by
  linarith

如果表达式包含变量相乘或平方，线性算法通常不够。

nlinarith

nlinarith 在正规化多项式以后处理非线性算术：

1
2
3
4
5
example (x : ℝ) : x ^ 2 + 1 > 0 := by
  nlinarith [sq_nonneg x]

example (x : ℝ) (h : x ^ 2 = 4) (hx : 0 ≤ x) : x = 2 := by
  nlinarith

它擅长由有限个多项式约束推出结论，但不会自动使用任意分析定理，也不适合包含超越函数的目标。

field_simp

field_simp 清除分母，并要求分母非零：

1
2
example (x : ℝ) (hx : x ≠ 0) : (x + 1) / x = 1 + 1 / x := by
  field_simp [hx]

纸面上的“同乘分母”省略了一个前提：分母必须非零。field_simp 会把这项前提保留为证明义务。

复杂目标通常先 field_simp，再用 ring：

1
2
3
4
example (x y : ℝ) (hx : x ≠ 0) (hy : y ≠ 0) :
    1 / x + 1 / y = (x + y) / (x * y) := by
  field_simp [hx, hy]
  ring

positivity

positivity 根据表达式结构自动证明非负或正性：

1
2
3
4
5
example (x : ℝ) : 0 ≤ x ^ 2 + 1 := by
  positivity

example (a b : ℝ) (ha : 0 < a) (hb : 0 < b) : 0 < a * b := by
  positivity

它适合为除法、乘法、平方根等定理准备边界条件。

omega

omega 处理自然数和整数上的 Presburger 算术，包括线性关系、离散边界和一部分取模问题：

1
2
3
4
5
example (m n : Nat) (h1 : m ≤ n) (h2 : n ≤ m) : m = n := by
  omega

example (n : Nat) (h : n < 3) : n = 0 ∨ n = 1 ∨ n = 2 := by
  omega

它可以理解自然数减法的截断语义，这类目标往往比强行转换到实数再 linarith 更适合 omega。

类型转换

数系之间的强制转换写成 (n : ℤ) 或 (x : ℝ)。转换后的等式经常可以用 norm_cast 整理：

1
2
example (m n : Nat) (h : (m : ℤ) < (n : ℤ)) : m < n := by
  exact_mod_cast h

常用工具的区别：

  • norm_cast：规范化目标或前提中的强制转换；
  • exact_mod_cast h：允许适当转换后用 h 精确完成目标；
  • push_cast：把转换推进加法、乘法等运算内部。

选择顺序

一个实用的判断顺序是：

  1. 纯具体数字：norm_num；
  2. 多项式恒等式：ring；
  3. 线性等式或不等式：linarith；
  4. 非线性多项式约束：nlinarith；
  5. 自然数、整数离散线性算术：omega；
  6. 含变量分母：先证明非零，再 field_simp；
  7. 正性旁支：positivity。

自动化失败时，先把数学问题转换成 tactic 能识别的正规形式，而不是连续叠加更多自动化。

函数、集合与有限结构

数学中的函数、集合和有限集合在 mathlib 中是三套相关但不同的接口。Set α 表示性质，Finset α 表示可计算的有限集合，Fintype α 表示整个类型只有有限多个值。

1
2
open Set
open scoped BigOperators

函数的性质

Lean 函数写成 α → β。mathlib 中最常见的性质包括：

1
2
3
4
5
#check Function.Injective
#check Function.Surjective
#check Function.Bijective
#check Function.LeftInverse
#check Function.RightInverse

单射和满射的定义可以直接按逻辑结构证明：

1
2
3
4
5
6
7
8
example : Function.Injective (fun n : Nat => n + 1) := by
  intro a b h
  exact Nat.add_right_cancel h

example : Function.Surjective (fun x : Int => x + 1) := by
  intro y
  use y - 1
  ring

函数复合使用 Function.comp 或记号 ∘：

1
#check fun x : Nat => (toString ∘ Nat.succ) x

Set 是谓词

Set α 在定义上接近 α → Prop，成员关系 x ∈ s 就是性质 s x：

1
2
3
4
def evens : Set Nat := {n | n % 2 = 0}

example : 4 ∈ evens := by
  norm_num [evens]

输入 ∈、∩、∪ 可以使用 \in、\inter、\union。对应的命名写法是 Membership.mem、Set.inter、Set.union；对集合而言，x ∈ s 还可以直接理解为 s x。命名形式便于查 API，符号形式更能保留集合表达式的结构。

常见集合构造：

1
2
3
4
5
#check (Set.univ : Set Nat)
#check (∅ : Set Nat)
#check evens ∩ {n | n ≤ 10}
#check evens ∪ {1, 3, 5}
#check evensᶜ

集合运算会通过 simp 展开为逻辑连接词：

1
2
3
4
5
6
example (s t : Set Nat) (x : Nat) : x ∈ s ∩ t ↔ x ∈ s ∧ x ∈ t := by
  rfl

example (s t : Set Nat) : s ∩ t = t ∩ s := by
  ext x
  simp [and_comm]

子集

s ⊆ t 表示所有 s 的元素也属于 t：

1
2
3
example (s t u : Set Nat) (hst : s ⊆ t) (htu : t ⊆ u) : s ⊆ u := by
  intro x hx
  exact htu (hst hx)

集合相等通常使用双向包含或 ext：

1
2
example (s t : Set Nat) (hst : s ⊆ t) (hts : t ⊆ s) : s = t := by
  exact Set.Subset.antisymm hst hts

像与原像

函数 f : α → β 的原像和像分别写成：

1
2
3
4
5
6
7
8
section

variable {α β : Type} (f : α → β) (s : Set α) (t : Set β)

#check f ⁻¹' t
#check f '' s

end

原像的成员关系只需计算，通常 rfl 或 simp 就能处理：

1
2
3
example (f : Nat → Nat) (t : Set Nat) (x : Nat) :
    x ∈ f ⁻¹' t ↔ f x ∈ t := by
  rfl

像包含一个存在量词，因为需要找到原来的元素：

1
2
3
example (f : Nat → Nat) (s : Set Nat) (y : Nat) :
    y ∈ f '' s ↔ ∃ x, x ∈ s ∧ f x = y := by
  rfl

区间

mathlib 提供统一的区间名称：

记号 含义
Icc a b $[a,b]$
Ioc a b $(a,b]$
Ico a b $[a,b)$
Ioo a b $(a,b)$
Ici a / Iic b 单侧闭区间
Ioi a / Iio b 单侧开区间 
1
2
example (x : ℝ) : x ∈ Icc 0 1 ↔ 0 ≤ x ∧ x ≤ 1 := by
  rfl

Finset

Finset α 是无重复的有限集合，需要可判定相等实例才能执行许多操作：

1
2
3
4
5
def small : Finset Nat := {1, 2, 3}

#eval small.card
#eval ∑ n ∈ small, n
#eval small.filter (fun n => n % 2 == 1)

Finset.range n 包含 0 到 n - 1：

1
2
3
4
#eval Finset.range 5

example (n : Nat) : (Finset.range n).card = n := by
  simp

有限求和使用大运算记号：

1
2
example (n : Nat) : (Finset.range n).sum (fun _ => 1) = n := by
  simp

Fintype 与 Fin

Fintype α 是“α 的所有值可以枚举”的类型类，Finset.univ 表示所有元素：

1
2
3
4
#eval (Finset.univ : Finset Bool)

example : (Finset.univ : Finset Bool).card = 2 := by
  decide

Fin n 表示严格小于 n 的自然数，值同时携带边界证明：

1
2
3
def index : Fin 3 := ⟨1, by omega⟩

#eval index.val

数组、矩阵和有限维向量经常使用 Fin n 作为安全索引。

归纳法

自然数归纳的基本结构如下：

1
2
3
4
example (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ n ih => simp [ih]

列表归纳按空列表和 x :: xs 分支：

1
2
3
4
example (xs : List Nat) : xs.reverse.reverse = xs := by
  induction xs with
  | nil => rfl
  | cons x xs ih => simp

归纳假设只对结构上更小的对象成立。遇到递归定义时，选择与定义递归参数相同的对象做归纳，通常能让化简规则直接对齐。

数系与强制转换的原理

数系层级

纸面上常写：

$$
\mathbb N\subset\mathbb Z\subset\mathbb Q\subset\mathbb R\subset\mathbb C.
$$

在 Lean 中这些是不同类型，不是同一个运行时对象带不同子类标签。包含关系通过显式或隐式的映射表达：

1
2
#check (Nat.cast : Nat → Int)
#check (Int.cast : Int → Rat)

实际代码通常直接写强制转换：

1
2
example (n : Nat) : (n : Int) ≥ 0 := by
  omega

不同类型独立存在有现实原因：

  • Nat 的减法截断；
  • Int 有负数但没有一般除法域结构；
  • Rat 可精确计算；
  • Real 是完备有序域，但不是普通可执行浮点数；
  • Complex 没有与域运算兼容的线性序。

若像 Python 那样在运行时自动提升对象，表达式容易写，但定理的精确适用结构会被隐藏。mathlib 选择显式结构和 coercion，让类型检查器记录在哪个数系中推理。

Real 与 Float

Float 是 IEEE 风格的机器浮点数，用于执行近似计算；ℝ 是数学实数，用于证明。

1
2
3
4
#eval (0.1 + 0.2 : Float)

example : (1 : ℝ) / 10 + 2 / 10 = 3 / 10 := by
  norm_num

实数包含任意精度数学对象，通常不可直接 #eval。把 Real 当作“更高精度 Float”会误解其构造和计算模型。

形式化数值算法时常分两层：

  1. 在 ℝ 等数学结构中证明理想算法性质；
  2. 单独分析浮点实现的舍入误差、溢出和可执行性。

纸面数学经常无意中混合这两层，Lean 的类型差异会迫使作者说明。

Nat 减法

自然数没有负数，因此：

1
#eval (3 - 5 : Nat)

得到 0。这导致普通环恒等式在 Nat 上不成立：

1
a - b + b = a

只有在 b ≤ a 时成立。

证明中有三种策略：

  • 保留 Nat，显式维护大小关系，使用 omega；
  • 尽早转换到 Int，使用环运算；
  • 重写目标，避免不必要的减法。

应根据问题本质选择。计数、长度和下标天然是 Nat；包含大量代数移项的论证通常在 Int/Rat/Real 中更顺畅。

自动化 tactic 的原理

tactic 的适用范围

几个算术 tactic 并不是“不同强度的同一个 AI”，而是面向不同理论的决策或正规化过程：

tactic 主要对象 典型限制
norm_num 具体数值表达式 不解决一般变量关系
ring 交换半环/环中的多项式恒等式 不使用序关系
linarith 线性有序环上的线性约束 不处理变量乘变量
nlinarith 多项式等式与不等式 不理解任意函数
omega Nat/Int Presburger 算术 不处理变量乘变量
positivity 表达式符号 依赖已注册正性规则
field_simp 清除域中的分母 必须提供非零条件

每个 tactic 只处理特定形式的目标。例如：

1
2
example (x : ℝ) : Real.sin x ≤ 1 := by
  exact Real.sin_le_one x

linarith 不知道正弦值域，必须先提供领域定理。得到多项式或线性约束以后，算术 tactic 才能接手。

ring 的反射思想

ring 不会盲目尝试交换律和分配律的各种排列。它把表达式反射为多项式语法，计算规范形，再生成规范形相等的证明。

概念上：

1
2
3
4
5
6
7
(x + y)^2
  ↓ reify
Pow (Add x y) 2
  ↓ normalize
x^2 + 2xy + y^2
  ↓ proof certificate
原表达式 = 规范形

因此它在大表达式上比手工 rw [mul_add, add_mul, ...] 稳定，也解释了为什么超越函数、除以变量和非交换乘法会超出它的默认能力。

类似技术称为 reflection：在 Lean 内部把一类目标转成可计算语法，再证明计算过程正确。

linarith 的前提

linarith 只看到局部上下文中的线性事实。若关键事实藏在结构字段、绝对值或函数定理中，需要先取出：

1
2
3
4
example (x y : ℝ) (hx : |x| ≤ 3) (hy : |y| ≤ 4) : x + y ≤ 7 := by
  have hx' : x ≤ 3 := le_trans (le_abs_self x) hx
  have hy' : y ≤ 4 := le_trans (le_abs_self y) hy
  linarith

linarith 不会自行展开绝对值的含义。先从绝对值界取出所需上界，再让它完成最后的线性组合。

nlinarith 的符号条件

由 $x^2\le y^2$ 推出 $x\le y$ 并不总成立，需要非负条件。Lean 会迫使这些条件出现在上下文：

1
2
3
example (x y : ℝ)
    (hx : 0 ≤ x) (hy : 0 ≤ y) (h : x ^ 2 ≤ y ^ 2) : x ≤ y := by
  nlinarith

若删去 hx 和 hy，命题本身就是假的。自动化失败有时是在揭示数学前提不足，而不是 tactic 不够强。

field_simp 的副作用

分式较多时，field_simp 会把目标变成高次多项式，并产生多个非零旁支。使用以前最好：

  1. 明确列出所有分母非零条件；
  2. 先用 rw 简化相同分母；
  3. 只在必要位置清分母；
  4. 清除后用 ring/nlinarith，不要继续把分式引回来。
1
2
3
4
example (x : ℝ) (hx : x ≠ 1) :
    (x ^ 2 - 1) / (x - 1) = x + 1 := by
  field_simp [hx]
  ring

纸面上常把约分写成一步；Lean 要求同时证明被约掉的因子不为零，这正是严格性所在。

集合与函数的表示

Set 的表示

定义上可以把：

1
Set α ≈ α → Prop

理解为“判断一个 α 是否属于集合的性质”。因此：

1
x ∈ s

就是把谓词 s 应用到 x。

交集对应逻辑合取，合集对应析取，补集对应否定：

1
2
3
4
5
6
7
example (s t : Set α) (x : α) :
    x ∈ s ∩ t ↔ x ∈ s ∧ x ∈ t := by
  rfl

example (s t : Set α) (x : α) :
    x ∈ s ∪ t ↔ x ∈ s ∨ x ∈ t := by
  rfl

这不是哈希表或平衡树的运行时集合。任意性质都能定义集合，包括不可判定、无限的性质，因此普通 Set 不提供枚举全部元素的算法。

Python set、C++ std::set 与 Lean Finset 更接近；Lean Set 更接近数学集合或逻辑谓词。

集合外延与函数外延

集合相等不是比较某个内部容器，而是成员完全相同：

1
2
3
example (s t : Set α) (h : ∀ x, x ∈ s ↔ x ∈ t) : s = t := by
  ext x
  exact h x

由于集合本质上是谓词，这也依赖函数外延：逐点结果相同的函数相等。

函数外延不是定义相等。例如两个 lambda 可能对所有输入给出相同结果，但语法和归约结构不同，需要 funext 建立命题相等。

集合像的逻辑

原像成员：

1
x ∈ f ⁻¹' t

直接化简为 f x ∈ t。像成员：

1
y ∈ f '' s

则需要证明存在 x ∈ s 使 f x = y。

因此原像保持交、并、补等结构通常很直接；像对交集只得到单向包含，除非函数单射。形式化时这些差异不会被集合图示掩盖。

1
2
3
4
example (f : α → β) (s t : Set β) :
    f ⁻¹' (s ∩ t) = f ⁻¹' s ∩ f ⁻¹' t := by
  ext x
  rfl

单射、满射与逆函数

Function.Injective f 展开为：

1
∀ ⦃a b⦄, f a = f b → a = b

Function.Surjective f 展开为：

1
∀ y, ∃ x, f x = y

左逆直接推出单射，右逆直接推出满射：

1
2
3
4
5
6
7
example (f : α → β) (g : β → α)
    (h : Function.LeftInverse g f) : Function.Injective f := by
  exact h.injective

example (f : α → β) (g : β → α)
    (h : Function.RightInverse g f) : Function.Surjective f := by
  exact h.surjective

这比直接操作“逆函数”更一般：函数不必先打包成双射结构，只要有一侧逆就能得到相应性质。

有限结构与大运算

DecidableEq

有限集合不能保存重复元素。插入新元素时必须判断它是否已经存在，因此很多 Finset 操作要求 [DecidableEq α]。

1
2
def insertTwice [DecidableEq α] (x : α) : Finset α :=
  {x, x}

数学上任意两个元素是否相等不一定可计算；经典逻辑可以非计算性地提供决定实例，但要执行 #eval 就需要真正可计算的相等判断。

List α 不去重，因此不要求可判定相等；是否允许重复正是 List 与 Finset 的关键语义差异。

Finset 与 Multiset

可以把三个容器粗略比较为：

1
2
3
List α      有顺序，允许重复
Multiset α  无顺序，允许重复
Finset α    无顺序，不允许重复

有限求和只关心每个元素出现次数而不关心顺序，底层与 multiset 很接近。集合运算则需要去重。

若证明依赖遍历顺序，应保留 List；若只关心组合计数或有限集合成员，Finset 通常更符合数学语义。

大运算

mathlib 使用统一记号表示有限和与有限积：

1
2
3
4
open scoped BigOperators

#eval ∑ n ∈ ({1, 2, 3, 4} : Finset Nat), n
#eval ∏ n ∈ ({1, 2, 3, 4} : Finset Nat), n

∑ 和 ∏ 分别由 \sum 和 \prod 输入，底层接口是 Finset.sum 和 Finset.prod。例如 ∑ n ∈ s, f n 可以逐层理解为在筛选后的 Finset 上调用 sum，但通常不必把清楚的大运算记号展开成长函数调用。

求和依赖加法交换幺半群，求积依赖乘法交换幺半群。交换性使结果不依赖 Finset 的内部枚举顺序。

常见拆分定理：

1
2
3
4
#check Finset.sum_insert
#check Finset.sum_union
#check Finset.sum_add_distrib
#check Finset.prod_insert

使用时经常需要成员不包含或集合不交等条件，这些条件正对应纸面上“没有重复计算”。

Fintype

Finset α 是一个具体有限子集；[Fintype α] 表示整个类型可枚举。

1
2
3
4
5
example : Fintype.card Bool = 2 := by
  decide

example : (Finset.univ : Finset (Fin 5)).card = 5 := by
  simp

当变量范围是一个有限类型时，可以直接写：

1
2
example : (∑ i : Fin 4, (i.val : Nat)) = 6 := by
  decide

这里的 binder 遍历 Finset.univ。矩阵行列、有限图顶点和组合对象经常以 Fintype 表达。

归纳与离散数学

自然数归纳与强归纳

普通归纳只给出 P n 作为证明 P (n+1) 的假设。强归纳则可以使用所有更小值：

1
2
3
4
example (P : Nat → Prop)
    (h : ∀ n, (∀ m < n, P m) → P n) : ∀ n, P n := by
  intro n
  exact Nat.strong_induction_on n (fun n ih => h n ih)

质因数分解、递归减去不固定大小等证明更适合强归纳。选择归纳原理应该与递归依赖关系匹配，而不是所有自然数目标都机械使用 induction n。

generalizing

归纳以前过早固定变量，可能得到太弱的归纳假设。tactic 可以把变量泛化：

1
2
3
4
5
6
example (xs ys : List α) : (xs ++ ys).length = xs.length + ys.length := by
  induction xs generalizing ys with
  | nil => simp
  | cons x xs ih =>
      simp only [List.cons_append, List.length_cons, ih]
      omega

这里对 xs 归纳时保留“任意 ys”，使归纳假设能用于递归分支中的具体尾部组合。

这种问题与程序验证中的 loop invariant 类似：假设必须足够一般，才能在下一步维持。

gcd、整除与素数

初等数论常围绕整除：

1
2
3
4
#check Dvd.dvd
#check Nat.gcd
#check Nat.Coprime
#check Nat.Prime

a ∣ b 本质上表示存在 c 使 b = a * c：

1
2
example (a b c : Nat) (hab : a ∣ b) : a ∣ b * c := by
  exact dvd_mul_of_dvd_left hab c

具体整除和素数可用 norm_num：

1
2
3
4
5
example : 7 ∣ 42 := by
  norm_num

example : Nat.Prime 101 := by
  norm_num

一般性证明则要使用整除的传递、gcd 性质和素因子定理，不应期待 norm_num 对含变量命题自动发明数论证明。

ZMod 与模运算

ZMod n 把模 $n$ 同余类组织成一个代数类型：

1
2
3
4
#eval ((10 : ZMod 7) + 5)

example : (10 : ZMod 7) + 5 = 1 := by
  decide

相比在自然数上反复写 % n，ZMod n 让加法和乘法自动在商结构中进行。若 $n$ 为素数，还能获得域结构，进而使用一般环与域定理。

mathlib 把模同余封装为等价关系，因此这里可以使用通用的等价关系定理，不必逐步操作代表元和余数。

有限组合证明的常见路线

一个计数问题通常需要在几个表示之间移动：

  1. 用 subtype 描述满足条件的对象；
  2. 为对象类型提供 Fintype；
  3. 用 Finset.univ 枚举；
  4. 建立双射或分割为不交并；
  5. 用 Fintype.card_congr、Finset.card_bij 等转换基数；
  6. 最后用有限求和或算术自动化计算。

纸面上的“显然一一对应”在 Lean 中通常对应一个显式 equivalence。虽然代码更长，但也会迫使映射、逆映射和边界条件全部明确。

综合不等式证明

单个 tactic 的例子只能说明输入和输出。较长的不等式证明还需要组织局部事实、转换否定目标、控制乘法的单调性，并在合适时机展开局部定义。

反证与否定目标

by_contra h 把目标 P 变成假设 h : ¬ P 和目标 False。若 P 是严格不等式，通常还需要把它的否定转换成反向的非严格不等式：

1
2
3
4
5
example (s : ℝ) (hs : 2 ≤ s) : 1 < s := by
  by_contra h
  have hle : s ≤ 1 := by
    exact le_of_not_gt h
  linarith

这里 le_of_not_gt 完成逻辑层的转换，linarith 才处理转换后的线性算术。不要期待算术 tactic 自动猜测证明采用反证法还是直接证明。

不等式相乘

由 a < b 不能无条件推出 a * c < b * c，还必须知道 c > 0。mathlib 将左右乘分别写成明确的定理：

1
2
3
4
5
6
7
example (a b c : ℝ) (hab : a < b) (hc : 0 < c) :
    a * c < b * c := by
  exact mul_lt_mul_of_pos_right hab hc

example (a b c : ℝ) (hab : a < b) (hc : 0 < c) :
    c * a < c * b := by
  exact mul_lt_mul_of_pos_left hab hc

两个不等式相乘时，可以分两步改变因子：

1
2
3
4
5
6
7
8
example (a b c d : ℝ)
    (hab : a < b) (hcd : c < d)
    (ha : 0 < a) (hc : 0 < c) :
    a * c < b * d := by
  have hb : 0 < b := lt_trans ha hab
  calc
    a * c < b * c := mul_lt_mul_of_pos_right hab hc
    _ < b * d := mul_lt_mul_of_pos_left hcd hb

这正是复杂不等式证明中经常需要显式写出的步骤。nlinarith 擅长多项式约束，但不会在缺少符号条件时任意相乘不等式。

局部定义

let 可以给重复出现的长表达式命名。证明局部定义的性质时，dsimp 只展开定义归约，不调用大规模重写规则：

1
2
3
4
5
example (x : ℝ) :
    let y := x + 1
    y ^ 2 - 2 * y + 1 = x ^ 2 := by
  dsimp
  ring

在较长证明中通常先声明定义，再保存相关事实：

1
2
3
4
5
6
7
example (x : ℝ) (hx : 0 < x) : 0 < 1 / (1 + x) := by
  let d := 1 + x
  have hd : 0 < d := by
    dsimp [d]
    linarith
  change 0 < 1 / d
  positivity

局部定义不会自动在所有目标中展开。需要精确控制时写 dsimp [d]、simp [d] 或 rw [show d = ... from rfl]。

平方根条件

Real.sqrt 不是多项式运算。先提供非负条件并使用平方根 API，才能把目标转换成代数约束：

1
2
3
4
5
example (x : ℝ) (hx : 0 ≤ x) : (Real.sqrt x) ^ 2 = x := by
  simpa using Real.sq_sqrt hx

example (x : ℝ) (hx : 0 < x) : Real.sqrt x ≠ 0 := by
  exact ne_of_gt (Real.sqrt_pos_of_pos hx)

simpa using h 表示先化简当前目标和事实 h 的类型，再用化简后的事实关闭目标。它适合处理记号、乘方写法或定义展开造成的小差异。

tactic 组合

分号组合符把右侧 tactic 应用于左侧产生的全部目标：

1
2
3
example (a b : ℝ) (ha : 0 < a) (hb : 0 < b) :
    0 < a ∧ 0 < b := by
  constructor <;> assumption

<;> 很适合处理完全相同的机械子目标。若各分支需要不同数学理由，使用项目符号分别书写更清楚，不应为了缩短行数强行合并。

分母条件

field_simp 清除分母以前必须获得非零证明。正性经常是最方便的来源：

1
2
3
4
5
6
example (u : ℝ) (hu : 0 < u) :
    1 - 1 / (1 + u) = u / (1 + u) := by
  have hden : 1 + u ≠ 0 := by
    exact ne_of_gt (show 0 < 1 + u by linarith)
  field_simp [hden]
  ring

这个证明同时展示了 show 对预期类型的显式说明。它不改变数学目标，只帮助 elaborator 和读者确认当前需要构造的是哪个命题。

自动化的边界

决策过程与证明搜索

decide 通过命题的 Decidable 实例计算真假并生成证明：

1
2
example : (3 : Fin 5) ≠ 4 := by
  decide

适合：

  • 小型有限枚举；
  • 具体相等比较；
  • 可计算布尔性质。

不适合：

  • 巨大搜索空间；
  • 不可计算实数命题；
  • 需要解释数学结构的核心定理。

native_decide 可以使用原生执行加速可判定目标，但仍应注意证明项生成方式、依赖公理和构建可移植性。

使用原则

处理自动化目标时可以按以下顺序排查：

  1. 先把目标转换到正确数系或结构；
  2. 展开真正需要展开的定义；
  3. 提取符号、非零、成员关系等关键事实；
  4. 用 rw/simp only 做可控规范化；
  5. 最后调用与理论匹配的 tactic；
  6. 若失败，查看剩余目标属于哪个理论，而不是继续随机试命令。

例如含平方根的题目，nlinarith 不会直接理解 Real.sqrt。应先使用平方根非负、平方等于原值等定理，把问题转成多项式约束，再交给 nlinarith。

自动化 tactic 接收的是整理后的问题。例如 nlinarith 需要多项式约束，omega 需要 Presburger 算术目标；调用之前的改写和引理往往才是证明的主要步骤。