Prime-counting function

Stream: new members

[Stepan Nesterov]

Dear all,
I have started learning Lean recently by doing some of the amazingly written exercises from prof. Buzzard's Formalising Mathematics workshop.
Now I am willing to formalize a simple theorem for myself: number 81 from Wiedijk's list, Divergence of Prime Reciprocals. I am having trouble figuring out how to define a function (n \mapsto p_n) in Lean properly. The definition should clearly rely on the Euclid's theorem of the infinitude of primes somehow. Is there a built-in way to define 'n-th member of a set' in Lean?

[Yakov Pechersky]

Sets are inherently disordered, so there is no "nth" element. You might prefer lists, or just a function nat -> _

[Stepan Nesterov]

Basically, I want a function which takes a subset of a linearly ordered set, and produces a list which contains all its elements sorted.
Although, how is divergence of a series defined in Lean? It uses the definition of a sequence as nat -> reals, right? Then I guess I want a function nat -> reals.

[Kevin Buzzard]

The way series work is that they're just functions from a random type (e.g. the naturals) to a type which is an additive commutative monoid and a topological space :-)

[Kevin Buzzard]

I didn't even say "topological monoid" because for the definition of convergence you don't need the addition and the topology to be compatible :-) Oh those computer scientists are so funny.

[Kevin Buzzard]

So you would want a function from the naturals to the reals, and my instinct is to define this function by recursion, sending 0 to 2 and, if it sends $n$ to $p(n)$, then it sends $n+1$ to nextprime (p n + 1)

[Kevin Buzzard]

which means you'll have to write nextprime first.

[Kevin Buzzard]

which is already an interesting exercise.

[Kevin Buzzard]

And then the theorem you're after would say that the function sending $n$ to $1/p(n)$ was not summable (you'd need to import topology.algebra.infinite_sum to get access to summable).

[Yakov Pechersky]

(Should we have a list.primes_up_to? Or a stream.primes?)

[Kevin Buzzard]

I dunno, those are CS questions. Maybe!

[Kevin Buzzard]

I cannot believe that it's 2021 and nat.find still does not have a docstring.

[Stepan Nesterov]

Looking through https://leanprover-community.github.io/mathlib_docs/data/nat/prime.html I only found (n -> list of factors of n) and no (n -> all primes less than n), unfortunately.
I could just use nat.factors(n!), but that would be ugly.

[Kevin Buzzard]

import data.nat.prime

open nat

#check exists_infinite_primes
-- ∀ (n : ℕ), ∃ (p : ℕ), n ≤ p ∧ nat.prime p

def nextprime (n : ℕ) : ℕ := nat.find (exists_infinite_primes (n + 1))

I think that's the function.

[Kevin Buzzard]

oh no wait, is nextprime 3 supposed to be 3 or 5? Hmm, pari-gp says 3.

[Kevin Buzzard]

def nextprime (n : ℕ) : ℕ := nat.find (exists_infinite_primes n)

That's the function then.

[Yakov Pechersky]

with sad sad computational performance

[Kevin Buzzard]

#eval nextprime 4 -- 5
#eval nextprime 5 -- 5

Looks good. Who cares about computational performance, we're proving a theorem.

[Stepan Nesterov]

Why is +1 an issue? Because it would skip 3?

[Kevin Buzzard]

I added 1 because I was jumping the gun: we do nextprime(p(n)+1) when defining p(n)

[Stepan Nesterov]

Thanks, will try that out! :-)

[Kevin Buzzard]

import data.nat.prime

open nat

#check exists_infinite_primes
-- ∀ (n : ℕ), ∃ (p : ℕ), n ≤ p ∧ nat.prime p

def nextprime (n : ℕ) : ℕ := nat.find (exists_infinite_primes n)

#eval nextprime 4 -- 5
#eval nextprime 5 -- 5

namespace prime

def p : ℕ → ℕ
| 0 := 2
| (n+1) := nextprime (p n + 1)

#eval p 3 -- 7 (note we start with p₀ = 2)

end prime

[Kevin Buzzard]

We've made some definitions so definitely the next thing to do is to prove some theorems about those definitions, for example some of the following might be helpful (and some might be hard): nextprime(n)>=n, nextprime(n) is prime, p(n) is prime, every prime p is p(n) for some n. The function p is injective, etc etc. thinking about it I'm not sure that calling the function p is a good idea -- you might want to use p for a prime number. Maybe pcount?

