How to state this problem

Stream: new members

[Shing Tak Lam]

image.png

I was doing some STEP problems, and came across one that was quite interesting. The proofs were fairly straightforward, and I thought I would be a fun exercise to try and prove it in Lean. However I'm not sure how I would create this function in Lean. I could define it from first principles like how I'd do it in Haskell, (fold, map, etc), but I feel like that way it wouldn't be as nice to deal with and the proofs may end up more complex.

For reference, this is 2005 STEP 2 Question 2.

[Yury G. Kudryashov]

Isn't it called nat.totient?

[Yury G. Kudryashov]

I don't remember if we have this equality.

[Mario Carneiro]

looks like not

[Mario Carneiro]

This is some chinese remainder theorem argument, yes?

[Yury G. Kudryashov]

This is one of the ways to interpret this.

[Yury G. Kudryashov]

Or inclusion exclusion formula.

[Mario Carneiro]

that sounds more complicated

[Mario Carneiro]

We would have to explode the product of binomials into a sum over subsets with fixed cardinality... sounds messy

[Shing Tak Lam]

This is from STEP, so it is (or should be) pre-university.

Therefore I don't think that the Chinese Remainder Theorem is expected here from the exam (if that reply is to me), although it may be required in lean. The properties that are required to be proven/disproved are attached below

image.png

So the proof for all of it is fairly straightforward (1 page of A4 when done on paper). The only part that may be more complicated is (i)(b).

The proof for (i)(b) uses the fact that

$N = p_1^{a_1} \times p_2^{a_2} \times ... \times p_k^{a_k}$

and

$f(N) = N(\frac{p_1 - 1}{p_1})(\frac{p_2 - 2}{p_2}) ...$

and these two cancel out nicely. So does this mean that in lean f(N) would need to be ℚ -> ℚ? and prove the denominator is 0?

(ii)(a) and (c) have trivial counterexamples, which Lean can check easily. (ii)(b) is also very simple as f(p) is just p - 1.

[Mario Carneiro]

One thing that makes lean different from "paper math" is that a property like (1)(b) will usually be true by definition

[Mario Carneiro]

for example nat.totient n is a natural number simply because its type is nat

[Kevin Buzzard]

The work still needs to be done, you just have to phrase it differently when you use totient, eg you now have to prove that the coercion to rat of totient equals the product in the question

[Kevin Buzzard]

For this question it might be easiest to avoid totient completely

[Shing Tak Lam]

@Mario Carneiro

I see. Looking on Wikipedia I found Euler's Totient Function, and it does seem to be equal to that formula. So I could use that for all of the rest. But then I'd still like to prove (i)(b) without using totient. I suppose this isn't the way that Lean proofs are normally written, as I deliberately avoid an existing result.

For this I'm more looking to follow the spirit of the original problem, rather than to do it the most straightforward way. Which means that I'd probably need to define my own version of the totient function. Anyways, knowing what it is called helps a lot, as I can (maybe) try and write my own version like the one that is already defined, only ℚ -> ℚ.

Thanks a lot!

[Kevin Buzzard]

It goes from positive naturals to Q

[Shing Tak Lam]

Oh right. Is there notation for positive rationals, or should I just special case 0 (such that the proofs would be trivial) with f 0 := 0

[Kevin Buzzard]

In pari-gp they define f 0 = 2 ;-) They argue that $f(n)$ is the number of units in $\mathbb{Z}/n\mathbb{Z}$.

[Shing Tak Lam]

Alright. It doesn't matter in this case as the proofs should all just be refl when N = 0as it is a special case. I just chose f 0 := 0 since if I use the original definition, (and say that 0 doesn't have any prime factors), then f(0) would be 0. #eval nat.totient also gave me 0.

There are probably reasons why it may not be zero, but I don't know enough about this topic to say which way it should be.

[Mario Carneiro]

it's obviously not defined at zero

[Kevin Buzzard]

$ gp
Reading GPRC: /home/buzzard/.gprc ...Done.

                                            GP/PARI CALCULATOR Version 2.9.3 (released)
                                   amd64 running linux (x86-64/GMP-5.1.3 kernel) 64-bit version
                             compiled: Jul 15 2017, gcc version 4.9.4 (Ubuntu 4.9.4-2ubuntu1~14.04.1)
                                                     threading engine: single
                                          (readline v6.3 enabled, extended help enabled)

                                              Copyright (C) 2000-2017 The PARI Group

PARI/GP is free software, covered by the GNU General Public License, and comes WITHOUT ANY WARRANTY WHATSOEVER.

Type ? for help, \q to quit.
Type ?15 for how to get moral (and possibly technical) support.

parisizemax = 1000001536, primelimit = 500000
? eulerphi(0)
%1 = 2
?

[Kevin Buzzard]

import data.pnat.factors data.rat algebra.big_operators

open pnat

def f : ℕ+ → ℚ :=
λ n, (n : ℚ) * ((factor_multiset n).to_finset.prod (λ (p : nat.primes), (1 : ℚ) - 1 / p)).

#eval f 12 -- 4
#eval f 80 -- 32

example : ∀ n : ℕ+, ∃ z : ℕ, f n = z :=
begin
  sorry
end

That's a pretty literal interpretation of part (i) and it would be pretty hard for a beginner do to (i)(b) in Lean.

[Kevin Buzzard]

(and say that 0 doesn't have any prime factors)

But every prime divides 0 ;-)

[Shing Tak Lam]

@Kevin Buzzard

