15.2.1. 组合规则🔗

• 操作：a + b —— Pos × Pos：Pos —— Pos × Nn：Pos —— Nn × Nn：Nn —— 备注：一侧为正即拉正

• 操作：a * b —— Pos × Pos：Pos —— Pos × Nn：Nn —— Nn × Nn：Nn —— 备注：需两侧均正才保正

• 一元操作：a ^ n（偶数） —— 输出：Nn —— 条件：无条件

• 一元操作：a ^ n（奇数） —— 输出：保持输入 —— 条件：需输入 Nn 或 Pos

• 一元操作：\ —— 输出：a\ —— 条件：、‖a‖、sqrt —— Nn —— 无条件

• 一元操作：exp a —— 输出：Pos —— 条件：无条件

15.3.1. 假设扫描🔗

递归分解前，positivity 自动扫描上下文假设：

识别的假设形式：0 < x → Positive，0 ≤ x → Nonneg，x ≠ 0 → Nonzero。

15.4.1. 基本算术🔗

• ❶ 偶数幂总是非负，不需要任何假设。

• ❷ 奇数幂保持符号，需要参数非负的假设。

15.4.2. 分析函数🔗

• ❶ Real.exp 返回 Positive（不只是 Nonneg），这是正确的数学性质。

15.4.3. 类型转换与除法🔗

15.4.4. 有限求和🔗

15.5.1. 扩展自定义函数🔗

-- [示意] 为自定义函数注册 positivity 插件
noncomputable def myNorm (x : ℝ) : ℝ := x ^ 2 + 1
lemma myNorm_pos (x : ℝ) : 0 < myNorm x := by unfold myNorm; positivity