[Kevin Buzzard]

If p is prime and n<=p then nextprime(n)<=p etc.

[Eric Rodriguez]

Just so you know, PR #7274 has a proof of this! I'd encourage you to still do it (it'll be good fun) and it'll be interesting to compare your two approaches after

[Eric Rodriguez]

(for example #7274 doesn't use the next prime function)

[Kevin Buzzard]

oh what a crazy coincidence -- I didn't know we had this

[Eric Rodriguez]

just 10 hours ago :b

[Kevin Buzzard]

Isn't $\pi(n)$ traditionally the number of primes $\le n$?

[Eric Rodriguez]

sorry yes you're right, my point is that it doesn't use a "next prime" function

[Kevin Buzzard]

Interesting! Now I'm curious to see how you even stated it :-)

[Kevin Buzzard]

Aah -- very nice!

filter.tendsto (λ n, ∑ p in { p ∈ range n | nat.prime p }, (1 / (p : ℝ))) at_top at_top :=

You literally write down the finite sums by summing over finite sets.

[Stepan Nesterov]

A small follow-up question to be clear: does nat.find outputs a smallest element from a nonempty subset of nat?

[Stepan Nesterov]

Or from a proof that a set is nonempty, I guess

[Yakov Pechersky]

nat.find finds the smallest nat that satisfies some exists (n : nat) such that ...

[Yakov Pechersky]

A subset of nat, in Lean a term of type set nat, is like a function that takes a x : nat and gives you back the proposition that the x in the subset you're talking about

[Yakov Pechersky]

The definition in mathlib, of a nonempty subset is given by docs#set.nonempty, which is definitionally equal to:

s.nonempty = ∃ (x : α), x ∈ s

[Stepan Nesterov]

So, in this piece of code above, is (exists_infinite_primes n) a proof of {p | prime p \and p > n}.nonempty?

[Yakov Pechersky]

So yes, if you have some s : set nat and a proof that s.nonempty, then nat.find s.nonempty will give you the least x : nat such that x ∈ s

[Yakov Pechersky]

docs#nat.exists_infinite_primes

[Stepan Nesterov]

Ok, thanks!

[Yakov Pechersky]

That lemma is definitionally equal to what you just wrote about { ... }.nonempty. But it is phrased as the explicit existential statement

[Kevin Buzzard]

lean#566

[Kevin Buzzard]

It's in core, that's why there's no docstring. I had to clone Lean! I felt like a real computer scientist :-)

[Eric Rodriguez]

there was no need to do that for such a small change btw - on the github website, you can press the little edit box and it'll auto-create a branch for you and let you edit/PR

[Stepan Nesterov]

There is a very stupid problem I am running into.
So I want to know that 1/2>0, but when I just write have f : 1/2 > 0 := or whatever, it just assumes that I mean 1, 2 and 0 as naturals, and under this interpretation the statement is wrong! How do I tell Lean that I mean the real 1, not 1 in any other mathematical structure?

[Eric Rodriguez]

(1 : ℝ) / 2

[Stepan Nesterov]

Ok, thanks!

[Scott Morrison]

(1 / 2 : ℝ) is fine too, and generally more readable.

[Julian Berman]

Why does that work? I mean I guess it obviously works because Lean doesn't evaluate the 1 / 2 until after seeing it should be done in R? So Lean basically doesn't try to interpret the left side of a coersion until after seeing what type it's supposed to be?

[Scott Morrison]

It's all a bit complicated, but at least when there is expected type information available, Lean works from the outside in. So here is goes to look for a had_div ℝ instance first, and then after that starts trying to interpret the numerals as terms in ℝ.

[Scott Morrison]

In the opposite direction we sometimes use the trick (X : _), which basically forces Lean to forget the expected type as it interprets X.

[Julian Berman]

Interesting. Thanks for the explanation.

[Stepan Nesterov]

What is Lean's notation for restriction of a function?

[Johan Commelin]

You just compose with the inclusion.

[Stepan Nesterov]

It's easy to find names for functions in measure theory in mathlib, but I can't find a list with set-theoretic operations :(

[Johan Commelin]

Just ask here (but maybe in a new thread).

[Lucas Allen]

There's also this function for the ith prime which Mario wrote in another thread.

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

[Mario Carneiro]

(warning: that function computes well but proving that it produces primes requires Bertrand's postulate)

[Johan Commelin]

Which is almost in mathlib, I think.

[Marc Masdeu]

Kevin Buzzard said:

oh no wait, is nextprime 3 supposed to be 3 or 5? Hmm, pari-gp says 3.

sage: next_prime(3)
5

[Johan Commelin]

Mathlib's compromise:

#eval nextprime 3
-- 3
#eval next_prime 3
-- 5

[Kevin Buzzard]

@Marc Masdeu how about we go for 4 as a compromise ;-)

[Kevin Buzzard]

$ gp
? nextprime(3)
%1 = 3
?

[Stepan Nesterov]

Does mathlib have the following statement:
If n is a natural number such that for any prime p, the order of p in n is even, then n is a perfect square?

[Ruben Van de Velde]

I'm failing to even state it, so perhaps not :)

[Anne Baanen]

Here's a proof sketch, combining docs#unique_factorization_monoid.factors and docs#multiset.count: Prove by strong induction on m that ∀ (m : multiset R), (∀ p, 2 \dvd m.count p) -> ∃ (x : R), m.prod = x * x, and use docs#unique_factorization_monoid.factors_prod to conclude ∀ x, (order_of_factors_is_even x) -> ∃ y, associated x (y * y). Finally you need that all units in ℕ are squares (because they are all 1) to conclude that ∃ y, x = y * y.

[Ruben Van de Velde]

I was trying to use multiplicity, though Anne's approach makes more sense - I even have a fair amount of that code written :)
Will send a pointer in a bit

[Anne Baanen]

Ah good point, forgot about multiplicity. I guess we could split the difference via docs#unique_factorization_monoid.multiplicity_eq_count_factors

[Ruben Van de Velde]

import ring_theory.int.basic

open unique_factorization_monoid

lemma multiset.exists_nsmul_of_dvd
  {α : Type*}
  [decidable_eq α]
  (s : multiset α)
  (k : ℕ)
  (h : ∀ x ∈ s, k ∣ multiset.count x s) :
  ∃ t : multiset α, s = k • t := sorry

example (n k : nat) (hn : 0 < n) (h : ∀ m : nat, m.prime → k ∣ (factors n).count m) : ∃ m : nat, n = m ^ k :=
begin
  suffices : ∃ m' : multiset ℕ, (factors n) = (k • m'),
  { obtain ⟨m', hm'⟩ := this,
    apply_fun multiset.prod at hm',
    have := factors_prod hn.ne',
    rw associated_iff_eq at this,
    rw [multiset.prod_nsmul, this] at hm',
    exact ⟨m'.prod, hm'⟩ },
  apply multiset.exists_nsmul_of_dvd,
  intros x hx,
  apply h,
  rw nat.factors_eq at hx,
  apply nat.prime_of_mem_factors hx,
end

with the first lemma from https://github.com/Ruben-VandeVelde/flt/blob/main/src/multiset.lean

[Kevin Buzzard]

Is this your Fermat's Last Theorem repo?

[Bhavik Mehta]

With Neil Strickland's little used API for prime multisets, this can be done as

import data.pnat.factors

lemma multiset.exists_nsmul_of_dvd
  {α : Type*}
  [decidable_eq α]
  {s : multiset α}
  {k : ℕ}
  (h : ∀ x ∈ s, k ∣ multiset.count x s) :
  ∃ t : multiset α, s = k • t := sorry

example (q : ℕ) (n : ℕ+) (hn : ∀ p, q ∣ n.factor_multiset.count p) :
  ∃ k, n = k^q :=
let ⟨m, hm⟩ := multiset.exists_nsmul_of_dvd (λ x hx, hn _) in
⟨prime_multiset.prod m, by rw [←n.prod_factor_multiset, hm, prime_multiset.prod_smul]⟩

[Eric Wieser]

I'd be inclined to try and do that computably as

def multiset.nsmul_of_dvd
  {α : Type*}
  [decidable_eq α]
  {s : multiset α}
  {k : ℕ}
  (h : ∀ x ∈ s, k ∣ multiset.count x s) :
  { t : multiset α // s = k • t} := sorry

[Bhavik Mehta]

import data.finsupp

@[simp]
lemma to_multiset_symm_apply {α : Type*} [decidable_eq α] (s : multiset α) (x : α) :
  finsupp.to_multiset.symm s x = multiset.count x s :=
by convert rfl

noncomputable def multiset.exists_nsmul_of_dvd {α : Type*} [decidable_eq α] {s : multiset α}
  {k : ℕ} (h : ∀ x, k ∣ multiset.count x s) :
  { t : multiset α // s = k • t } :=
⟨(finsupp.map_range (λ t, t / k) (by simp) (finsupp.to_multiset.symm s)).to_multiset,
  by { ext x, simp [nat.mul_div_cancel' (h _)]} ⟩

Not much more computable, but potentially could be improved

[Eric Wieser]

Ah, docs#finsupp.to_multiset was something I was looking for

[Eric Wieser]

But finsupp is (almost) entirely non-computable, which is annoying here

[Eric Wieser]

Oh, it's even more annoying than that; docs#finsupp.to_multiset is non-computable only because the addition needed to state map_add is noncomputable!

[Stepan Nesterov]

So I have found and used unique_factorization_monoid.factors_prod, to prove that a natural number is a product of a multiset of its prime factors. Is there a converse statement: if s is a multiset of primes, than unique_factorization_monoid.factors (s.prod) = s?

[Johan Commelin]

I think that Neil Strickland proved that equivalence, yes. Hopefully it's somewhere in the same file.

[Bhavik Mehta]

docs#prime_multiset.factor_multiset_prod

[Stepan Nesterov]

Ok, so now I really struggle with the fact that some useful lemmas are proved fo unique_factorization_monoid.factors and some for pnat.factor_multiset.

I have started by

lemma square_separation (n : ℕ+) : ∃ m : ℕ+, ∃ r : ℕ+, (n = m * m * r ∧ squarefree r) :=
begin

  have f := pnat.prod_factor_multiset n,
  have ev_sep := even_separation ℕ+ (n.factor_multiset),
  cases ev_sep with t ht,
  cases ht with r hr,
  cases hr with n_uni hr',
  cases hr' with t_ev r_sqf,
  have t_sq := multiset_square ℕ+ t t_ev,
  cases t_sq with v hv,
  use v.prod, use r.prod, split,
  rw <- multiset.prod_add,
  rw <- multiset.prod_add,
  rw <- hv, rw <- n_uni,
  symmetry, exact f,

and then I fail to apply nat.squarefree_iff_nodup_factors because I have to work in \N+ and unique_factorization_monoid.squarefree_iff_nodup_factors because \N+ is not a unique factorization domain.
Is there a good way to deal with this issue?
For example, is it easy to relate squarefree r.prod and squarefree (\u r.prod : \N)?

[Hanting Zhang]

#backticks? Ok yay

[Johan Commelin]

But pnat is a unique factorization monoid, right? So hopefully that instance is in mathlib. And if not, then we should add it.

[Stepan Nesterov]

Hanting Zhang said:

#backticks? Ok yay

Thanks, they look nice :)

[Stepan Nesterov]

Johan Commelin said:

But pnat is a unique factorization monoid, right? So hopefully that instance is in mathlib. And if not, then we should add it.

looks like https://leanprover-community.github.io/mathlib_docs/ring_theory/unique_factorization_domain.html#unique_factorization_monoid means that a unique factorization monoid has a zero by definition, so I guess not.

[Johan Commelin]

I found

src/ring_theory/int/basic.lean
86:instance : unique_factorization_monoid ℕ :=

[Johan Commelin]

But maybe pnat is missing

[Johan Commelin]

ooh, hmz

[Johan Commelin]

Is there a reason that you want to prove your result for pnat?

[Johan Commelin]

Maybe prove it for nat first?

[Johan Commelin]

Once you have it for nat, deducing it for pnat is easy.

[Johan Commelin]

And I guess that you might as well prove it for an arbitrary UFM first, right?

[Stepan Nesterov]

Johan Commelin said:

Is there a reason that you want to prove your result for pnat?

I prove it for pnat because pnat has a lemma I asked about a few hours ago

[Stepan Nesterov]

Stepan Nesterov|407114* said:

So I have found and used unique_factorization_monoid.factors_prod, to prove that a natural number is a product of a multiset of its prime factors. Is there a converse statement: if s is a multiset of primes, than unique_factorization_monoid.factors (s.prod) = s?

this one

[Stepan Nesterov]

And I couldn't find a lemma that unique_factorization_monoid.factors (s.prod) is associated to s for s a multiset in a UFM

[Bhavik Mehta]

Johan Commelin said:

Is there a reason that you want to prove your result for pnat?

I think the issue is that Neil Strickland's nice results for prime multisets and pnats were done before unique factorization monoids and they haven't got linked between them

[Ruben Van de Velde]

@Stepan Nesterov one line, once I managed to state it :)

import ring_theory.unique_factorization_domain

example {α : Type*} [comm_cancel_monoid_with_zero α] [unique_factorization_monoid α]
  [nontrivial α] [decidable_eq α] [normalization_monoid α]
  {s : multiset α}
  (h : ∀ (x : α), x ∈ s → prime x)
  (h' : s.prod ≠ 0) :
  multiset.rel associated (unique_factorization_monoid.factors (s.prod)) s :=
prime_factors_unique unique_factorization_monoid.prime_of_factor h (unique_factorization_monoid.factors_prod h')

[Stepan Nesterov]

Ok, thanks, works like a charm :)

[Stepan Nesterov]

Under these definitions:

def nextprime (n : ℕ) : ℕ := nat.find (nat.exists_infinite_primes n)

def primecount : ℕ → ℕ
| 0 := 2
| (n+1) := nextprime (primecount n + 1)

how do I prove that, say, primecount 1 = 3? I am able to reduce it to nextprime 3 = 3 by unfolding the definitions, but I don't know how to prove that if 3 is the smallest prime greater than 3, then 3 = nextprime 3.

[Eric Wieser]

One of the lemmas about docs#nat.find should do that

[Stepan Nesterov]

It seems that there are three lemmas, which collectively cover 'nat.find p' is the smallest number that satisfies p, but no converse statement.

[Kevin Buzzard]

If this is a question, can you formalise what you're looking for in Lean?

[Kevin Buzzard]

PS I wrote that nat.find docstring a few weeks ago because I noticed that it was in fashion right now but didn't have a docstring. I notice from Eric's link that the docstring is now live, but there's no link to nat.find_min' whereas the other two things in the API seem to be live links.

[Eric Wieser]

docs#nat.find_min' works at least? I guess the link heuristic doesn't like a trailing '.

[Stepan Nesterov]

I wanted something like this, but I realized it is actually provable from the lemmas:

lemma nat_find_criterion (m : ℕ) {p : ℕ → Prop} (s : ∃ x : ℕ, p x) (hsat : p m) (hmin : ∀ n : ℕ, n < m → ¬p n) : m = nat.find s :=
begin
  have f := lt_trichotomy m (nat.find s),
  cases f,
  exfalso,
  exact nat.find_min s f hsat,
  cases f,
  exact f,
  exfalso,
  specialize hmin (nat.find s) f,
  exact hmin (nat.find_spec s),
end

[Stepan Nesterov]

But now, when I try to actually prove that 3 is the first prime with

lemma primecount_succ (n : ℕ) : primecount (n.succ) = nextprime (primecount n + 1) :=
begin
  refl,
end

lemma zeroth_prime : primecount 0 = 2 :=
begin
  refl,
end

lemma next_prime (n : ℕ) : nextprime n = nat.find (nat.exists_infinite_primes n) :=
begin
  refl,
end

lemma first_prime : primecount 1 = 3 :=
begin
  rw primecount_succ 0,
  rw zeroth_prime,
  norm_num,
  symmetry,
  rw next_prime,
  apply nat_find_criterion 3 (nat.exists_infinite_primes 3),
end

Lean says
invalid apply tactic, failed to unify
3 = nat.find _ with
3 = nat.find _

[Stepan Nesterov]

How do I modify the lemma so that it becomes applicable?

[Patrick Massot]

#mwe?

[Stepan Nesterov]

import data.nat.prime
import topology.algebra.infinite_sum
import algebra.squarefree
import ring_theory.unique_factorization_domain
import data.multiset.basic
import data.nat.parity
import algebra.associated
import data.pnat.factors

open finset
open_locale classical

def nextprime (n : ℕ) : ℕ := nat.find (nat.exists_infinite_primes n)

def primecount : ℕ → ℕ
| 0 := 2
| (n+1) := nextprime (primecount n + 1)

#eval primecount 1

lemma primecount_succ (n : ℕ) : primecount (n.succ) = nextprime (primecount n + 1) :=
begin
  refl,
end

lemma zeroth_prime : primecount 0 = 2 :=
begin
  refl,
end

lemma next_prime (n : ℕ) : nextprime n = nat.find (nat.exists_infinite_primes n) :=
begin
  refl,
end

lemma nat_find_criterion (m : ℕ) {p : ℕ → Prop} (s : ∃ x : ℕ, p x) (hsat : p m) (hmin : ∀ n : ℕ, n < m → ¬p n) : m = nat.find s :=
begin
  have f := lt_trichotomy m (nat.find s),
  cases f,
  exfalso,
  exact nat.find_min s f hsat,
  cases f,
  exact f,
  exfalso,
  specialize hmin (nat.find s) f,
  exact hmin (nat.find_spec s),
end

lemma first_prime : primecount 1 = 3 :=
begin
  rw primecount_succ 0,
  rw zeroth_prime,
  norm_num,
  symmetry,
  rw next_prime,
  apply nat_find_criterion 3 (nat.exists_infinite_primes 3),
end

[Patrick Massot]

The puzzling issue is you combined open_locale classical with wanting to compute. You can't have everything. So the first layer of fix is to go to

import data.nat.prime
import topology.algebra.infinite_sum
import algebra.squarefree
import ring_theory.unique_factorization_domain
import data.multiset.basic
import data.nat.parity
import algebra.associated
import data.pnat.factors

open finset
--open_locale classical

def nextprime (n : ℕ) : ℕ := nat.find (nat.exists_infinite_primes n)

def primecount : ℕ → ℕ
| 0 := 2
| (n+1) := nextprime (primecount n + 1)

#eval primecount 1

lemma primecount_succ (n : ℕ) : primecount (n.succ) = nextprime (primecount n + 1) :=
begin
  refl,
end

lemma zeroth_prime : primecount 0 = 2 :=
begin
  refl,
end

lemma next_prime (n : ℕ) : nextprime n = nat.find (nat.exists_infinite_primes n) :=
begin
  refl,
end

lemma nat_find_criterion {p : ℕ → Prop} [decidable_pred p] {m : ℕ} (hsat : p m)
  (hmin : ∀ n : ℕ, n < m → ¬p n) : m = nat.find ⟨m, hsat⟩ :=
sorry

lemma first_prime : primecount 1 = 3 :=
begin
  change nextprime 3 = 3,
  symmetry,
  apply nat_find_criterion,
  sorry, sorry,
end

[Patrick Massot]

(I put everything so you can use a diff tool to compare with your file)

[Patrick Massot]

The second layer is to realize you criterion is already in mathlib:

lemma nat_find_criterion {p : ℕ → Prop} [decidable_pred p] {m : ℕ} (hsat : p m)
  (hmin : ∀ n : ℕ, n < m → ¬p n) : m = nat.find ⟨m, hsat⟩ :=
((nat.find_eq_iff ⟨m, hsat⟩).mpr ⟨hsat, hmin⟩).symm

[Patrick Massot]

So you can remove it and start the last proof with:

lemma first_prime : primecount 1 = 3 :=
begin
  erw nat.find_eq_iff,
  sorry,
end

[Patrick Massot]

Note the e in erw asks rw to unfold definitions, but you could also write change nat.find _ = _, as the first line and then use the ordinary rw

[Stepan Nesterov]

Actually, if I remove open_locale classical, then my proof of nat_find_criterion stops working, and Lean objects with

failed to synthesize type class instance for
m : ℕ,
p : ℕ → Prop,
s : ∃ (x : ℕ), p x,
hsat : p m,
hmin : ∀ (n : ℕ), n < m → ¬p n
⊢ decidable_pred (λ (x : ℕ), p x)

[Stepan Nesterov]

Where can I read about what open_locale classical actually does?
It seems to come up quite often

[Patrick Massot]

Did you actually compare my version with yours?

[Patrick Massot]

I did change the statement of nat_find_criterion

[Stepan Nesterov]

By adding [decidable_pred p], I see

[Patrick Massot]

I don't know if we have a web page gathering what different locales do. You can go in the src folder of mathlib and run grep -R "localized.*classical"

[Patrick Massot]

That would show you everything, potentially including stuff you haven't imported. To make sure, you can write in your current lean file
run_cmd print_localized_commands [`classical], as explained on https://leanprover-community.github.io/mathlib_docs/commands.html#localized%20notation (whose title is a bit misleading)

[Patrick Massot]

Either way, you see that open_locale classical puts the instance tag on a bunch of declarations: eq.decidable, decidable_eq_of_decidable_le, classical.prop_decidable.

[Eric Wieser]

Oh, I thought all it did was src#classical.dec

[Patrick Massot]

The main thing is classical.prop_decidable

[Eric Wieser]

Huh, I guess docs#classical.prop_decidable is what docs#classical.dec is short for.

[Patrick Massot]

Stepan, do you understand what all those instances are about, or do you need more explanations?

[Patrick Massot]

Eric Wieser said:

Huh, I guess docs#classical.prop_decidable is what docs#classical.dec is short for.

#print classical.dec
/-
@[nolint id.{1} (list.{0} name) (Prop def_lemma)]
noncomputable theorem classical.dec : Π (p : Prop), decidable p :=
λ (p : Prop), classical.prop_decidable p
-/

[Patrick Massot]

I have no idea we why this need this duplication

[Stepan Nesterov]

So I guess open_locale classical lets you use axiom of choice (which implies the law of excluded middle)?

[Patrick Massot]

No, that's not at all about the axiom of choice.

[Stepan Nesterov]

But Lean is using classical logic by default, right? I'm using by_contra all the time and it is allowed

[Patrick Massot]

It's about excluded middle only.

[Stepan Nesterov]

So if we are allowed to apply classical.choice only to Prop, then this is equivalent to excluded middle?

[Eric Wieser]

You are always free to use classical.choice etc whenever. The locale just means that typeclass search will use it to produce decidable instances via LEM.

[Stepan Nesterov]

But now I'm confused on why do we have to open something if I can already use by_contra in Lean without opening it anyway?

[Eric Wieser]

Because by_contra isn't typeclass search

[Patrick Massot]

Lean can do two things: it can do mathematical reasoning, and there of course you want excluded middle and choice, but it can also do programming, which is useful when you want to write tactics and, less crucially, can be convenient in some proofs about computable objects. In programming excluded middle doesn't make any sense. Whatever the language, you want to be able to write if condition then ... else ... without the program hanging forever. The decidable classes in Lean are a way to register decision procedures so that it can execute such if statements. If classical.decidable_prop is an instance you're telling Lean that the procedure for any condition is to use the excluded middle law, but this will block execution.

[Mario Carneiro]

Many tactics will fall back on classical mode anyway, but if you are in term mode some things won't work, for example if x = y then ... if x = y isn't decidable

[Stepan Nesterov]

So if my definition is not noncomputable, then Lean will be able to actually calculate its output

[Stepan Nesterov]

Then shouldn't there be some universal tactic that proves things like primecount 1 = 3 by computation? If I type #eval primecount 1, then Lean correctly outputs 3, which means that deep down it knows the answer somehow

[Mario Carneiro]

yes, that exists

[Mario Carneiro]

due to recent changes in lean it doesn't quite work out of the box but you can do this:

import data.nat.prime

local attribute [instance] nat.decidable_prime_1

example : nat.prime 7 := dec_trivial

[Eric Wieser]

Why is docs#nat.decidable_prime_1 not an instance?

[Mario Carneiro]

because it's slower than the default instance, which is used by #eval

[Mario Carneiro]

if you want to do kernel computation you shouldn't use either one and use num.prime instead

[Mario Carneiro]

import data.num.prime

def find_prime : ℕ → num → num
| 0 n := 0
| (i+1) n := if n.prime then n else find_prime i n.succ

def ith_prime : ℕ → num
| 0 := 2
| (i + 1) := let n := ith_prime i in find_prime n n.succ

example : ith_prime 1 = 3 := dec_trivial
example : ith_prime 4 = 11 := dec_trivial
example : ith_prime 100 = 547 := dec_trivial

[Mario Carneiro]

The "universal tactic that proves things like primecount 1 = 3 by computation" is called norm_num

[Mario Carneiro]

however you have to write plugins for it to support new functions, and it doesn't know about primecount

[Mario Carneiro]

If it did, it could do a lot better than this naive counting algorithm