Ambiguous overload

Stream: new members

[Stepan Nesterov]

I have a little annoying thing happen every time I refer to a natural prime:
ambiguous overload, possible interpretations
prime x
nat.prime x
The only thing I find that works is to replace prime x with its definition (p ≠ 0 ∧ ¬is_unit p ∧ ∀ (a b : ℕ), p ∣ a * b → p ∣ a ∨ p ∣ b)), which is very ugly. How do I specify that I mean 'prime' and not 'nat.prime' is a non-ugly way?

[Damiano Testa]

Probably, _root_.prime works, but is still clunky

[Eric Wieser]

Does your file do open nat somewhere? Because if it does, maybe removing that line would help

[Damiano Testa]

This may be happening because you have open nat: removing that might also work, but then you have to explicitly say nat. all the time.

[Johan Commelin]

@Stepan Nesterov Instead of nat.prime x you can write x.prime.

[Johan Commelin]

So that we you can do without open nat and still have "nice" notation for primes in nat

[Stepan Nesterov]

Eric Wieser said:

Does your file do open nat somewhere? Because if it does, maybe removing that line would help

Oh yes, it did for some reason and I never noticed. Thanks!

[Stepan Nesterov]

So next I am trying to define a set of primes up to a certain point, but
'''noncomputable def primes : ℕ → finset ℕ :=
λ n, filter (λ p, prime p) (range (primecount n))'''
results in
'''failed to synthesize type class instance for
n : ℕ
⊢ decidable_pred (λ (p : ℕ), prime p)'''
What does that mean?

[Eric Rodriguez]

filter needs a decision procedure to computably work, and for some reason there doesn't seem to be one for prime; can you try removing the lambda abstraction and see if it works? there should be one

[Ruben Van de Velde]

There might be one for nat.prime, not _root_.prime

[Stepan Nesterov]

How do I remove the lambda-abstraction? filter requires a function as an input

[Eric Rodriguez]

just write prime instead of λ p, prime p

[Eric Rodriguez]

but I fear Ruben is right

[Stepan Nesterov]

Oh, right

[Stepan Nesterov]

failed to synthesize type class instance for
n : ℕ
⊢ decidable_pred prime

[Stepan Nesterov]

The same

[Ruben Van de Velde]

So does

noncomputable def primes : ℕ → finset ℕ :=
λ n, filter nat.prime (range (primecount n))

work?

[Ruben Van de Velde]

Though if your def is noncomputable anyway, you might as well use open_locale classical before it, I suspect

[Eric Rodriguez]

noncomputable def primes := by { classical, exact λ n, filter (_root_.prime) (range (primecount n)) }

will do

[Stepan Nesterov]

Ruben Van de Velde said:

Though if your def is noncomputable anyway, you might as well use open_locale classical before it, I suspect

Yes, that does the trick :)

[Eric Rodriguez]

i do wonder why you're using this prime over nat.prime, especially as docs#nat.prime_iff_prime exists

[Stepan Nesterov]

Because the API for the fundamental theorem of arithmetic is for unique factorization monoids, basically

[Stepan Nesterov]

But I guess I have to use this equivalence at some point anyway, because infinitely many primes uses nat.prime