## Stream: new members

### Topic: Expand list.countp

#### Gareth Ma (Jan 23 2023 at 19:55):

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 (Jan 23 2023 at 20:24):

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 (Jan 23 2023 at 20:34):

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 (Jan 23 2023 at 20:38):

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 (Jan 23 2023 at 20:40):

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 (Jan 23 2023 at 20:45):

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 (Jan 23 2023 at 20:46):

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 (Jan 23 2023 at 20:46):

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 (Jan 23 2023 at 20:48):

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 (Jan 23 2023 at 20:48):

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 (Jan 23 2023 at 20:49):

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 (Jan 23 2023 at 20:49):

more like reimplemented

Alright!

#### Mario Carneiro (Jan 23 2023 at 20:50):

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

#### Gareth Ma (Jan 23 2023 at 20:54):

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 (Jan 23 2023 at 21:05):

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 (Jan 23 2023 at 21:05):

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 (Jan 23 2023 at 21:09):

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

#### Mario Carneiro (Jan 23 2023 at 21:09):

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

#### Mario Carneiro (Jan 23 2023 at 21:10):

this makes it less useful for proof purposes

#### Mario Carneiro (Jan 23 2023 at 21:11):

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

#### Gareth Ma (Jan 23 2023 at 21:15):

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 (Jan 23 2023 at 21:18):

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 (Jan 23 2023 at 21:19):

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 (Jan 24 2023 at 00:04):

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 (Jan 24 2023 at 00:11):

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

Last updated: Dec 20 2023 at 11:08 UTC