Zulip Chat Archive

Stream: new members

Topic: How to state this problem


view this post on Zulip Shing Tak Lam (Mar 02 2020 at 07:13):

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.

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 07:14):

Isn't it called nat.totient?

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 07:15):

I don't remember if we have this equality.

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:16):

looks like not

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:16):

This is some chinese remainder theorem argument, yes?

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 07:17):

This is one of the ways to interpret this.

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 07:18):

Or inclusion exclusion formula.

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:18):

that sounds more complicated

view this post on Zulip 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

view this post on Zulip 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

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=p1a1×p2a2×...×pkakN = p_1^{a_1} \times p_2^{a_2} \times ... \times p_k^{a_k}

and

f(N)=N(p11p1)(p22p2)...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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:28):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 02 2020 at 07:57):

For this question it might be easiest to avoid totient completely

view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Mar 02 2020 at 08:19):

It goes from positive naturals to Q

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 02 2020 at 08:27):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Mar 02 2020 at 08:38):

it's obviously not defined at zero

view this post on Zulip Kevin Buzzard (Mar 02 2020 at 08:40):

$ 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
?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 02 2020 at 09:05):

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

But every prime divides 0 ;-)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...)

view this post on Zulip 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 (pi,ei)(p_i,e_i) such that n=ipiein=\prod_ip_i^{e_i}.

view this post on Zulip Johan Commelin (Mar 02 2020 at 09:13):

maybe even "finset of pairs"?

view this post on Zulip Johan Commelin (Mar 02 2020 at 09:13):

You could use finsupp for that.

view this post on Zulip Kevin Buzzard (Mar 02 2020 at 09:13):

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

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Mar 02 2020 at 09:14):

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

view this post on Zulip 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 ;-)

view this post on Zulip 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 ;-)

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Johan Commelin (Mar 02 2020 at 09:26):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 02 2020 at 09:31):

Even that probably only deals with division, not the subtraction

view this post on Zulip 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) i(11/pi)=i(pi1)/i(pi)\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 nn.

view this post on Zulip 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 (pi,ei)(p_i,e_i) such that n=ipiein=\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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 :-/

view this post on Zulip Kevin Buzzard (Mar 02 2020 at 10:26):

For me the most natural mathematical proof is ni(11pi)=ipiei(11pi)=ipiei1(p1)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)

view this post on Zulip Kevin Buzzard (Mar 02 2020 at 10:27):

but without easy access to ipiei\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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 02 2020 at 10:34):

I bet that guy Carneiro proved that back in 17.

view this post on Zulip Mario Carneiro (Mar 02 2020 at 10:34):

lol he would

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 02 2020 at 10:58):

Why not turn the multiset into a finsupp?

view this post on Zulip Johan Commelin (Mar 02 2020 at 10:58):

That does exactly what you want, right?


Last updated: May 13 2021 at 18:26 UTC