Zulip Chat Archive

Stream: general

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


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 24 2019 at 10:30):

You should use by norm_num to prove this though

view this post on Zulip Scott Morrison (Feb 24 2019 at 10:31):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 24 2019 at 15:30):

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

view this post on Zulip 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. :-)

view this post on Zulip 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?!

view this post on Zulip Mario Carneiro (Feb 24 2019 at 20:54):

because proofs are irreducible

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Feb 24 2019 at 21:06):

It means that #eval and tactics can use it

view this post on Zulip Mario Carneiro (Feb 24 2019 at 21:06):

I think norm_num uses it

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 24 2019 at 21:08):

I think it might be the rw inside binary_rec

view this post on Zulip Kenny Lau (Feb 24 2019 at 21:30):

let's make a PR to core!


Last updated: May 10 2021 at 00:31 UTC