10.2.1. 基本用法🔗

linarith 证明有序域（LinearOrderedField 或 LinearOrderedCommRing）上的线性不等式：

-- 最简单的情况：假设的线性组合直接蕴含目标
example (x y : ℝ) (h1 : x ≤ 3) (h2 : y ≤ 4) : x + y ≤ 7 := by
  linarith
  -- ▶ 取 1 * h1 + 1 * h2 得 x + y ≤ 7

-- 传递性：linarith 自动串联不等式链
example (a b c : ℝ) (h1 : a < b) (h2 : b ≤ c) (h3 : c < 0) : a < 0 := by
  linarith
  -- ▶ 从 a < b ≤ c < 0 得 a < 0

-- 等式也可以：linarith 把 = 拆成 ≤ 和 ≥
example (x : ℝ) (h : x = 5) : x ≤ 10 := by
  linarith

10.2.2. 内部原理：Farkas 引理🔗

linarith 的核心是 Farkas 引理：一组线性不等式无解，当且仅当存在非负系数的线性组合导出 0 < 0。

具体流程：

1. 否定目标加入假设：要证 a ≤ b，假设 a > b

2. 收集线性假设：从 context 中提取形如 c₁x₁ + c₂x₂ + … ≤ k 的假设

3. 搜索非负系数 λᵢ ≥ 0，使得 Σ λᵢ · (假设ᵢ) 化简为 0 < 0

4. 构造证明项：把找到的组合翻译成 Lean 证明

示例推导：假设集 {x ≤ 3, y ≤ 4, x + y > 7}
取 λ₁ = 1, λ₂ = 1：
  1·(x ≤ 3) + 1·(y ≤ 4) 得 x + y ≤ 7
  与 x + y > 7 矛盾 → 0 < 0 ✓

预处理步骤：① 严格不等式 a < b 转为 b - a > 0；② norm_num 化简具体数值；③ 展开 max/min。

10.2.3. 带额外提示🔗

当 context 中的假设不够时，可以手动传入引理：

example (x y : ℝ) (h : x + y = 10) : x ≤ 10 - y := by
  linarith [h]
  -- ▶ 方括号中的项被加入假设集

10.2.4. 失败模式🔗

失败 1：非线性项

example (x : ℝ) (h : x ≥ 2) : x ^ 2 ≥ 4 := by
  linarith  -- ✗ x ^ 2 不是 x 的线性函数
  -- 修复：nlinarith [sq_nonneg (x - 2)]

失败 2：类型不支持

example (n : ℕ) (h : n ≥ 1) : n + 1 ≥ 2 := by
  linarith  -- ✗ ℕ 不是有序域
  -- 修复：omega

工作规则：遇到 ℕ 或 ℤ 上的线性算术目标，优先尝试 omega 而非 linarith。omega 原生支持自然数减法截断等语义，而 linarith 要求有序域结构。

失败 3：假设不可见

-- 如果关键假设藏在结构体字段中，linarith 看不到
-- 需要先 obtain 解构或手动传入方括号

10.3.1. 基本用法🔗

nlinarith 处理多项式不等式。核心策略：生成假设的乘积项，然后调用 linarith。

-- 平方非负
example (x : ℝ) : x ^ 2 ≥ 0 := by
  nlinarith [sq_nonneg x]
  -- ▶ sq_nonneg x 提供 x ^ 2 ≥ 0 作为假设

-- AM-GM 的特殊情况
example (x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) :
    x * y ≤ (x ^ 2 + y ^ 2) / 2 := by
  nlinarith [sq_nonneg (x - y)]
  -- ▶ (x - y)² ≥ 0 展开为 x² - 2xy + y² ≥ 0
  --   即 x² + y² ≥ 2xy，除以 2 得结论

10.3.2. 内部原理：Positivstellensatz🔗

Positivstellensatz：若多项式 p 在 g₁ ≥ 0, …, gₘ ≥ 0 定义的半代数集上严格正，则 p 可写成平方和多项式与约束多项式乘积之和。

nlinarith 的简化实现：

1. 把假设记为 h₁, …, hₙ（各自 ≥ 0 或 > 0）

2. 枚举乘积：生成 hᵢ · hⱼ、hᵢ² 等二次乘积

3. 把这些乘积作为新假设加入集合

4. 对增广后的假设集调用 linarith

10.3.3. 提供手动提示🔗

默认只枚举二次乘积。更复杂的不等式需要手动提示：

-- 三次不等式：默认枚举不到
example (x : ℝ) (hx : x ≥ 1) : x ^ 3 ≥ x := by
  nlinarith [sq_nonneg x, sq_nonneg (x - 1), mul_self_nonneg (x - 1)]

-- 多变量：ab ≤ 1/4 当 a+b ≤ 1
example (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) :
    a * b ≤ 1 / 4 := by
  nlinarith [sq_nonneg (a - b), sq_nonneg (a + b - 1)]

10.3.4. 失败模式🔗

失败 1：乘积阶数过高

example (x : ℝ) (hx : x ≥ 2) : x ^ 4 ≥ 16 := by
  nlinarith  -- ✗ 默认只枚举二次乘积
  -- 修复：nlinarith [sq_nonneg (x^2 - 4), sq_nonneg x, sq_nonneg (x - 2)]

