# Zulip Chat Archive

## 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