## Stream: new members

### Topic: Prop to bool

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


#### Kenny Lau (Sep 11 2018 at 12:51):

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

#### Olli (Sep 11 2018 at 12:54):

I get:

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


#### Chris Hughes (Sep 11 2018 at 12:55):

You need prime to be a decidable proposition.

#### Chris Hughes (Sep 11 2018 at 12:55):

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

#### Kenny Lau (Sep 11 2018 at 12:55):

oh, he defined prime by himself

I didn't notice

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

#### Olli (Sep 11 2018 at 12:57):

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

#### Chris Hughes (Sep 11 2018 at 12:57):

There isn't one in core.

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

#### Olli (Sep 11 2018 at 13:31):

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

#### Kevin Buzzard (Sep 11 2018 at 14:09):

or use mathlib's prime :-)

Last updated: May 10 2021 at 00:31 UTC