primes

Stream: new members

[Alex Zhang]

How can I close the second example? (it is a little bit weird to me that norm_num doesn't work for the second one...)

import data.set.lattice
import data.nat.prime

open set nat

def primes : set ℕ := {x | prime x}

example : prime 2 :=
begin
  norm_num,
end

example : 2 ∈ primes :=
begin
   sorry
end

[Kevin Buzzard]

norm_num won't unfold the definition of primes for you so it can't make any progress

[Kevin Buzzard]

It's not its job to unfold things and it sticks to its job

[Johan Commelin]

maybe norm_num [primes] works.

[Alex Zhang]

Johan Commelin said:

maybe norm_num [primes] works.

Sadly, it wouldn't work. What can I do to close the goal then?

[Eric Wieser]

simp [primes], norm_num should work

[Kevin Buzzard]

or you can unfold primes (which does simp [primes] under the hood)

[Mario Carneiro]

actually just unfold primes won't be enough since you also need to cancel the mem and set_of

[Mario Carneiro]

although norm_num will probably do this since it uses the default simp set iirc

[Mario Carneiro]

by the way simp [primes] has an informative error message:

ambiguous overload, possible interpretations
    primes
    nat.primes

[Mario Carneiro]

norm_num [_root_.primes] works

[Alex Zhang]

It does work!

[Alex Zhang]

(deleted)

[Mario Carneiro]

It should work here and it usually makes some kind of progress.

[Mario Carneiro]

you will need to be more specific

[Mario Carneiro]

I don't recommend open nat because it has a tendency to cause name conflicts

[Mario Carneiro]

although I guess in this case it's due to your own definition overlapping with nat's

[Alex Zhang]

Could you explain what does _root_ mean in _root_.primes?

[Johan Commelin]

do_not_auto_insert_a_namespace.primes

[Mario Carneiro]

it is being used here to disambiguate between the absolute path primes and nat.primes since with open nat the unqualified primes could refer to either of them

[Mario Carneiro]

think of it like /primes vs /nat/primes instead of primes as a path