what's going on with `decidable_prime`?

Stream: general

[Scott Morrison]

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]

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

[Mario Carneiro]

You should use by norm_num to prove this though

[Scott Morrison]

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

[Bryan Gin-ge Chen]

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

[Scott Morrison]

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]

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]

because proofs are irreducible

[Scott Morrison]

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]

It means that #eval and tactics can use it

[Mario Carneiro]

I think norm_num uses it

[Mario Carneiro]

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]

I think it might be the rw inside binary_rec

[Kenny Lau]

let's make a PR to core!