Zulip Chat Archive

Stream: new members

Topic: weird prime error


view this post on Zulip Mantas Baksys (Apr 15 2021 at 15:52):

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!

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 15:56):

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.

view this post on Zulip Mantas Baksys (Apr 15 2021 at 16:01):

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.

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 16:03):

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.

view this post on Zulip Mantas Baksys (Apr 15 2021 at 16:38):

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?

view this post on Zulip Alex J. Best (Apr 15 2021 at 17:43):

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

view this post on Zulip Alex J. Best (Apr 15 2021 at 17:44):

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.

view this post on Zulip Alex J. Best (Apr 15 2021 at 17:54):

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

view this post on Zulip Mantas Baksys (Apr 15 2021 at 18:01):

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, qp

view this post on Zulip Alex J. Best (Apr 15 2021 at 18:34):

(deleted)

view this post on Zulip Scott Morrison (Apr 16 2021 at 00:17):

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


Last updated: May 11 2021 at 00:31 UTC