ith prime

Stream: new members

[Lucas Allen]

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]

nat.find

[Alex J. Best]

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]

Cool Thanks.

[Lucas Allen]

Oh you can compute the primes as well. :)

[Kevin Buzzard]

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

[Mario Carneiro]

what do you mean?

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

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]

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]

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]

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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]

I think Patrick Stevens was working on this

[Johan Commelin]

There are some PRs even

[Mario Carneiro]

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]

Oleans or it didn't happen

[Kevin Buzzard]

Any version of lean/mathlib fine

[Kevin Buzzard]

Any community master version

[Kevin Buzzard]

Get a tick on the leaderboard/graveyard!