CODEWITHSUNDEEP
decidablelean
user3078439
user3078439

Reputation: 315

Lean complains it can't see that a statement is decidable

I'm trying to define the following quantity partn:

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)

but get the error

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

How can I help Lean recognize that (pi p) is indeed decidable thanks to Hdecp?

Upvotes: 2

Views: 596

Answers (2)

Sebastian Ullrich
Sebastian Ullrich

Reputation: 1230

edit: The elaborator can actually infer the instance completely on its own, as long it's available in the definition's context:

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)

original answer (still useful if the instance has more complex hypotheses):

If you want to avoid the explicit call to ite, you can locally introduce the decidable instance:

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

Upvotes: 2

user3078439
user3078439

Reputation: 315

I found a solution:

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

which allows me to explicitly use Hdecp in my if-the-else

Upvotes: 0

Related Questions