Zulip Chat Archive

Stream: Is there code for X?

Topic: Bézout's identity


view this post on Zulip Adrián Doña Mateo (Jan 11 2021 at 16:54):

I need a generalised Bézout's identity for more than 2 integers for an IMO problem. Is there something like that in mathlib?

view this post on Zulip Johan Commelin (Jan 11 2021 at 17:10):

Not that I know of

view this post on Zulip Kevin Buzzard (Jan 11 2021 at 17:17):

What's the statement?

view this post on Zulip Adrián Doña Mateo (Jan 11 2021 at 17:22):

Given any integers a₁,...,aₙ there always exist integers x₁,...,xₙ such that x₁ * a₁ + ⋯ + xₙ * aₙ = gcd(a₁,...,aₙ). I believe something similar is true for principal ideal domains.

view this post on Zulip Adrián Doña Mateo (Jan 11 2021 at 17:26):

I don't think there is a definition of gcd for more than two elements in mathlib so seems like there can't be for this. Any thoughts on how difficult it would be to define this and prove the generalised identity?

view this post on Zulip Aaron Anderson (Jan 11 2021 at 17:28):

You can state this with multiset.gcd or finset.gcd

view this post on Zulip Aaron Anderson (Jan 11 2021 at 17:29):

And multiset has a good inductive principle, so you could prove your desired version by induction

view this post on Zulip Aaron Anderson (Jan 11 2021 at 17:30):

What data structure did you want to use to encode the tuple of numbers?

view this post on Zulip Adrián Doña Mateo (Jan 11 2021 at 17:31):

I thought finset would make the most sense

view this post on Zulip Eric Wieser (Jan 11 2021 at 17:32):

Seems like this would be nice to prove for multiset, from which the proof for finset ought to be obvious?

view this post on Zulip Alex J. Best (Jan 11 2021 at 19:12):

Here's a messy sketch of this :smile:

import algebra.big_operators
open int
open euclidean_domain

lemma map_mul_sum (r : ) (l : list ) : (l.map ((*) (r : ))).sum = r * l.sum :=
by convert list.sum_hom l ⟨((*) r), mul_zero r, λ x y, mul_add r x y
lemma zip_with_mul_map_mul (r : ) (l₁ l₂ : list ) : l₁.zip_with (*) (l₂.map ((*) (r : ))) =
                                                     (l₁.zip_with (*) l₂).map ((*) (r : )) := sorry

def asd : Π (l : list ), {a : list  // l.foldr gcd 0 = (l.zip_with (*) a).sum }
| [] :=  [], by simp 
| (h :: ll) :=  gcd_a h (ll.foldr gcd 0) :: ((asd ll : list ).map ((*) (gcd_b h (ll.foldr gcd 0)))), begin
 simp,
 convert gcd_eq_gcd_ab _ _,
 have := (asd ll).2,
 simp [zip_with_mul_map_mul _ _ _, map_mul_sum],
 rw mul_comm,
 congr,
 exact this.symm,
end
#eval asd [6, 15, 10]

view this post on Zulip Adrián Doña Mateo (Jan 12 2021 at 11:43):

Is it preferable to have a function to this subtype or a theorem that states the existence of such list?

view this post on Zulip Eric Wieser (Jan 12 2021 at 11:44):

Given that @Alex J. Best has gone to the effort of a computable construction, it seems a shame to not use it and and provide a non-computable construction via exists.

view this post on Zulip Adrián Doña Mateo (Jan 12 2021 at 11:45):

That makes sense, thanks!

view this post on Zulip Eric Wieser (Jan 12 2021 at 11:47):

Although it might make sense to split asd into

def bezout_factors (l : list ) : list 

lemma bezout_prop (l) :  (bezout_factors l).foldr gcd 0 = (l.zip_with (*) (bezout_factors l)).sum

but only if that makes the definition simpler


Last updated: May 16 2021 at 05:21 UTC