2 is the first prime

Stream: Is there code for X?

[Ralf Stephan]

Is there code for it? If not, I suspect it should be possible to prove

import Mathlib

example : Nat.nth Nat.Prime 0 = 2 := by
    sorry

using not_prime_zero, not_prime_one, and prime_two, but I have no idea how. Can you please help?

[Yaël Dillies]

Does rfl do it?

[Yaël Dillies]

I would check myself, but you haven't provided a #mwe

[Ralf Stephan]

type mismatch
  Iff.rfl
has type
  ?m.7574 ↔ ?m.7574 : Prop
but is expected to have type
  nth Nat.Prime 0 = 2 : Prop

[Ralf Stephan]

added the import above, sorry

[Kyle Miller]

Here's getting it into a different form that's more computational, but rfl still doesn't work:

import Mathlib

example : Nat.nth Nat.Prime 0 = 2 := by
  rw [Nat.nth_zero]
  have : Set.Nonempty {n | Nat.Prime n} := ⟨2, Nat.prime_two⟩
  rw [Nat.sInf_def this]
  -- ⊢ Nat.find this = 2
  sorry

[Mitchell Lee]

Here's one way

import Mathlib

example : Nat.nth Nat.Prime 0 = 2 := by
    suffices 2 ≤ Nat.nth Nat.Prime 0 ∧ Nat.nth Nat.Prime 0 < 3 by linarith
    rw [← Nat.count_le_iff_le_nth Nat.infinite_setOf_prime, ← Nat.lt_nth_iff_count_lt Nat.infinite_setOf_prime]
    decide

[Ralf Stephan]

Thanks. I guess this is worth a PR? I just have the time.

[Ruben Van de Velde]

Yes, this seems fine to add

[Mitchell Lee]

Here's a potentially better way to do it

import Mathlib

theorem nth_eq_iff_of_ne_zero {p : ℕ → Prop} [DecidablePred p] {n m : ℕ} (hm : m ≠ 0) :
    Nat.nth p n = m ↔ Nat.count p m = n ∧ p m := by
  sorry

example : Nat.nth Nat.Prime 0 = 2 := by
  rw [nth_eq_iff_of_ne_zero]
  · decide
  · decide

[Kyle Miller]

Another approach along those lines:

theorem Nat.nth_eq_iff_of_infinite {p : ℕ → Prop} [DecidablePred p] (hi : (setOf p).Infinite) {n m : ℕ} :
    Nat.nth p n = m ↔ Nat.count p m = n ∧ p m := by
  constructor
  · rintro rfl
    simp [Nat.count_nth_of_infinite hi, Nat.nth_mem_of_infinite hi]
  · rintro ⟨rfl, h⟩
    exact Nat.nth_count h

example : Nat.nth Nat.Prime 0 = 2 := by
  rw [Nat.nth_eq_iff_of_infinite Nat.infinite_setOf_prime]
  decide

[Kyle Miller]

It turns out that's more powerful than needed. This suffices:

example : Nat.nth Nat.Prime 0 = 2 := by
  convert_to Nat.nth Nat.Prime (Nat.count Nat.Prime 2) = 2
  exact Nat.nth_count Nat.prime_two

[Kyle Miller]

Or rather

example : Nat.nth Nat.Prime 0 = 2 := Nat.nth_count Nat.prime_two

[Mitchell Lee]

Here's a way to make it all decidable

import Mathlib

instance {p : ℕ → Prop} [DecidablePred p] [hp : Fact (setOf p).Infinite] {n m : ℕ} :
    Decidable (Nat.nth p n = m) :=
  decidable_of_iff (Nat.count p m ≤ n ∧ n < Nat.count p (m + 1)) (by
    rw [Nat.lt_nth_iff_count_lt hp.elim, Nat.count_le_iff_le_nth hp.elim,
      Nat.lt_succ_iff, ← Nat.le_antisymm_iff, eq_comm])

instance : Fact (setOf Nat.Prime).Infinite := ⟨Nat.infinite_setOf_prime⟩

example : Nat.nth Nat.Prime 0 = 2 := by decide
example : Nat.nth Nat.Prime 1 = 3 := by decide
example : Nat.nth Nat.Prime 2 = 5 := by decide
example : Nat.nth Nat.Prime 3 = 7 := by decide

[Ralf Stephan]

So this is more general, thus more preferred I guess.

[Kyle Miller]

That kind of decidable instance isn't the best, since it only applies to Nat.nth Nat.Prime n = m, and it can't be used to evaluate Nat.nth Nat.prime n inside of other expressions. (Plus, we generally don't want to add global Facts if we can help it. That Fact might be ok since it has no hypotheses.)

[Ralf Stephan]

The zeroth case suffices for me so'll first PR the one-liner.

[Kyle Miller]

There could one day either be a norm_num plugin or a simproc to calculate Nat.nth Nat.prime n in general

[Ralf Stephan]

Kyle Miller said:

Or rather

example : Nat.nth Nat.Prime 0 = 2 := Nat.nth_count Nat.prime_two

failed to synthesize instance
  DecidablePred Prime

[Ralf Stephan]

Hmm.. simply adding it and an import of Nth to Nat/Prime will give me this error, but a plain mwe will not.
Ah, I inserted too high in the file.

[Mario Carneiro]

I think a good way to write the decidable instance would be to have a class Productive p like this:

import Mathlib.Data.Nat.Nth

class Productive (p : ℕ → Prop) where
  next : ℕ → ℕ
  next_least {i n} (h : i ≤ next n) : next n = i ↔ p i ∧ n ≤ i

def Nat.nth' (p : ℕ → Prop) [Productive p] (n : ℕ) : ℕ :=
  Productive.next p <|
    match n with
    | 0 => 0
    | i+1 => Nat.nth' p i + 1

theorem nth_eq_nth' (p : ℕ → Prop) [Productive p] (n : ℕ) : Nat.nth p n = Nat.nth' p n := sorry

instance (p : ℕ → Prop) [Productive p] (n a : ℕ) : Decidable (Nat.nth p n = a) :=
  decidable_of_iff (Nat.nth' p n = a) <| by rw [nth_eq_nth']

[Timo Carlin-Burns]

Is it possible to write an efficient implementation of Productive Nat.Prime? next only gives you the largest prime you've generated so far, but you want to test divisibility against all the primes you've generated so far.