14.1.1. Prop 与 Bool 的桥梁🔗

Decidable 连接 Prop 世界和 Bool 世界：

-- [签名] 核心库关键定义
#check @Decidable.decide  -- {p : Prop} → [Decidable p] → Bool  -- ❶ 命题 → 布尔
-- of_decide_eq_true : decide p = true → p               -- ❷ 布尔真 → 命题真

• ❶ 把命题"降级"为布尔值，供 if / match 使用。

• ❷ 若内核规约 decide p 到 true，rfl 即证 decide p = true， 再经 of_decide_eq_true rfl 得到 p 的证明——这正是 decide tactic 的核心。

14.3.1. 失败 1：缺少 Decidable 实例🔗

-- [会报错] p 是任意命题，无法合成实例
-- example (p : Prop) : p ∨ ¬p := by decide
--   -- ▸ failed to synthesize Decidable (p ∨ ¬p)
--   -- ▸ 修复：用 Classical.em p，或为 p 提供 Decidable 实例

p ∨ ¬p 在经典逻辑中成立（Classical.em），但 decide 只处理构造性可判定的命题。

14.3.2. 失败 2：内核超时（计算量过大）🔗

-- [会超时] 内核解释器需要试除到 √1000003 ≈ 1000
-- example : Nat.Prime 1000003 := by decide
--   -- ▸ 修复：改用 native_decide 或 norm_num

经验法则：decide 不宜超过几万步 reduction，超过应换 tactic。

14.3.3. 失败 3：命题为假🔗

-- [会报错] 4 不是质数
-- example : Nat.Prime 4 := by decide
--   -- ▸ decide evaluated to false
--   -- ▸ 这不是 tactic 的问题，而是命题本身不成立

decide 只能证明为真的可判定命题。报告 evaluated to false 本身是有用的诊断。

14.3.4. 失败 4：目标含自由变量🔗

-- [会报错] n 不是字面量，无法规约
-- example (h : n = 3) : n + 1 = 4 := by decide
--   -- ▸ decide 只做封闭项（closed term）的计算
--   -- ▸ 修复：先 subst h 消除 n，再 decide
-- example (h : n = 3) : n + 1 = 4 := by subst h; decide  -- ✓

14.3.5. 失败 5：实例存在但计算量不可行🔗

-- [会超时] 实例存在 ≠ 计算可行
-- example : (Finset.range 10000).card = 10000 := by decide
--   -- ▸ 修复：native_decide 或 simp [Finset.card_range]

14.4.1. 可信度代价🔗

decide 的证明完全在内核中完成，可信边界仅限于 Lean kernel 本身。 native_decide 则依赖编译器将判定过程编译为原生代码再执行—— 如果编译器存在 bug（错误优化、代码生成缺陷），理论上可能把 实际为 false 的计算"证明"为 true。因此 native_decide 的可信边界 比 decide 更宽：它信任的不仅是内核，还有编译执行路径。

Mathlib 策略：能用 decide 就不用 native_decide， 能用 norm_num / omega 等专用 tactic 就优先使用。

14.4.2. native_decide 的失败模式🔗

-- [会报错] 同样需要 Decidable 实例
-- example (p : Prop) : p ∨ ¬p := by native_decide
--   -- ▸ failed to synthesize Decidable (p ∨ ¬p)

-- [会报错] 命题为假
-- example : Nat.Prime 4 := by native_decide
--   -- ▸ native_decide evaluated to false

-- [会报错] 代码链中含 sorry 或 partial 导致编译失败
-- partial def foo : Nat → Bool := fun _ => true
-- instance : Decidable P := if foo 0 then .isTrue sorry else .isFalse sorry
-- example : P := by native_decide  -- failed to compile

native_decide 不能绕过 Decidable 的要求，也不能证明假命题。 包含 sorry 或 partial 的代码链会导致编译失败。

14.5.1. 方式 1：deriving 自动派生🔗

• ❶ 结构体、枚举、带参数的归纳类型都支持 deriving DecidableEq。

14.5.2. 方式 2：dependent if 手动构造🔗

• ❶ if h : cond 是 dependent if——分支中 h 分别绑定 cond 和 ¬cond。

• ❷ 正分支利用库引理构造整除证明。❸ 负分支推出矛盾。

14.5.3. 方式 3：归约到已有可判定命题🔗

• ❶ inferInstanceAs 告诉 typeclass search IsEven n 就是 n % 2 = 0。

14.5.4. 方式 4：组合逻辑连接词🔗

