Zulip Chat Archive

Stream: new members

Topic: Prop to bool


view this post on Zulip Olli (Sep 11 2018 at 12:34):

I'm sure this will be covered later in the book, but I was wondering if there is a quick explanation for why I can't turn this prime Prop into a bool?

namespace hidden

open classical
open decidable
local attribute [instance] prop_decidable

def divides (m n : ) : Prop :=  k, m * k = n

instance : has_dvd  := divides

variables m n : 

def prime (n : ) : Prop := n  2   k, k  n  k = 1  k = n

#reduce prime 5
-- nat.less_than_or_equal 2 5 ∧ ∀ (k : ℕ), (∃ (k_1 : ℕ), nat.mul k k_1 = 5) → k = 1 ∨ k = 5

#eval to_bool $ prime 5
-- code generation failed, VM does not have code for 'classical.choice'

end hidden

view this post on Zulip Kenny Lau (Sep 11 2018 at 12:51):

if you remove local attribute [instance] prop_decidable then it should be fine

view this post on Zulip Olli (Sep 11 2018 at 12:54):

I get:

failed to synthesize type class instance for
m n : ℕ
⊢ decidable (prime 5)

view this post on Zulip Chris Hughes (Sep 11 2018 at 12:55):

You need prime to be a decidable proposition.

view this post on Zulip Chris Hughes (Sep 11 2018 at 12:55):

Lean doesn't know how to check whether 5 is prime.

view this post on Zulip Kenny Lau (Sep 11 2018 at 12:55):

oh, he defined prime by himself

view this post on Zulip Kenny Lau (Sep 11 2018 at 12:55):

I didn't notice

view this post on Zulip Chris Hughes (Sep 11 2018 at 12:56):

But it does know how to decide for the library definition of prime, so it should work for that.

view this post on Zulip Olli (Sep 11 2018 at 12:57):

I found a definition for prime in mathlib but nothing for it in the core library

view this post on Zulip Chris Hughes (Sep 11 2018 at 12:57):

There isn't one in core.

view this post on Zulip Kevin Buzzard (Sep 11 2018 at 13:28):

If you're going to roll your own prime then to do what you want to do you're also going to have to roll your own prime.decidable function giving an algorithm for testing primality. This is a good exercise; the way to do it is perhaps to search the source code for example of proofs of decidability, then figure out how to prove the key lemma (if n>=1 and k divides n then k<=n) and then write the algorithm. If you don't make it efficient then that's OK, you will have trouble working out if 617 is prime, but on the other hand at least the code will work (or it might give you a time-out the moment the numbers get too large to do on your fingers :-) )

view this post on Zulip Olli (Sep 11 2018 at 13:31):

yeah I think I should finish a few more chapters before attempting that

view this post on Zulip Kevin Buzzard (Sep 11 2018 at 14:09):

or use mathlib's prime :-)


Last updated: May 10 2021 at 00:31 UTC