精益抱怨看不出一个陈述是可判定的

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)

我怎样才能帮助精益认识到(π，p)确实是可判定的，多亏了Hdecp？

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。