Zulip Chat Archive

Stream: new members

Topic: Bezout's identity


view this post on Zulip Brian Jiang (Mar 22 2020 at 17:08):

I've been trying to prove Bézout's identity, but am stuck on the fact that the normal proof involves using the Euclidean algorithm indefinitely

view this post on Zulip Brian Jiang (Mar 22 2020 at 17:08):

Can someone give a few hints on how to start/proceed?

view this post on Zulip Kevin Buzzard (Mar 22 2020 at 17:09):

I'm not sure that proofs are allowed to be indefinitely long, in mathlib or otherwise :-)

view this post on Zulip Kevin Buzzard (Mar 22 2020 at 17:09):

Did you look at the proof which is already in mathlib?

view this post on Zulip Brian Jiang (Mar 22 2020 at 17:11):

whoops I meant that it uses the Euclidean algorithm until there is no remainder left

view this post on Zulip Brian Jiang (Mar 22 2020 at 17:11):

I'll take a look, thanks!

view this post on Zulip Kevin Buzzard (Mar 22 2020 at 17:11):

right, so it basically uses induction.

view this post on Zulip Kevin Buzzard (Mar 22 2020 at 17:13):

I haven't looked at what is in the repo, but if b<=a then you could prove that gcd(a,b) is a Z-linear combination of a and b by strong induction on a, and the inductive step could be done by observing that gcd(a,b)=gcd(a-b,b)

view this post on Zulip Mario Carneiro (Mar 22 2020 at 17:16):

The way it is done in mathlib is to slightly modify the definition of gcd to calculate the coefficients at the same time as it is doing the euclidean division

view this post on Zulip Brian Jiang (Mar 22 2020 at 17:17):

by mathlib do you mean the github page?

view this post on Zulip Brian Jiang (Mar 22 2020 at 17:17):

sorry Im having a little trouble finding it

view this post on Zulip Mario Carneiro (Mar 22 2020 at 17:17):

https://github.com/leanprover/mathlib/

view this post on Zulip Kevin Buzzard (Mar 22 2020 at 17:17):

Do you have a Lean project set up and a working leanproject command?

view this post on Zulip Mario Carneiro (Mar 22 2020 at 17:18):

That is, the work needed to prove gcd exists in the first place is about the same as that needed to prove that it is a linear combination of the inputs

view this post on Zulip Kevin Buzzard (Mar 22 2020 at 17:20):

Here is the theorem in mathlib but if you have set up a Lean project with mathlib as a dependency then all that code is on your computer already.

view this post on Zulip Brian Jiang (Mar 22 2020 at 17:20):

alright, thanks

view this post on Zulip Kevin Buzzard (Mar 22 2020 at 17:20):

They prove a constructive version of Bezout there, i.e. they actually come up with functions λ(a,b)\lambda(a,b) and μ(a,b)\mu(a,b) such that d=λ(a,b)a+μ(a,b)bd=\lambda(a,b)a+\mu(a,b)b.

view this post on Zulip Kevin Buzzard (Mar 22 2020 at 17:22):

this is what gcd_a and gcd_b are. They can't call them λ\lambda and μ\mu because λ\lambda is already used up for λ\lambda-calculus :-)

view this post on Zulip Mario Carneiro (Mar 22 2020 at 17:25):

actually I think the idea behind the naming convention is that gcd_a x y and gcd_b x y are aa and bb in the equation gcd(x,y)=ax+bygcd(x,y)=ax+by

view this post on Zulip Mario Carneiro (Mar 22 2020 at 17:28):

Hm, my name should be on that file, it looks like the proof got transplanted from another file and the attribution got separated from it

view this post on Zulip Patrick Massot (Mar 22 2020 at 17:31):

In France, Bézout's theorem is ua+vb=pgcd(a,b)ua + vb = \mathrm{pgcd}(a, b) so I always found mathlib utterly confusing hehre.

view this post on Zulip Mario Carneiro (Mar 22 2020 at 17:32):

we could change the names to gcd_u and gcd_v. There seems to be no name that is at all descriptive

view this post on Zulip Mario Carneiro (Mar 22 2020 at 17:32):

Clearly the letter pairs are not allocated reliably

view this post on Zulip Patrick Massot (Mar 22 2020 at 18:35):

I don't have a good solution here (and I don't think we should spend too much time thinking about this).

view this post on Zulip Bryan Gin-ge Chen (Mar 23 2020 at 00:06):

Mario Carneiro said:

Hm, my name should be on that file, it looks like the proof got transplanted from another file and the attribution got separated from it

https://github.com/leanprover-community/mathlib/pull/2217

view this post on Zulip Mario Carneiro (Mar 23 2020 at 02:53):

thanks!


Last updated: May 11 2021 at 13:22 UTC