weird prime error

Stream: new members

[Mantas Baksys]

I wanted to mess around with the prime numbers for a bit but quickly ran into this problem.

import tactic data.nat.prime topology.metric_space.basic

open_locale classical
open filter nat
noncomputable theory

def inv_prime : primes → ℝ := λ p, 1/p

instance primes.preorder: preorder primes := subtype.preorder _
instance primes.nonempty: nonempty primes :=  nonempty_of_inhabited
instance primes.semilattice_sup: semilattice_sup primes := order_dual.semilattice_sup {p // nat.prime p}

theorem test : tendsto inv_prime at_top (nhds (0: ℝ)) :=
begin
    rw @metric.tendsto_at_top ℝ primes
     real.pseudo_metric_space primes.nonempty primes.semilattice_sup inv_prime (0: ℝ),
end

As posted above I tried to supply all instances manually but it fails saying it can't find exactly what it's trying to find!
Also, preorder primes was not automatic, is that intended (for the at_top part)? Thanks!

[Kevin Buzzard]

Lean seems to think there's two preorders on the primes, as you can see by set_option pp.all true before the test. If you just comment out instance primes.preorder it works.

[Mantas Baksys]

Thanks @Kevin Buzzard for the tool to check, will use that. So it turns out preorder primes was automatic, how weird that I got an error about that before, sorry.

[Kevin Buzzard]

I'm pretty sure that the semilattice_sup is giving you a preorder, and it might not be the preorder you want: what is this dual thing? You are ordering them twice in your code, with 2<=3 the first time and 3<=2 the second; this is why you were having problems.

[Mantas Baksys]

To be honest, I didn't look into it, I just looked at what the hypotheses were and then supplied them, just to check if I still got an error. I've now defined the correct semilattice_sup via subtype.semilattice_sup and I think I'll be good to go from here.
Anyways, isn't the idea here to not have to use @ before metric.tendsto_at_top at all?

[Alex J. Best]

I think using a linear order is a cleaner setup that gives what you want.

import tactic data.nat.prime topology.metric_space.basic

open_locale classical
open filter nat
noncomputable theory

def inv_prime : primes → ℝ := λ p, 1/p

instance primes.linear_order : linear_order primes := subtype.linear_order _

theorem test : tendsto inv_prime at_top (nhds (0: ℝ)) :=
begin
    rw metric.tendsto_at_top,
end

[Alex J. Best]

And yes, using that @ is sometimes a bad sign, as it means you are doing steps that the person who wrote the lemma thought should be automatic, sometimes it is necessary though.

[Alex J. Best]

One more thing: another approach is to make the definition of primes reducible locally, so that lean can see that it is just a subtype of nat, as most properties you need are just properties coming from the fact its a subtype of nat:

import tactic data.nat.prime topology.metric_space.basic

open_locale classical
open filter nat
noncomputable theory

def inv_prime : primes → ℝ := λ p, 1/p
local attribute [reducible] primes

theorem test : tendsto inv_prime at_top (nhds (0: ℝ)) :=
begin
    rw metric.tendsto_at_top,
end

[Mantas Baksys]

Thanks @Alex J. Best , this is very useful and I'm sure will prevent a lot of future subtype headaches :smiley:. Just as a quick follow-up, how would one define 'the set of all primes less than p : primes' as a subset of primes? I can define it as set ℕ but doing an equivalent thing for primes gives a Type error.

I think I worked it out myself

import data.nat.prime

open_locale classical
open nat
noncomputable theory

local attribute [reducible] primes

def primes_le (p:primes) : set primes := λ q, q≤p

[Alex J. Best]

(deleted)

[Scott Morrison]

Better to write { q | q ≤ p }. One should pretend as much as possible that you don't know that "sets are just functions to Prop".