## Stream: new members

### Topic: How to state this problem

#### Shing Tak Lam (Mar 02 2020 at 07:13):

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 (Mar 02 2020 at 07:14):

Isn't it called nat.totient?

#### Yury G. Kudryashov (Mar 02 2020 at 07:15):

I don't remember if we have this equality.

looks like not

#### Mario Carneiro (Mar 02 2020 at 07:16):

This is some chinese remainder theorem argument, yes?

#### Yury G. Kudryashov (Mar 02 2020 at 07:17):

This is one of the ways to interpret this.

#### Yury G. Kudryashov (Mar 02 2020 at 07:18):

Or inclusion exclusion formula.

#### Mario Carneiro (Mar 02 2020 at 07:18):

that sounds more complicated

#### Mario Carneiro (Mar 02 2020 at 07:19):

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

#### Shing Tak Lam (Mar 02 2020 at 07:26):

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

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 (Mar 02 2020 at 07:28):

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

#### Mario Carneiro (Mar 02 2020 at 07:28):

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

#### Kevin Buzzard (Mar 02 2020 at 07:57):

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 (Mar 02 2020 at 07:57):

For this question it might be easiest to avoid totient completely

#### Shing Tak Lam (Mar 02 2020 at 08:14):

@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 (Mar 02 2020 at 08:19):

It goes from positive naturals to Q

#### Shing Tak Lam (Mar 02 2020 at 08:23):

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 (Mar 02 2020 at 08:27):

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 (Mar 02 2020 at 08:31):

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 (Mar 02 2020 at 08:38):

it's obviously not defined at zero

#### Kevin Buzzard (Mar 02 2020 at 08:40):

\$ gp

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)
(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 (Mar 02 2020 at 08:58):

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 (Mar 02 2020 at 09:05):

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

But every prime divides 0 ;-)

#### Shing Tak Lam (Mar 02 2020 at 09:08):

@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 (Mar 02 2020 at 09:09):

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 (Mar 02 2020 at 09:09):

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 (Mar 02 2020 at 09:12):

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 (Mar 02 2020 at 09:13):

maybe even "finset of pairs"?

#### Johan Commelin (Mar 02 2020 at 09:13):

You could use finsupp for that.

#### Kevin Buzzard (Mar 02 2020 at 09:13):

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 (Mar 02 2020 at 09:14):

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 (Mar 02 2020 at 09:14):

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

#### Kevin Buzzard (Mar 02 2020 at 09:15):

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 (Mar 02 2020 at 09:16):

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 (Mar 02 2020 at 09:22):

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 (Mar 02 2020 at 09:26):

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

#### Johan Commelin (Mar 02 2020 at 09:26):

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

#### Johan Commelin (Mar 02 2020 at 09:28):

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 (Mar 02 2020 at 09:31):

Even that probably only deals with division, not the subtraction

#### Kevin Buzzard (Mar 02 2020 at 09:53):

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 (Mar 02 2020 at 10:05):

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 (Mar 02 2020 at 10:06):

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

#### Mario Carneiro (Mar 02 2020 at 10:07):

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

#### Kevin Buzzard (Mar 02 2020 at 10:25):

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 (Mar 02 2020 at 10:26):

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 (Mar 02 2020 at 10:27):

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 (Mar 02 2020 at 10:33):

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 (Mar 02 2020 at 10:34):

I bet that guy Carneiro proved that back in 17.

lol he would

#### Mario Carneiro (Mar 02 2020 at 10:37):

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

#### Johan Commelin (Mar 02 2020 at 10:58):

Why not turn the multiset into a finsupp?

#### Johan Commelin (Mar 02 2020 at 10:58):

That does exactly what you want, right?

Last updated: May 13 2021 at 18:26 UTC