bezout

Stream: new members

[Brian Jiang]

one of the theorems I am trying to prove uses this version of bezouts defined over the integers

'''
theorem relatively_prime_sum_to_one (a b : ℤ) (h : relatively_prime a b) :
∃ m n: ℤ, m* a + n * b = 1 := sorry
'''
Does lean already have a way to show the existence of m and n? Could I end up exacting something to get rid of the sorry?

[Bryan Gin-ge Chen]

You can probably use nat.gcd_eq_gcd_ab from data.int.gcd. If you paste more of your code (esp. the definition of relatively_prime) we can give more details.

By the way, to get proper syntax highlighting, use three backticks: ```, not single quotes.

[Brian Jiang]

here is the definition of relatively_prime:

def relatively_prime(a b:ℤ) := ∀l:ℤ, ¬(divides l a) ∨ ¬(divides l b)

[Mario Carneiro]

That's false

[Mario Carneiro]

1 always divides both a and b

[Mario Carneiro]

Maybe use nat.coprime instead?

[Mario Carneiro]

I'm not sure if there is an int.coprime but you could use nat.coprime (int.nat_abs a) (int.nat_abs b)

[Brian Jiang]

ah right, thanks

[Brian Jiang]

any suggestions on how to fill in the first theorem?

[Mario Carneiro]

Bryan already gave the suggestion

[Brian Jiang]

exact nat.gcd_eq_gcd_ab ?

[Brian Jiang]

apologies my grasp of the syntax isn't too good

[Mario Carneiro]

You will probably have to do some modifications depending on the exact statement of the theorem

[Mario Carneiro]

There is another version, euclidean_domain.gcd_eq_gcd_ab, that works over any euclidean domain. Since int is a euclidean domain this should give you something closer to what you want

[Mario Carneiro]

you have to import algebra.euclidean_domain

[Brian Jiang]

so when I define relatively_prime as def relatively_prime(a b:ℤ) := nat.coprime (int.nat_abs a) (int.nat_abs b)
and my theorem as theorem relatively_prime_sum_to_one (a b : ℤ) (h : relatively_prime a b) : ∃ m n: ℤ, m* a + n * b = 1 :=

[Brian Jiang]

how should I use euclidean_domain.gcd_eq_gcd_ab?

[Brian Jiang]

I tried exact euclidean_domain.gcd_eq_gcd_ab but that did not work

[Mario Carneiro]

Here's the start:

import algebra.euclidean_domain

def relatively_prime(a b:ℤ) :=  nat.coprime (int.nat_abs a) (int.nat_abs b)
open euclidean_domain
theorem relatively_prime_sum_to_one (a b : ℤ) (h : relatively_prime a b) :
  ∃ m n : ℤ, m * a + n * b = 1 :=
begin
  existsi [gcd_a a b, gcd_b a b],
  rw [mul_comm _ a, mul_comm _ b, ← gcd_eq_gcd_ab],

end

but I see now that there is a hole in the library: euclidean_domain.gcd on int is not proven equal to int.gcd

[Mario Carneiro]

What's more, it seems that euclidean_domain.gcd is not easily relatable to int.gcd because of a +- 1 difference. It seems that the proof using the nat version is easiest

import data.int.gcd

def relatively_prime(a b:ℤ) :=  nat.coprime (int.nat_abs a) (int.nat_abs b)
theorem relatively_prime_sum_to_one (a b : ℤ) (h : relatively_prime a b) :
  ∃ m n : ℤ, m * a + n * b = 1 :=
begin
  existsi [int.sign a * nat.gcd_a (int.nat_abs a) (int.nat_abs b),
           int.sign b * nat.gcd_b (int.nat_abs a) (int.nat_abs b)],
  rw [mul_right_comm, mul_comm _ a, int.mul_sign,
      mul_right_comm, mul_comm _ b, int.mul_sign,
      ← nat.gcd_eq_gcd_ab,
      show nat.gcd (int.nat_abs a) (int.nat_abs b) = 1, from h,
      int.coe_nat_one],
end

[Mario Carneiro]

@Brian Jiang Sorry for this, but it seems you might have picked an example that is not appropriate for your level. You should try working through theorem proving in lean to get the hang of the syntax

[Reid Barton]

If this isn't easy, it's definitely a hole in the library

[Bryan Gin-ge Chen]

What's the +-1 issue?

[Mario Carneiro]

This theorem itself is also a hole in the library, indeed

[Mario Carneiro]

It's easy enough to define gcd_a, gcd_b and gcd_eq_gcd_ab for integers using the parts of this proof

[Mario Carneiro]

It is true that int.nat_abs (gcd a b) = int.gcd a b but not gcd a b = \u (int.gcd a b)

[Mario Carneiro]

because gcd 0 b = b and int.gcd 0 b = int.nat_abs b

[Mario Carneiro]

I think we need a variation on gcd_eq_gcd_ab for euclidean domains where the lhs is any multiple of the gcd

[Mario Carneiro]

(in particular 1)

[Brian Jiang]

alright, thanks!

[Patrick Massot]

Mario Carneiro said:

but I see now that there is a hole in the library: euclidean_domain.gcd on int is not proven equal to int.gcd

This is a very well known hole. And each time we discuss it we end up noticing that sign issue, and the discussion stops.

[Mario Carneiro]

int.nat_abs (gcd a b) = int.gcd a b should be there regardless

[Mario Carneiro]

Isn't there something about normalization domains that should ensure that gcd a b is always the "canonical" element of the unit class, which in this case would mean that it's always nonnegative?

[Mario Carneiro]

Otherwise this function looks pretty scatterbrained