Expand `list.countp`

Stream: new members

[Gareth Ma]

Hi. I have the following goal:

list.countp prime (list.range (10 + 1)) = 4

How can I tell lean to expand countp and evaluate and actually prove this? It seems to me that by definition, lean should do this already:

def countp (p : α → Prop) [decidable_pred p] : list α → nat
| []      := 0
| (x::xs) := if p x then succ (countp xs) else countp xs

Here is reproducible code:

import data.nat.prime_norm_num
import number_theory.prime_counting

namespace nat
open_locale nat

example : prime 3 :=
begin
  norm_num,
end

example : π 10 = 4 :=
begin
  unfo
  unfold prime_counting' count prime,
  unfold list.countp,
  unfold prime_counting' count prime list.countp,
end

end nat

[Kevin Buzzard]

There has been far less effort been put into making Lean 3 compute like this than there has been into developing a large body of theorems. I don't even know how to prove this:

example : list.filter prime [0,1,2,3,4,5,6,7,8,9,10] = [2,3,5,7] :=
begin
  sorry,
end

[Gareth Ma]

Actually surprisingly, an unfold, combined with a tactic that evaluates prime n, works:

example : list.filter prime [0,1,2,3,4,5,6,7,8,9,10] = [2,3,5,7] :=
begin
  unfold list.filter,
  norm_num,
end

However, I am not sure why unfold list.countp doesn't, it gives simplify tactic failed to simplify, despite them having similar structures.

[Kevin Buzzard]

Oh nice! Mimicing your trick:

example : π 10 = 4 :=
begin
  change list.countp prime [0,1,2,3,4,5,6,7,8,9,10] = 4,
  unfold list.countp,
  norm_num,
end

[Kevin Buzzard]

The fact that some thought has to be given to navigating the minefield is just an indication that people have not put too much effort into this kind of question. Perhaps one reason for this is that lean 3 begins to struggle with computations of any kind of non-trivial size. This is the sort of question which you might hope a tactic in Lean 4 can solve much more efficiently.

[Mario Carneiro]

I have certainly put a lot of thought into problems of this form. The issue is that at least currently, norm_num basically needs custom implementations for every function you want to compute with, unless you can live with the fortuitous interaction it has with simp (which is often enough for list problems like this)

[Kevin Buzzard]

Yes -- you wrote norm_num and many custom extensions to it! Example here. But it was a one person show in Lean 3 and I for one had no motivation for trying to get stuff like this working in mathlib3 because it always seemed to me that lean 4 would be a far more appropriate tool for this kind of job.

[Mario Carneiro]

for an example like this I think the best approach is just to give the function a name (since this is the prime pi function after all) and implement a norm_num extension for it

[Mario Carneiro]

Lean 4 doesn't bring anything fundamentally new here, there are a few extra features that sometimes help like simp being able to prove stuff by decide sometimes but mostly it looks the same except that numerics are more practical because of bignum arithmetic

[Gareth Ma]

I see, I will definitely look into mathlib4 soon, once I get comfortable with mathlib3 and have the mental capacity haha. By the way, I modified your code to not require explicitly writing out the list:

example : π 10 = 4 :=
begin
  rw [prime_counting, prime_counting', count, list.range],

  simp only [list.range_core, list.countp], -- recursively simp.
  norm_num,
end

But then since countp by definition has a if-then-else branch, the tree grows exponentially I believe.

[Kevin Buzzard]

Seems to me that you're already half way towards writing the custom extension! However I would discourage you from doing this in mathlib3 because any changes to norm_num right now would need to be manually ported to mathlib4.

[Mario Carneiro]

more like reimplemented

[Gareth Ma]

Alright!

[Mario Carneiro]

we're implementing norm_num extensions on an as needed basis right now

[Gareth Ma]

If I do get to implement the norm_num extension for prime_counting at some point, probably a good idea to get Meissel-Lehmer Algorithm in too, since I believe it runs in O(n^(2/3+epsilon))

[Mario Carneiro]

Note that norm_num is (at least currently) primarily concerned with the small-numbers case, which is why primality checking is done using trial division instead of more sophisticated approaches with a better asymptotic complexity

[Mario Carneiro]

there isn't much point in having an algorithm that only pays off when the numbers are so big that other implementation limits are hit first

[Gareth Ma]

Ahh, that makes sense. Maybe I will add it as an extension, similar to the lucas-lehmer test?

[Mario Carneiro]

lucas-lehmer is also not a 100% correct test, right?

[Mario Carneiro]

this makes it less useful for proof purposes

[Mario Carneiro]

because we don't really care about certificates for compositeness, those are trivial

[Gareth Ma]

I think it is 100% correct for mersenne numbers - at least the wikipedia page suggests so. What I meant was to implement it as a separate tactic (lucas_lehmer.run_test) that user can use instead if required for some reason :)

[Mario Carneiro]

if we have the method available it makes sense to use it by default after switching based on the size of the number. I don't know whether it helps in these algorithms to know what the answer is before you start the computation (which is the usual situation in certificate generation)

[Mario Carneiro]

I guess you wouldn't be using it on mersenne numbers in the first place (if it's part of the algorithm for prime n or prime_counting n), because that would require recognizing mersenne numbers which seems like an unnecessary step

[Junyan Xu]

Gareth Ma said:

If I do get to implement the norm_num extension for prime_counting at some point, probably a good idea to get Meissel-Lehmer Algorithm in too, since I believe it runs in O(n^(2/3+epsilon))

Take a look at https://github.com/kimwalisch/primecount if you haven't :)

[Gareth Ma]

Yea I have, it is very cool, they computed the current prime_pi record didn't they?