在形式化方法系列的前几篇中，从类型论基础（01）、目标窗口与 tactic 交互模型（02）到 Gallina 核心语法（03）、基础 tactic 全景（04）以及搜索与自动化（05），关注点始终落在"如何与 Lean 的类型检查器对话"。本篇收窄焦点：当证明目标是算术命题时，四个专用 tactic 各自覆盖哪个数学域，各自在哪里失效。

这不是一个"哪个 tactic 更强"的比较，而是四个具有严格数学边界的决策过程的并排描述。选错工具只会让证明永远挂起或留下 sorry，而不会神奇地奏效。

omega：Presburger 算术的完备决策器

覆盖范围

omega 实现了 Presburger 算术（Presburger arithmetic）的完备决策过程。Presburger 算术是一阶逻辑中关于自然数和整数的理论，限定以下运算：

  • 加减法（+、-）
  • 整数常量乘法（n * x 其中 n 是字面整数）
  • 整除与取模（%、/）
  • 比较运算（<、≤、=、≠）

对 Nat 和 Int 类型的线性整数命题，omega 要么给出证明，要么报告不可满足——它是完备的，不需要提示，也不会猜测。

基本用法

1
2
3
4
5
6
import Mathlib.Tactic.Omega

example (n : Nat) : n + 0 = n := by omega
example (n m : Nat) : n + m = m + n := by omega
example (x : Int) : x - x = 0 := by omega
example (a b : Nat) (h : a ≤ b) : a + 1 ≤ b + 1 := by omega

InfoView 在 by omega 之前显示的典型目标形如：

1
⊢ a + 1 ≤ b + 1

omega 消耗掉这个目标后，InfoView 变为空（No goals），证明结束。

带假设时，omega 会自动从上下文中收集所有整数/自然数假设：

1
example (x y : Int) (h1 : x ≥ 3) (h2 : y ≥ 2) : x + y ≥ 5 := by omega

目标窗口在 omega 之前显示：

1
2
3
4
x y : Int
h1 : x ≥ 3
h2 : y ≥ 2
⊢ x + y ≥ 5

omega 调用后直接关闭目标。

omega 的边界

omega 无法处理乘法中两个变量相乘的情形（这超出了 Presburger 算术的范围）：

1
2
3
-- 这会失败：
-- example (n : Nat) : n * n ≥ n := by omega
-- error: omega could not find a proof of the following arithmetic expression ...

同样，omega 不处理实数（Real）或有理数（Rat）类型的命题——域不对。

与 decide 的关系

对于有限的命题（如 (3 : Nat) + 5 = 8），decide 和 omega 都可用。omega 的优势在于它对含变量的全称量化命题依然有效；decide 只适用于命题的可枚举实例，详见 04 篇的基础 tactic 讨论。

linarith：有序域上的线性算术

覆盖范围

linarith 处理线性算术命题，但目标类型可以是 Real、Rat、或任何满足 LinearOrderedCommRing 实例的类型。它本质上是 Farkas 引理的一个自动化实现：通过对已知假设取非负线性组合来导出矛盾或目标。

与 omega 的关键区别：

特性 omega linarith
适用类型 Nat、Int 任意有序环（含 Real）
处理整除/取模 可以 不行
完备性 对 Presburger 完备 对线性实数算术完备
处理变量积 不行 不行

基本用法

1
2
3
4
import Mathlib.Tactic.Linarith

