## Stream: general

### Topic: what's going on with decidable_prime?

#### Scott Morrison (Feb 24 2019 at 10:29):

import data.nat.prime

open nat

example : prime 11 := dec_trivial


fails, with

exact tactic failed, type mismatch, given expression has type
true
but is expected to have type
as_true (prime 11)


but

import data.nat.prime

open nat

instance (n : ℕ) : decidable (prime n) := nat.decidable_prime_1 n
example : prime 11 := dec_trivial


works. What's going with with nat.decidable_prime? It seems to be failing.

#### Mario Carneiro (Feb 24 2019 at 10:30):

There are two decidable instances. One works in the VM and the other works in the kernel

#### Mario Carneiro (Feb 24 2019 at 10:30):

You should use by norm_num to prove this though

#### Scott Morrison (Feb 24 2019 at 10:31):

I see. Maybe we should put some comments on those instances explaining this.

#### Bryan Gin-ge Chen (Feb 24 2019 at 15:30):

I think that would a good idea as this has come up before.

#### Scott Morrison (Feb 24 2019 at 20:32):

Ok, I've made https://github.com/leanprover-community/mathlib/pull/757. If someone could check that I actually wrote the right things, that would be great. :-)

#### Scott Morrison (Feb 24 2019 at 20:54):

I still don't understand why example : prime 11 := dec_trivial with the default instances actually fails. @Rob Lewis and @Mario Carneiro have explained at https://github.com/leanprover-community/mathlib/pull/757 that the problem is the kernel having to unfold proofs in the well-founded recursion used by the first instance. But why failure, rather than just being slow?!

#### Mario Carneiro (Feb 24 2019 at 20:54):

because proofs are irreducible

#### Scott Morrison (Feb 24 2019 at 21:00):

So, why do we provide that default decidable_prime instance at all? It's apparently faster in the VM, but who is actually taking advantage of that?

#### Mario Carneiro (Feb 24 2019 at 21:06):

It means that #eval and tactics can use it

#### Mario Carneiro (Feb 24 2019 at 21:06):

I think norm_num uses it

#### Mario Carneiro (Feb 24 2019 at 21:07):

I think it is actually a timeout problem. I traced the evaluation of nat.prime 7 back to evaluation of nat.size 7, which times out when you #reduce

#### Mario Carneiro (Feb 24 2019 at 21:08):

I think it might be the rw inside binary_rec

#### Kenny Lau (Feb 24 2019 at 21:30):

let's make a PR to core!

Last updated: May 10 2021 at 00:31 UTC