Thanks a lot.

It seems like I've found something that is relatively easy Mathematics (as in STEP, so pre-university), but is quite difficult in Lean. I thought it was going to be relatively easy, since the proof (on paper), didn't require much beyond basic mathematics.

I've done enough functional programming to be able to understand the definition of f in your example, but yeah, I don't think I would have been able to come up with it. I think I'm gonna leave this for now and gain more experience in lean before I attempt the rest of it.

[Kevin Buzzard]

The proof is probably not too hard in Lean if you know what you're doing, but to do something in Lean you need to know the interface for the tools you're using, and I'm using a fair few things here.

[Shing Tak Lam]

Kevin Buzzard said:

(and say that 0 doesn't have any prime factors)

But every prime divides 0 ;-)

I know. Actually when thinking about it 0*n is 0 anyways, so even if I use all primes it wouldn't make a difference. (Although Lean wouldn't terminate then as there is an infinite number of primes, so...)

[Kevin Buzzard]

In Lean there is currently a function which takes a natural number n and returns the multiset of prime factors of n (e.g. it sends 45 to {3,3,5}). But what we really want here is a function which takes n and returns the multiset of pairs $(p_i,e_i)$ such that $n=\prod_ip_i^{e_i}$.

[Johan Commelin]

maybe even "finset of pairs"?

[Johan Commelin]

You could use finsupp for that.

[Kevin Buzzard]

Then you could just write $f(n)=\prod_ip_i^{e_i}(1-\frac{1}{p})=\prod_ip_i^{e_i-1}(p-1)$ and you'd be done.

[Kevin Buzzard]

modulo the issue of permuting the product around, and proving that a product of rationals each one of which was an integer, is an integer...

[Johan Commelin]

There is a way to move back and forth between multiset and finsupp

[Kevin Buzzard]

As far as I can see, this is a nice example of something which mathematicians would dismiss as trivial but that people like Mario would just complain was "not the right question" or something, as a way to cover up the fact that it's still such a mess to do in Lean ;-)

[Kevin Buzzard]

Mario Carneiro said:

One thing that makes lean different from "paper math" is that a property like (1)(b) will usually be true by definition

cunningly completely avoiding the question ;-)

[Kevin Buzzard]

The general issue, I guess, is something like the following: if someone comes along with a maths question and says "how do I do this in Lean?" then a formaliser might say "aah well, one way of formalising this question is as follows, and here's how to prove it". And then the person with the question might say "well that doesn't look the same as my question" and the formaliser could say "but it is mathematically equivalent, so we're done". My formalisation above is quite a literal formalisation of the question, and it might not be the one the formaliser wants to see, because we have all the added inconvenience of working with rationals, but it is arguably the one closest to the original intent of the question.

[Johan Commelin]

There is a proof in mathlib that nat.choose n k = n.fact / (k.fact * (n-k).fact).

[Johan Commelin]

The catch is... the subtraction and division take place in nat.

[Johan Commelin]

So to prove the mathematically-expected statement

(nat.choose n k : ℚ) = (n.fact : ℚ) / (k.fact * (n-k).fact : ℚ)

you'll have to work.

[Kevin Buzzard]

Even that probably only deals with division, not the subtraction

[Kevin Buzzard]

I think a relatively straightforward way to prove this, the way I formalised it, would be

(a) $\prod_i(1-1/p_i)=\prod_i(p_i-1)/\prod_i(p_i)$

(b) The finset is a subset of the multiset, so the product over the finset divides the product over the multiset

(c) The product over the multiset is $n$.

[Mario Carneiro]

Kevin Buzzard said:

In Lean there is currently a function which takes a natural number n and returns the multiset of prime factors of n (e.g. it sends 45 to {3,3,5}). But what we really want here is a function which takes n and returns the multiset of pairs $(p_i,e_i)$ such that $n=\prod_ip_i^{e_i}$.

There are functions to do this to a multiset. multiset.to_finset will produce the finset that results from deduplicating the factors, and for each of them you can call multiset.count on the original factors to get the multiplicity

[Mario Carneiro]

That said, it's not the most efficient algorithm, given that factors already has the information it needs to build the pairs

[Mario Carneiro]

For abstract work, I think there are some functions used in the padics that make this easier, something like padic_val

[Kevin Buzzard]

Yes, another approach would be to prove that the p-adic valuation of the product was >= 0 for all primes p. But this seemed even less convenient :-/

[Kevin Buzzard]

For me the most natural mathematical proof is $n\prod_i(1-\frac{1}{p_i})=\prod_ip_i^{e_i}(1-\frac{1}{p_i})=\prod_ip_i^{e_i-1}(p-1)$

[Kevin Buzzard]

but without easy access to $\prod_ip_i^{e_i}$ the approach I outlined above might be easier. The issue is that we don't seem to have any API for the finset of prime divisors of a pnat.

[Mario Carneiro]

I think if we had a theorem saying that if you take a multiset, turn it into a finset, and duplicate all elements by their count you get the original multiset, this would go a long way to break it down the way you want, because we already know things like the product over repeat a n is a power

[Kevin Buzzard]

I bet that guy Carneiro proved that back in 17.

[Mario Carneiro]

lol he would

[Mario Carneiro]

Ooh, there are some near misses: multiset.to_finset_sum_count_eq, and multiset.le_smul_erase_dup

[Johan Commelin]

Why not turn the multiset into a finsupp?

[Johan Commelin]

That does exactly what you want, right?