decidable - 精益抱怨它看不到一个声明是可判定的

Question

我正在尝试定义以下数量部分：

variable pi : nat -> Prop
variable (Hdecp : ∀ p, decidable (pi p))

definition partn (n : nat) : nat := ∏ p ∈ (prime_factors n), (if pi p then p^(mult p n) else 1)

但得到错误

error: failed to synthesize placeholder
pi : ℕ → Prop,
n p : ℕ
⊢ decidable (pi p)

由于 Hdecp，我如何帮助 Lean 认识到 (pi p) 确实是可判定的？

Answer 1

编辑：只要它在定义的上下文中可用，详细说明者实际上可以完全自行推断实例：

variable (Hdecp : ∀ p, decidable (pi p))

include Hdecp
definition partn (n : nat) : nat := ∏ p ∈ (prime_factors n), (if pi p then p^(mult p n) else 1)

---

原始答案（如果实例有更复杂的假设仍然有用）：

如果要避免显式调用ite，可以在本地引入decidable实例：

definition partn (n : nat) : nat := ∏ p ∈ (prime_factors n),
have decidable (pi p), from Hdecp p,
if pi p then p^(mult p n) else 1

Answer 2

我找到了一个解决方案：

definition partn (n : nat) : nat := ∏ p ∈ (prime_factors n), (@ite (pi p) (Hdecp p) nat (p^(mult p n)) 1)

这允许我在 if-the-else 中明确使用 Hdecp