16.1.1. 历史背景🔗

在 fun_prop 之前，Mathlib 有独立的 continuity（连续性）和 measurability（可测性）tactic， 各自维护规则集。fun_prop 将它们统一为一个框架：

• ❶❷ 旧 tactic 目前仍然可用，但其内部实现和兼容性可能随版本变化。 新代码应统一使用 fun_prop。

注意：fun_prop 是 tactic（在 by 后使用），不是 term-level 常量。

16.2.1. 四步流程🔗

1. 识别目标类型：检查目标是否形如 P f（Continuous、Differentiable ℝ、Measurable 等）

2. 函数分解：把 f 拆成基本函数的组合——识别 lambda 结构、复合、算术运算

3. 规则搜索：在 @[fun_prop] 引理库中查找匹配规则

4. 递归证明：对每个子函数递归执行步骤 1–3

16.2.2. 分解过程详解🔗

以 Continuous (fun x : ℝ => Real.exp (x ^ 2 + 1)) 为例：

目标: Continuous (fun x => exp (x ^ 2 + 1))

第一层: 复合 exp ∘ (fun x => x ^ 2 + 1)
├── 外层: exp
│   └── Real.continuous_exp → ✓                     -- ❶
├── 内层: fun x => x ^ 2 + 1
│   第二层: 加法 (·) + (·)
│   ├── 左: fun x => x ^ 2
│   │   ├── 底: fun x => x → continuous_id → ✓     -- ❷
│   │   └── Continuous.pow → ✓                      -- ❸
│   ├── 右: fun _ => 1 → continuous_const → ✓       -- ❹
│   └── Continuous.add → ✓                          -- ❺
└── Continuous.comp → ✓                             -- ❻

• ❶ exp 连续是已注册的基本事实。❷❸ 恒等函数连续，连续函数的幂连续。

• ❹ 常数函数连续。❺ 连续函数之和连续。❻ 复合规则组合最终证明。

16.2.3. Lambda 分解：与 aesop 的核心区别🔗

fun_prop 的核心能力是理解 lambda 表达式的结构—— 识别 fun x => f (g x) 是 f ∘ g，fun x => f x + g x 是逐点加法。 aesop 是通用搜索，不理解函数组合的特殊结构，因此通常无法处理这类目标。

16.3.1. 支持的性质🔗

fun_prop 不硬编码特定性质，通过引理注册支持任意性质。 Mathlib 中已注册的主要性质包括： Continuous、Differentiable ℝ、Measurable、AEMeasurable、 AEStronglyMeasurable、LipschitzWith K 等。

16.4.1. 失败 1：性质未注册🔗

-- [会报错] 自定义性质没有 fun_prop 引理
def MySmooth (f : ℝ → ℝ) : Prop := Continuous f ∧ Differentiable ℝ f

example : MySmooth (fun x : ℝ => x ^ 2) := by fun_prop
  -- ▸ fun_prop failed: MySmooth 不是已注册的函数性质
  -- ▸ 修复：分别证明两个分量
example : MySmooth (fun x : ℝ => x ^ 2) := by
  exact ⟨by fun_prop, by fun_prop⟩

16.4.2. 失败 2：自定义函数未展开🔗

-- [会报错] fun_prop 不自动展开定义
noncomputable def mySpecialFun (x : ℝ) : ℝ := Real.exp (Real.sin x)

example : Continuous (fun x : ℝ => mySpecialFun x + 1) := by fun_prop
  -- ▸ 修复方案 1：先 unfold
example : Continuous (fun x : ℝ => mySpecialFun x + 1) := by
  unfold mySpecialFun; fun_prop                            -- ❶

-- ▸ 修复方案 2：一次性注册引理（更好）
-- @[fun_prop]
-- theorem continuous_mySpecialFun : Continuous mySpecialFun := by
--   unfold mySpecialFun; fun_prop                         -- ❷

• ❶ unfold 暴露内部结构。❷ 注册后以后都不用 unfold。

16.4.3. 失败 3：侧目标无法自动解决🔗

-- [会报错] 除法需要分母非零，fun_prop 无法自动证明
example : Continuous (fun x : ℝ => 1 / x) := by fun_prop
  -- ▸ 产生侧目标 ∀ x, x ≠ 0，但无法证明
  -- ▸ 修复：限制定义域或用 disch 提供条件

16.4.4. 失败 4：非 lambda 形式🔗

-- [会报错] Function.comp 形式不易分解
example : Continuous (Function.comp Real.exp Real.sin) := by fun_prop
  -- ▸ 修复：用 show 转换为 lambda 形式
example : Continuous (Function.comp Real.exp Real.sin) := by
  show Continuous (fun x => Real.exp (Real.sin x))         -- ❶
  fun_prop