example (x y : Real) (h1 : x > 0) (h2 : y > 0) : x + y > 0 := by linarith
example (a b c : Real) (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c := by linarith

有时 linarith 需要帮助。若目标涉及绝对值或平方，可先引入辅助引理再调用 linarith：

1
2
3
4
example (x : Real) (hx : x ≥ 0) : x ^ 2 ≥ 0 := by
  -- 直接 linarith 会失败，因为 x^2 是非线性的
  -- 改用 positivity（见下节）或 nlinarith
  positivity

linarith 的目标形状：

1
2
3
4
x y : Real
h1 : x > 0
h2 : y > 0
⊢ x + y > 0

调用 linarith 后目标关闭。linarith 内部对这一结论的处理是：假设 ¬(x + y > 0)，即 x + y ≤ 0，与 h1 : x > 0、h2 : y > 0 相加可得矛盾 0 < x + y ≤ 0。

linarith 的边界

线性的定义很严格。以下命题中任何出现变量相乘的项，linarith 都无法处理：

1
2
3
-- 以下会失败：
-- example (x : Real) : x^2 ≥ 0 := by linarith
-- example (x y : Real) : x * y ≥ 0 := by linarith  -- 即使加上 x≥0, y≥0

对非线性情形，要用 nlinarith（非线性 linarith，带有限次多项式展开）或 polyrith（见后文）。

nlinarith：linarith 的非线性延伸

nlinarith 是 linarith 的扩展，支持非线性情形，但不完备。它尝试对假设构造多项式乘积再调 linarith：

1
2
example (x : Real) : x ^ 2 ≥ 0 := by nlinarith [sq_nonneg x]
example (x y : Real) (hx : x ≥ 0) (hy : y ≥ 0) : x * y ≥ 0 := by nlinarith [mul_nonneg hx hy]

这里 [sq_nonneg x] 是给 nlinarith 的额外提示——显式地告诉它可以把 x^2 ≥ 0 加入假设集合。

positivity：非负性与正性的专用证明器

覆盖范围

positivity 专门证明"某个表达式 > 0"或"某个表达式 ≥ 0"这类形式的命题。它的工作方式是递归地检查表达式的语法结构，利用已知的非负性引理组合出结论：

  • 非负常量 → 直接成立
  • 两个非负项之和 → 非负
  • 两个非负项之积 → 非负
  • 绝对值、偶次幂 → 非负
  • 平方根（Real.sqrt）→ 非负

基本用法

1
2
3
4
5
import Mathlib.Tactic.Positivity

example (x : Real) : x ^ 2 + 1 > 0 := by positivity
example (x y : Real) : x ^ 2 * y ^ 2 ≥ 0 := by positivity
example (n : Nat) : (n : Real) ≥ 0 := by positivity

在 InfoView 中，positivity 处理的典型目标：

1
2
x y : Real
⊢ x ^ 2 * y ^ 2 ≥ 0

调用 positivity 后目标关闭，因为 x^2 ≥ 0 和 y^2 ≥ 0 均为 sq_nonneg 的实例，乘积非负。

positivity 的边界

positivity 只能处理"结构上可以被拆解为非负部分"的表达式。以下情形它无法独立完成：

1
2
3
4
5
-- 需要假设，单靠结构推断不够：
-- example (x : Real) (hx : x > 0) : x + 1 > 0 := by positivity
-- 上面这行实际上 positivity 可以处理（常量 1 > 0 加上 x ≥ 0）
-- 但以下会失败：
-- example (x : Real) : x > 0 := by positivity  -- 没有关于 x 的信息

positivity 对变量 x 没有任何假设时，无法推断 x > 0。这类情形必须通过假设（have h : x > 0 := ...）或者其他 tactic 引入。

与 norm_num 的关系

对于纯数值表达式（无变量），norm_num 通常更合适：

1
2
example : (2 : Real) ^ 10 > 0 := by norm_num
example : (0 : Real) ≤ 3.14 := by norm_num

positivity 的核心价值在于含变量的表达式，此时 norm_num 无能为力。

polyrith：多项式算术的 oracle 证明器

覆盖范围与工作原理

polyrith 处理多项式环上的等式命题（不是不等式）。它的工作方式分两步：

  1. oracle 调用阶段：将当前目标和假设发送到外部计算代数服务（Sage/Groebner basis 计算），返回多项式系数。
  2. 验证阶段：将返回的系数代入 ring tactic，在 Lean 内完成验证。

这是四个 tactic 中唯一依赖外部服务的一个。网络不可用时，polyrith 会失败。

1
2
3
4
5
6
7
8
9
10
11
12
13
import Mathlib.Tactic.Polyrith

example (x y : Real) (h : x + y = 3) (h2 : x - y = 1) : x = 2 := by
  linarith  -- 这里 linarith 足够

-- 更复杂的多项式等式场景：
example (a b : Real) (h : a ^ 2 - b ^ 2 = 0) (h2 : a + b ≠ 0) : a = b := by
  have := h
  have key : (a + b) * (a - b) = 0 := by ring_nf; linarith
  have hfactor : a - b = 0 := by
    field_simp at key ⊢
    exact (mul_eq_zero.mp key).resolve_left h2
  linarith

polyrith 真正的使用场景是假设集合是多项式理想成员时的等式证明：

1
2
3
4
-- 典型 polyrith 场景（需要网络连接运行 oracle）：
example (x y z : Real) (h1 : x + y + z = 1) (h2 : x*y + y*z + z*x = 0)
    (h3 : x*y*z = -1) : x^3 + y^3 + z^3 = 4 := by
  polyrith

polyrith 成功时，会在 InfoView 中输出一段可重放的 linear_combination 调用，将证明固化，不再依赖网络：

1
Try this: linear_combination (...)

polyrith 的边界

polyrith 不处理不等式——这是它与 linarith/nlinarith 最鲜明的分界线。它也不处理 Nat/Int 的整除性质（整除在多项式环意义下无法直接表达）。此外，polyrith 的 oracle 可能对某些目标超时。

关于 #check 和 #print axioms 的验证用法

在确认某个引理是否存在或查看 omega 等 tactic 背后的公理依赖时，可以：

1
2
3
4
5
#check Nat.add_comm
-- Nat.add_comm : ∀ (n m : ℕ), n + m = m + n

#check Int.ediv_add_emod
-- Int.ediv_add_emod : ∀ (a b : ℤ), b * (a / b) + a % b = a

查看一个定理依赖了哪些公理：

1
2
3
theorem my_thm (n : Nat) : n + 0 = n := by omega
#print axioms my_thm
-- my_thm depends on axioms: [propext, Classical.choice, Quot.sound]

omega 的实现不引入额外公理，只用 Lean 4 的内置基础。这与 polyrith 不同——polyrith 实际上是生成一个 linear_combination 调用，后者只依赖 ring，所以公理足迹同样干净。

四个 tactic 的边界对照

一个更紧凑的视角，描述每个 tactic 在哪个"格子"里有效：

1
2
3
4
5
6
7
8
命题类型\工具      omega    linarith   positivity   polyrith
─────────────────────────────────────────────────────────
Nat/Int 线性不等式   ✓        ✓（Int）      —            —
Nat/Int 整除/取模    ✓          —           —            —
Real 线性不等式      —          ✓           —            —
Real 平方非负        —          —           ✓            —
Real 多项式非负      —       nlinarith    ✓（结构）      —
多项式等式（任意域） —          —           —            ✓

这张表的实用意义：当 omega 失败时，先看目标类型是否超出 Nat/Int；当 linarith 失败时，先看是否含有变量积（考虑 nlinarith 或 positivity）；当目标是等式且含高次项时，首选 polyrith，或先尝试 ring。

term-mode 与 tactic-mode 的对比

以 Nat.add_comm 为例，两种证明风格并列：

1
2
3
4
5
6
7
-- tactic-mode：
theorem add_comm_tac (n m : Nat) : n + m = m + n := by
  omega

-- term-mode：直接引用 Mathlib 定理
theorem add_comm_term (n m : Nat) : n + m = m + n :=
  Nat.add_comm n m

InfoView 在 tactic-mode 的 by 之后显示：

1
2
n m : Nat
⊢ n + m = m + n

omega 执行后目标清空。term-mode 版本则跳过了 InfoView，直接构造了证明项，因为 Nat.add_comm 的类型精确匹配目标。

对于 linarith 涉及实数的场景，term-mode 对应的写法通常需要借助具名引理，略显冗长；tactic-mode 的 linarith 自动搜索假设的线性组合，更简洁。这是选择 tactic-mode 的主要动机之一，也是 02 篇中"goal-directed 交互模型"的典型体现。

前置系列的衔接说明

在「形式化方法」前置系列中，算术命题通常以 Prop 的形式出现，讨论语义层面的可满足性。Lean 4 的 omega/linarith 等 tactic 将这种可满足性转化为构造性证明：不只是声称命题为真，而是提交一个类型检查器可验证的证明对象。

03 篇介绍的 ring tactic 与 polyrith 有明确分工：ring 处理无假设的纯代数恒等式（环公理直接蕴含的等式），polyrith 处理依赖假设的多项式等式（通过 Groebner 基计算系数）。

常见误用与排查

对初次接触这四个 tactic 的读者，以下几种报错有固定的处理路径。

omega could not find a proof

原因通常是目标含实数或含两变量之积。先用 #check @my_var 确认类型，再换 linarith。

linarith failed to find a contradiction

原因通常是目标非线性。用 nlinarith 并酌情添加乘积提示，如 nlinarith [mul_self_nonneg x]。

positivity failed

表示 positivity 无法从表达式结构推断非负性——通常是缺少关于变量符号的假设。先用 have 引入必要假设，再调 positivity。

polyrith 无输出或超时

网络问题或目标不在多项式理想中。先尝试 ring（无假设恒等式）或 linear_combination（手工指定系数）。

练习一：omega 的应用边界

给定以下命题，判断 omega 能否证明，并给出能证明的部分的完整 Lean 4 代码：

1
2
3
(a) ∀ n : Nat, 2 * n + 1 ≠ 2 * n
(b) ∀ x : Int, x % 2 = 0 ∨ x % 2 = 1
(c) ∀ x : Real, x + x = 2 * x

提示：© 的类型是 Real，考虑哪个 tactic 更合适。

练习二：linarith 与 nlinarith 的选择

证明以下命题，不使用 sorry，选择合适的 tactic 并解释为何 linarith 单独不够：

1
2
example (x y : Real) (hx : x ≥ 1) (hy : y ≥ 1) : x * y ≥ 1 := by
  ???

提示：观察 x * y - 1 = (x - 1) * y + (y - 1) 并考虑是否可以将乘积项作为提示传递给 nlinarith。

练习三：综合使用与边界探查

以下定理需要结合多个 tactic。给出完整的无 sorry 证明，并在每步注释中说明选择该 tactic 的原因：

1
2
3
4
5
-- 目标：对任意实数 a, b，有 a^2 + b^2 ≥ 2*a*b
example (a b : Real) : a ^ 2 + b ^ 2 ≥ 2 * a * b := by
  ???
  -- 提示一：a^2 + b^2 - 2*a*b = (a - b)^2 ≥ 0
  -- 提示二：考虑 nlinarith 配合 sq_nonneg (a - b)

如果改写为等价形式 a^2 + b^2 - 2*a*b ≥ 0，再尝试 positivity，会发生什么？解释结果。

参考资料

  • Mathlib4 文档：omega、linarith、positivity、polyrith
  • Lean 4 官方文档：Theorem Proving in Lean 4
  • Cooper, D. C. (1972). Theorem Proving in Arithmetic without Multiplication. — Presburger 算术决策过程的原始论文背景
  • Lasserre, J. B. (2001). Global Optimization with Polynomials and the Problem of Moments. — polyrith 背后的代数几何动机