失败 2：搜索空间爆炸

n 个假设产生 O(n²) 个乘积。超过 ~8 个假设时性能下降。应对：用 nlinarith [具体提示] 跳过枚举，或先 have 推导中间不等式。

失败 3：除法 / 分式

example (x : ℝ) (hx : x > 0) : 1 / x > 0 := by
  nlinarith  -- ✗ 不理解除法语义
  -- 修复：positivity 或 exact div_pos one_pos hx

10.4.1. 基本用法🔗

polyrith 用 Gröbner 基方法证明多项式等式，调用外部 Sage 服务器计算系数，生成 linear_combination 证明。

example (x y : ℚ) (h1 : x + y = 3) (h2 : x - y = 1) : x = 2 := by
  polyrith
  -- ▶ 输出：linear_combination (1/2) * h1 + (1/2) * h2

example (x y : ℚ) (h1 : x + y = 3) (h2 : x * y = 2) :
    x ^ 2 + y ^ 2 = 5 := by
  polyrith
  -- ▶ x² + y² = (x+y)² - 2xy = 9 - 4 = 5

10.4.2. 内部原理：Gröbner 基🔗

工作流程：

1. 编码：把假设 hᵢ : pᵢ = 0 和目标 q = 0 编码为理想成员问题 q ∈ ⟨p₁, …, pₙ⟩

2. 调用 Sage：计算系数 cᵢ 使得 q = Σ cᵢ pᵢ

3. 生成证明：输出 linear_combination c₁ * h₁ + c₂ * h₂ + …

4. 本地验证：linear_combination 内部用 ring 验证

关键：外部求解器只发现系数，证明由 Lean 本地验证，正确性不依赖 Sage。

10.4.3. 替换为 linear_combination🔗

polyrith 成功后会打印 linear_combination 调用。强烈建议替换：

-- 替换前（需要网络）
example (a b : ℚ) (h : a + b = 4) : 2 * a + 2 * b = 8 := by polyrith
-- 替换后（纯本地，编译更快，CI 不会因 Sage 不可用而失败）
example (a b : ℚ) (h : a + b = 4) : 2 * a + 2 * b = 8 := by
  linear_combination 2 * h

10.4.4. 失败模式🔗

失败 1：无网络 — CI 或离线环境直接失败。先本地运行记录输出。

失败 2：不等式 — polyrith 只处理等式，不等式用 linarith/nlinarith。

失败 3：非 ℚ 系数 — Gröbner 基在 ℚ 上精确，ℝ 上可能找不到系数。

失败 4：高次多变量 — Gröbner 基最坏双指数复杂度，可能超时。

10.5.1. 决策树🔗

目标类型？
├─ 等式
│  ├─ 纯代数恒等式（无假设） → ring
│  ├─ 需要假设推导 → polyrith → 替换为 linear_combination
│  └─ ℤ / ℕ → omega 或 ring
│
└─ 不等式 / 序关系
   ├─ 线性（无乘积项）
   │  ├─ ℝ / ℚ → linarith
   │  └─ ℤ / ℕ → omega
   │
   └─ 非线性（有乘积 / 幂次）
      ├─ 仅需证非负 → positivity
      └─ 一般不等式 → nlinarith [提示]
         └─ 仍然失败 → 手动 have + nlinarith

10.5.2. 与 omega 的边界🔗

omega 处理 Presburger 算术（ℤ/ℕ 线性算术），linarith 处理有序域线性算术（ℝ/ℚ）。

example (n : ℕ) (h : n ≥ 3) : n + 1 ≥ 4 := by omega     -- ℕ → omega
example (x : ℝ) (h : x ≥ 3) : x + 1 ≥ 4 := by linarith  -- ℝ → linarith

10.6.1. 组合使用🔗

example (x y : ℝ) (hx : x ≥ 0) (hy : y ≥ 0) (hsum : x + y = 1) :
    x ^ 2 + y ^ 2 ≥ 1 / 2 := by
  nlinarith [sq_nonneg (x - y), hsum]
  -- ▶ (x-y)² ≥ 0 → x²-2xy+y² ≥ 0
  --   结合 x+y=1 得 x²+y² ≥ 1/2

10.6.2. 调试失败的 linarith🔗

诊断步骤：① 检查目标是否线性；② 检查假设是否在 context 中；③ 手动提供缺失假设。

下面是一个示意型 debug 场景——绝对值本身已超出 linarith 的直接适用范围，这里展示的是"拆解后再调用"的 debug 思路：

-- 示意：|x| 不是线性项，需要先拆成分支再用 linarith
example (x : ℝ) (h : |x| ≤ 1) : -1 ≤ x := by
  linarith  -- ✗ 不理解绝对值
  -- 修复：先拆开绝对值，让每个分支变成线性目标
  cases abs_cases x with
- inl h' => linarith [h'.1, h'.2]：inr h' => linarith [h'.1, h'.2]

10.6.3. 在 meta 编程中调用🔗

-- 依次尝试多个算术 tactic
macro "auto_ineq" : tactic =>
  `(tactic| first | linarith | nlinarith | positivity | omega)