## Stream: new members

### Topic: ith prime

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

#### Kenny Lau (Dec 30 2020 at 06:56):

nat.find

#### 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  #### Lucas Allen (Dec 30 2020 at 07:13): Cool Thanks. #### Lucas Allen (Dec 30 2020 at 07:15): Oh you can compute the primes as well. :) #### 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? #### Mario Carneiro (Dec 30 2020 at 08:22): what do you mean? #### Mario Carneiro (Dec 30 2020 at 08:22): I don't think it will be significantly different in lean 4 #### 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 #### Kevin Buzzard (Dec 30 2020 at 08:26): I mean "now you're supposed to compile it, will there will be be a VM?" #### Kevin Buzzard (Dec 30 2020 at 08:28): Will #eval exist? Not that I ever use it... #### 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?

#### 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)

#### 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

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

#### 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

#### 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

#### 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?

#### Johan Commelin (Dec 30 2020 at 09:58):

I think Patrick Stevens was working on this

#### Johan Commelin (Dec 30 2020 at 09:58):

There are some PRs even

#### 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

#### Kevin Buzzard (Dec 30 2020 at 12:33):

Oleans or it didn't happen

#### Kevin Buzzard (Dec 30 2020 at 12:33):

Any version of lean/mathlib fine

#### Kevin Buzzard (Dec 30 2020 at 12:34):

Any community master version

#### Kevin Buzzard (Dec 30 2020 at 12:35):

Get a tick on the leaderboard/graveyard!

Last updated: May 11 2021 at 22:14 UTC