Zulip Chat Archive

Stream: new members

Topic: Bezout's identity

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

Brian Jiang (Mar 22 2020 at 17:08):

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

Kevin Buzzard (Mar 22 2020 at 17:09):

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

Kevin Buzzard (Mar 22 2020 at 17:09):

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

Brian Jiang (Mar 22 2020 at 17:11):

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

Brian Jiang (Mar 22 2020 at 17:11):

I'll take a look, thanks!

Kevin Buzzard (Mar 22 2020 at 17:11):

right, so it basically uses induction.

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)

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

Brian Jiang (Mar 22 2020 at 17:17):

by mathlib do you mean the github page?

Brian Jiang (Mar 22 2020 at 17:17):

sorry Im having a little trouble finding it

Mario Carneiro (Mar 22 2020 at 17:17):

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

Kevin Buzzard (Mar 22 2020 at 17:17):

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

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

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.

Brian Jiang (Mar 22 2020 at 17:20):

alright, thanks

Kevin Buzzard (Mar 22 2020 at 17:20):

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

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 :-)

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 $a$ and $b$ in the equation $gcd(x,y)=ax+by$

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

Patrick Massot (Mar 22 2020 at 17:31):

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

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

Mario Carneiro (Mar 22 2020 at 17:32):

Clearly the letter pairs are not allocated reliably

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).

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

Mario Carneiro (Mar 23 2020 at 02:53):

thanks!

Last updated: Dec 20 2023 at 11:08 UTC