@[positivity myNorm _]
def evalMyNorm : Positivity.PositivityExt where
  eval {u α} _zα _pα e := do
    let .app (.const ``myNorm _) a := e | throwError "not myNorm"
    return .positive (← mkAppM ``myNorm_pos #[a])

注册后，positivity 能自动处理包含 myNorm 的表达式。

15.6.1. 失败 1：目标形式不对🔗

-- [会报错] positivity 只接受 0 ≤ e 或 0 < e 形式
example (a b : ℝ) (ha : 0 ≤ a) (hab : a ≤ b) : a ≤ b := by positivity
  -- ▸ positivity failed: the goal is not of the form `0 ≤ _` or `0 < _`
  -- ▸ 修复：这不是符号判定问题，用 exact hab 或 linarith

positivity 不做一般不等式推理——它只回答"这个表达式相对于零的符号是什么"。

15.6.2. 失败 2：缺少假设 / 奇数幂🔗

-- [会报错] x 的符号未知
example (x : ℝ) : 0 ≤ x := by positivity
  -- ▸ 修复：需要假设 (hx : 0 ≤ x)

-- [会报错] 奇数幂不自动非负（偶数幂 x^2、x^4 无条件非负）
example (x : ℝ) : 0 ≤ x ^ 3 := by positivity
  -- ▸ 修复：添加 (hx : 0 ≤ x)

15.6.3. 失败 4：减法🔗

-- [会报错] 减法破坏符号推理
example (a b : ℝ) (ha : 0 ≤ a) : 0 ≤ a - b := by positivity
  -- ▸ 修复：需要 b ≤ a 的假设，或改用 linarith

a ≥ 0 不保证 a - b ≥ 0。positivity 需要上下文中有 0 ≤ a - b 等直接假设。

15.6.4. 失败 5：不认识的函数🔗

-- [会报错] 自定义函数没有注册插件
noncomputable def myFunc (x : ℝ) : ℝ := x ^ 2 + 1
example (x : ℝ) : 0 < myFunc x := by positivity
  -- ▸ positivity failed: ...
  -- ▸ 修复：先 unfold myFunc，再 positivity
example (x : ℝ) : 0 < myFunc x := by unfold myFunc; positivity  -- ✓

positivity 不会自动展开定义。要么先 unfold，要么注册 @[positivity] 插件。

15.6.5. 失败 6：表达式可能为零🔗

-- [会报错] x² 在 x=0 时为零，无法证 ≠ 0
example (x : ℝ) : x ^ 2 ≠ 0 := by positivity
  -- ▸ 修复：需要 (hx : x ≠ 0)
example (x : ℝ) (hx : x ≠ 0) : x ^ 2 ≠ 0 := by positivity  -- ✓

15.7.1. 模式 1：为 gcongr 提供侧目标🔗

• ❶ gcongr 需要底数非负。❷ positivity 从 ha 直接收尾。

15.7.2. 模式 2：为 field_simp 准备分母非零🔗

15.7.3. 选择速查表🔗

• 场景：0 ≤ e 或 0 < e，结构化表达式 —— 推荐 tactic：positivity —— 原因：递归分解，利用代数结构

• 场景：0 ≤ e 或 0 < e，纯数值 —— 推荐 tactic：norm_num —— 原因：直接计算

• 场景：a ≤ b 一般不等式 —— 推荐 tactic：linarith / gcongr —— 原因：线性推理或单调性

• 场景：分母 ≠ 0 —— 推荐 tactic：positivity（若可推出为正） —— 原因：0 < e → e ≠ 0

• 场景：乘积 / 除法符号 —— 推荐 tactic：positivity —— 原因：组合规则直接适用

15.8.1. 技巧 1：用 positivity? 查看证明项🔗

positivity? 输出具体的证明项，可用于理解推理过程或替换为显式证明。

15.8.2. 技巧 2：逐步分解定位失败🔗

-- [示意] 定位失败位置
example (x : ℝ) (hx : 0 < x) : 0 < (x - 1) * x := by
  -- positivity 失败——哪个子表达式有问题？
  -- have h1 : 0 < x := hx           -- ✓ x 为正
  -- have h2 : 0 < x - 1 := ???      -- ✗ x-1 可能为负！
  -- 原因：x > 0 不保证 x - 1 > 0
  sorry

15.8.3. 技巧 3：添加中间假设🔗

• ❶❷ 用 linarith 建立中间事实，让 positivity 能从上下文读取符号信息。

15.9.1. 练习 1（基础）：判断 positivity 能否成功🔗

判断以下哪些能被 positivity 证明，不能的说明原因：

example (x : ℝ) : 0 ≤ x ^ 2 := by sorry                    -- (a)
example (x : ℝ) : 0 ≤ x := by sorry                         -- (b)
example (x : ℝ) : 0 < Real.exp x := by sorry                -- (c)
example (a b : ℝ) (ha : 0 ≤ a) : 0 ≤ a - b := by sorry     -- (d)
example (x : ℝ) (hx : x ≠ 0) : 0 < |x| := by sorry         -- (e)

提示：(a) 偶数幂无条件非负 ✓；(b) 缺假设 ✗；(c) exp 总为正 ✓； (d) 减法需要更多信息 ✗；(e) 非零的绝对值为正 ✓。

15.9.2. 练习 2（组合推理）：多步符号分析🔗

example (a b : ℝ) (ha : 0 < a) (hb : 0 ≤ b) : 0 < a ^ 2 + a * b + 1 := by
  sorry

提示：positivity 直接可用——a² Positive, a*b Nonneg, 1 Positive。

15.9.3. 练习 3（修复失败）：补充假设让 positivity 成功🔗

-- 添加最弱的假设使 positivity 成功
example (x y : ℝ) /- 补充假设 -/ : 0 < x * y := by positivity

提示：需要 (hx : 0 < x) (hy : 0 < y) 或 (hx : x < 0) (hy : y < 0)。 positivity 只处理第一种（两个 Positive 的乘积）。

15.9.4. 练习 4（unfold 技巧）：处理自定义函数🔗

noncomputable def energy (v : ℝ) (m : ℝ) : ℝ := m * v ^ 2 / 2

example (v : ℝ) (m : ℝ) (hm : 0 < m) : 0 ≤ energy v m := by
  sorry

提示：先 unfold energy，再 positivity。

15.9.5. 练习 5（实战）：为 gcongr 提供侧目标🔗

example (x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) (hxy : x ≤ y) :
    x ^ 3 ≤ y ^ 3 := by
  sorry

提示：gcongr 会产生 0 ≤ x 等侧目标，用 positivity 或 assumption 收尾。

15.9.6. 练习 6（进阶）：分段证明🔗

example (x : ℝ) (hx : 2 ≤ x) : 0 < x ^ 2 - x := by
  sorry

提示：positivity 直接失败（减法）。用 have : 0 < x * (x - 1) := by ... 建立中间事实，或用 nlinarith。