• ❶ fun_prop 针对 fun x => ... 优化，show / change 可帮助转换。

16.4.5. 失败 5：性质间依赖🔗

-- [示意] fun_prop 不自动利用 "Differentiable 蕴含 Continuous" 的关系
-- 自定义性质中要注意：只注册了 P 的引理，不会自动推出蕴含的性质 Q

16.5.1. 技巧 1：trace 查看搜索过程🔗

set_option trace.Meta.Tactic.fun_prop true in
example : Continuous (fun x : ℝ => x ^ 2 + 1) := by fun_prop

trace 输出显示每一步分解和规则匹配：

[Meta.Tactic.fun_prop] Continuous (fun x => x ^ 2 + 1)
  [Meta.Tactic.fun_prop] Continuous (fun x => x ^ 2)      -- ❶
    [Meta.Tactic.fun_prop] Continuous (fun x => x)         -- ❷
    [Meta.Tactic.fun_prop] ✓ continuous_id
  [Meta.Tactic.fun_prop] Continuous (fun _ => 1)           -- ❸
    [Meta.Tactic.fun_prop] ✓ continuous_const
  [Meta.Tactic.fun_prop] ✓ Continuous.add

• ❶ 分解加法左侧。❷ 分解幂的底数。❸ 分解加法右侧。

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

-- [示意] 大表达式失败时，拆开逐个测试
example : Continuous (fun x : ℝ => Real.exp (1 / Real.sin x)) := by
  -- fun_prop 失败——拆开定位：
  -- have h1 : Continuous Real.exp := by fun_prop                 -- ✓
  -- have h2 : Continuous (fun x => 1 / Real.sin x) := by fun_prop  -- ✗
  -- 原因：sin x 可能为零，除法需要分母非零条件
  sorry

16.5.3. 技巧 3：unfold + show 暴露结构🔗

16.6.1. 模式 1：disch 处理侧目标🔗

fun_prop 的 disch 参数指定侧目标处理策略：

• ❶ disch 告诉 fun_prop：遇到侧目标时用指定 tactic 解决。

16.6.2. 模式 2：simp 化简后收尾🔗

16.6.3. 模式 3：分析证明中的组合链🔗

16.6.4. 选择速查表🔗

• 场景：Continuous f、Differentiable ℝ f 等 —— 推荐 tactic：fun_prop —— 原因：专门为此设计

• 场景：连续性 + 旧代码兼容 —— 推荐 tactic：continuity —— 原因：目前仍可用，兼容性可能变化

• 场景：0 ≤ e 或 0 < e —— 推荐 tactic：positivity —— 原因：符号判定，不是函数性质

• 场景：分母 ≠ 0 作为侧目标 —— 推荐 tactic：positivity / norm_num —— 原因：与 disch 配合

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

example : Continuous (fun x : ℝ => x ^ 2 + 1) := by sorry          -- (a)
example : Continuous (fun x : ℝ => 1 / x) := by sorry              -- (b)
example : Differentiable ℝ (fun x : ℝ => Real.exp x) := by sorry   -- (c)
example : Continuous (fun x : ℝ => if x > 0 then x else 0) := by sorry  -- (d)
example : Measurable (fun x : ℝ => x * 3 + 2) := by sorry          -- (e)

提示：(a) 多项式 ✓；(b) 分母可能为零 ✗；(c) exp 可微 ✓； (d) 分段函数不是标准组合结构 ✗；(e) 线性函数可测 ✓。

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

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

example (m : ℝ) : Continuous (kinetic_energy m) := by
  sorry

提示：先 unfold kinetic_energy，再 fun_prop。

16.8.3. 练习 3（组合推理）：嵌套复合🔗

example : Continuous (fun x : ℝ => Real.exp (Real.sin x + Real.cos x)) := by
  sorry

提示：fun_prop 直接可用——逐层分解复合结构。

16.8.4. 练习 4（修复失败）：补充条件🔗

-- 添加缺少的假设使 fun_prop 成功
example (f : ℝ → ℝ) : Continuous (fun x => f x + x) := by fun_prop

提示：需要假设 (hf : Continuous f)。fun_prop 不能凭空得知 f 连续。

16.8.5. 练习 5（disch）：处理侧目标🔗

example (x : ℝ) (hx : x > 0) :
    DifferentiableAt ℝ (fun y : ℝ => Real.log y) x := by
  sorry

提示：fun_prop (disch := linarith) 或 先 have : x ≠ 0 := by linarith 再 fun_prop (disch := assumption)。

16.8.6. 练习 6（实战）：分母非零🔗

example : Continuous (fun x : ℝ => (Real.exp x - 1) / Real.exp x) := by
  sorry

提示：分母 exp x > 0 恒成立。 尝试 fun_prop (disch := positivity)。