Zulip Chat Archive

Stream: new members

Topic: ith prime


view this post on Zulip Lucas Allen (Dec 30 2020 at 06:51):

Hello, I'd like to define the notion of the "ith prime," So far I have

import data.nat.prime

open nat

def primes_greater_than_n (n : ) : set  := {p :  | n < p  prime p}

def prime.ith :   
| 0     := 1
| (i+1) := set.min (primes_greater_than_n (prime.ith i)) --min isn't right, want the smallest element of a set of ℕ

However min isn't what I'm looking for, I need a function that returns the minimum element in a set of , is there something like this in mathlib? Also, is this a good way to formalize "ith prime"? At the moment I'm content with a definition which only works in proofs, but I think it'd be cool if it could be used to compute the ith prime as well. Thanks.

view this post on Zulip Kenny Lau (Dec 30 2020 at 06:56):

nat.find

view this post on Zulip Alex J. Best (Dec 30 2020 at 06:57):

import data.nat.prime
open nat
def ith_prime :   
| 0 := 2
| (i + 1) := nat.find (exists_infinite_primes $ ith_prime i + 1)

#eval ith_prime 4

view this post on Zulip Lucas Allen (Dec 30 2020 at 07:13):

Cool Thanks.

view this post on Zulip Lucas Allen (Dec 30 2020 at 07:15):

Oh you can compute the primes as well. :)

view this post on Zulip Kevin Buzzard (Dec 30 2020 at 08:11):

Lean's kernel isn't checking those computations though. How will this work in Lean 4 by the way?

view this post on Zulip Mario Carneiro (Dec 30 2020 at 08:22):

what do you mean?

view this post on Zulip Mario Carneiro (Dec 30 2020 at 08:22):

I don't think it will be significantly different in lean 4

view this post on Zulip Mario Carneiro (Dec 30 2020 at 08:23):

I think there might be a vm_compute kind of construct in lean 4 if you feel like trusting #eval to be a proof

view this post on Zulip Kevin Buzzard (Dec 30 2020 at 08:26):

I mean "now you're supposed to compile it, will there will be be a VM?"

view this post on Zulip Kevin Buzzard (Dec 30 2020 at 08:28):

Will #eval exist? Not that I ever use it...

view this post on Zulip Bryan Gin-ge Chen (Dec 30 2020 at 08:42):

So this is another example where #eval can show something but dec_trivial can't prove it:

import data.nat.prime
open nat
def ith_prime :   
| 0 := 2
| (i + 1) := nat.find (exists_infinite_primes $ ith_prime i + 1)
#eval ith_prime 4
example : ith_prime 4 = 11 := dec_trivial -- nope

I'm still surprised by this not working, but maybe I should know better.

Let me check my understanding. Mario suggested using whnf to try to figure out what gets stuck in a previous thread:

set_option pp.proofs true
run_cmd tactic.whnf `(by simp [ith_prime]; apply_instance : decidable (ith_prime 4 = 11)) >>= tactic.trace
/- something nasty starting with
nat.decidable_eq
  (nat.find
     (eq.rec (ith_prime._main._proof_1 3)
        (funext
           (λ (n : ℕ), ...
-/

Is the issue here similar to the one in that thread, where using well-founded recursion leads to something that doesn't reduce? Is there any reasonable way to define ith_prime so that it plays well with dec_trivial?

view this post on Zulip Kevin Buzzard (Dec 30 2020 at 08:48):

Who cares what the primes actually are? The only theorem you need about them is that there's at least two of them (or occasionally that there are infinitely many)

view this post on Zulip Mario Carneiro (Dec 30 2020 at 08:49):

I think lean 4 still has #eval. It will automatically use the VM for functions in the same file and compiled code for functions defined in other files

view this post on Zulip Mario Carneiro (Dec 30 2020 at 08:50):

The vm_compute thing will be more interesting to you, I think, because it basically replaces dec_trivial with "proof by #eval"

view this post on Zulip Mario Carneiro (Dec 30 2020 at 08:56):

import data.nat.prime
open nat

def find_prime :     
| 0 n := 0
| (i+1) n :=
  by haveI := decidable_prime_1 n; exact
  if prime n then n else find_prime i (n+1)

def ith_prime :   
| 0 := 2
| (i + 1) := let n := ith_prime i in find_prime n (n+1)

example : ith_prime 4 = 11 := dec_trivial

You need bertrand's postulate to prove the correctness of this function though

view this post on Zulip Mario Carneiro (Dec 30 2020 at 08:58):

but you can prove without much difficulty that it is correct if it returns a nonzero number

view this post on Zulip Kevin Buzzard (Dec 30 2020 at 09:57):

Wasn't there a partially finished version of Bertrand's postulate in a branch somewhere? I could see if I could drum up some interest on the discord?

view this post on Zulip Johan Commelin (Dec 30 2020 at 09:58):

I think Patrick Stevens was working on this

view this post on Zulip Johan Commelin (Dec 30 2020 at 09:58):

There are some PRs even

view this post on Zulip Mario Carneiro (Dec 30 2020 at 10:10):

incidentally, bertrand's postulate is also in the strike zone for the set.mm import: it only talks about nat and prime and it's been proven in metamath already. So I guess we've got it already via the set.mm -> lean bridge

view this post on Zulip Kevin Buzzard (Dec 30 2020 at 12:33):

Oleans or it didn't happen

view this post on Zulip Kevin Buzzard (Dec 30 2020 at 12:33):

Any version of lean/mathlib fine

view this post on Zulip Kevin Buzzard (Dec 30 2020 at 12:34):

Any community master version

view this post on Zulip Kevin Buzzard (Dec 30 2020 at 12:35):

Get a tick on the leaderboard/graveyard!


Last updated: May 11 2021 at 22:14 UTC