Decidable 对逻辑连接词封闭——p ∧ q、p ∨ q、¬p、p → q 在两侧可判定时自动可判定。对有限量词 ∀ x : α, P x 和 ∃ x : α, P x， 需要 α 是 Fintype 且 P 对每个 x 可判定：

14.6.1. 选择速查表🔗

• 场景：小规模有限穷举（< 100 种） —— 推荐 tactic：decide —— 原因：内核可信，无额外假设

• 场景：大规模有限穷举（> 100 种） —— 推荐 tactic：native_decide —— 原因：编译执行，快几个数量级

• 场景：Nat/Int 线性算术 —— 推荐 tactic：omega —— 原因：专用 decision procedure

• 场景：具体数值计算、素性、整除 —— 推荐 tactic：norm_num —— 原因：meta 层高效归约 + 证书

• 场景：含变量的等式 / 不等式 —— 推荐 tactic：simp / ring / linarith —— 原因：符号化简

14.7.1. 模式 1：有限案例验证🔗

14.7.2. 模式 2：interval_cases + decide 联用🔗

14.7.3. 模式 3：在 have 中建立局部事实🔗

14.7.4. 调试技巧 1：用 #eval 预判🔗

-- #eval Nat.Prime 7          -- true  → decide 应能证明
-- #eval Nat.Prime 1000003    -- true  → 但 decide 会超时，用 native_decide
#eval (4 : Nat) ∣ 6        -- false → decide 会失败（命题为假）

先 #eval 确认真假和计算量，再选 tactic。

14.7.5. 调试技巧 2：检查实例 + 调整心跳🔗

#check (inferInstance : Decidable (3 < 5))      -- OK
#check (inferInstance : DecidableEq Color)      -- 报错则需 deriving 或手写

-- set_option maxHeartbeats 400000 in
-- example : Nat.Prime 997 := by decide
--   -- ▸ 默认 200000，可临时提高；若需大幅增加，应换 tactic

14.8.1. 练习 1（基础）：decide 能证什么🔗

判断以下哪些能用 decide 证明，不能的说明原因并给出替代方案：

example : 10 * 10 = 100 := by sorry              -- (a) 基础算术
-- example : ¬ Nat.Prime 15 := by sorry              -- (b) 否定命题
example (n : Nat) : n + 0 = n := by sorry         -- (c) 含自由变量
example : ∀ b : Bool, b && true = b := by sorry   -- (d) Bool 穷举
-- example : Nat.Prime 104729 := by sorry             -- (e) 大素数

提示：(a)(b)(d) 直接 decide；(c) 含变量用 simp；(e) 超时用 native_decide 或 norm_num。

14.8.2. 练习 2（编写实例）：自定义 Decidable🔗

def IsPalindrome (l : List Char) : Prop := l = l.reverse
instance (l : List Char) : Decidable (IsPalindrome l) := sorry
-- 验证
-- example : IsPalindrome ['a', 'b', 'a'] := by decide
-- example : ¬ IsPalindrome ['a', 'b', 'c'] := by decide

提示：用 inferInstanceAs (Decidable (l = l.reverse)) 归约到 DecidableEq。

14.8.3. 练习 3（性能选择）：为每题选择最合适的 tactic🔗

-- example : Nat.Prime 10007 := by sorry             -- (a) 大素数
example : ∀ n : Nat, n < n + 1 := by sorry        -- (b) 全称线性不等式
example : ∀ a b : Fin 4, a * b = b * a := by sorry -- (c) 有限穷举
example : (3 : ℤ) ^ 5 = 243 := by sorry           -- (d) 数值幂运算

提示：(a) norm_num；(b) omega；(c) decide；(d) norm_num。

14.8.4. 练习 4（调试）：修复失败的 decide🔗

-- (a) 为什么超时？给出两种修复方案。
-- example : Nat.Prime 1000003 := by decide
-- (b) 为什么失败？只改 tactic 前面的代码。
-- example (h : n = 5) : n + 1 = 6 := by decide

提示：(a) 换 native_decide 或 norm_num；(b) 在 decide 前加 subst h;。

14.8.5. 练习 5（进阶）：组合判定实例🔗

def InRange (lo hi n : Nat) : Prop := lo ≤ n ∧ n < hi
instance (lo hi n : Nat) : Decidable (InRange lo hi n) := sorry
-- 验证
-- example : InRange 3 10 5 := by decide
-- example : ¬ InRange 3 10 2 := by decide

提示：展开后是 lo ≤ n ∧ n < hi，用 inferInstanceAs 归约到 And 的组合实例。