different gcd's?

Stream: Is there code for X?

[Alex Kontorovich]

Hello, is there code identifying these two gcds? Thanks!

import ring_theory.int.basic

lemma come_on (cc dd : ℤ ) : euclidean_domain.gcd cc dd = gcd cc dd :=
begin
  sorry,
end

[Alex J. Best]

Unfortunately it's not true!

import ring_theory.int.basic
import tactic.slim_check

lemma come_on (cc dd : ℤ ) : euclidean_domain.gcd cc dd = gcd cc dd :=
begin
  slim_check
end

reports

===================
Found problems!

cc := 0
dd := -1
issue: -1 = 1 does not hold
(1 shrinks)
-------------------

[Mario Carneiro]

It is surprising there is no theorem about this though

[Mario Carneiro]

it's not hard to prove they are equal up to sign, because they both satisfy the universal property of gcd

[Mario Carneiro]

but I'm not sure the exact rules of the sign of euclidean_domain.gcd are important to pin down

[Alex Kontorovich]

Ah ok, thanks. Is there a lemma that they agree up to sign?

[Alex J. Best]

I didn't see any, hopefully it shouldn't be too hard to prove, but it might depend a bit on what version is needed for your application.

[Mario Carneiro]

import algebra.euclidean_domain data.int.gcd

example (a b : ℤ) : int.nat_abs (euclidean_domain.gcd a b) = int.gcd a b :=
begin
  apply nat.dvd_antisymm; rw ← int.coe_nat_dvd,
  { rw int.nat_abs_dvd,
    exact int.dvd_gcd (euclidean_domain.gcd_dvd_left _ _) (euclidean_domain.gcd_dvd_right _ _) },
  { rw int.dvd_nat_abs,
    exact euclidean_domain.dvd_gcd (int.gcd_dvd_left _ _) (int.gcd_dvd_right _ _) }
end

[Mario Carneiro]

After some mathematica explorations, looks like this is the sign:

import algebra.euclidean_domain tactic.slim_check

example (a b : ℤ) : to_bool (euclidean_domain.gcd a b < 0 ↔ a = 0 ∧ b < 0 ∨ a < 0 ∧ a ∣ b) :=
by slim_check

[Paul van Wamelen]

We have
lemma nat_abs_gcd (i j : ℤ) : nat_abs (gcd_monoid.gcd i j) = int.gcd i j := rfl
in ring_theory/int/basic.lean.

[Mario Carneiro]

that's evidently a different function, though, since it's true by refl

[Mario Carneiro]

to wit:

lemma coe_gcd (i j : ℤ) : ↑(int.gcd i j) = gcd_monoid.gcd i j := rfl

[Mario Carneiro]

however there might be a theorem relating euclidean_domain.gcd and gcd_domain.gcd when they both apply

[Alex Kontorovich]

Great thanks! Followup question: I started using euclidean_domain.gcd because there's a function euclidean_domain.gcd_a etc, which I don't see in int.gcd? Or am I just missing something? Thanks!

[Mario Carneiro]

import data.int.gcd

namespace int

def gcd_a : ℤ → ℤ → ℤ
| (of_nat m) n := m.gcd_a n.nat_abs
| -[1+ m]    n := -m.succ.gcd_a n.nat_abs

def gcd_b : ℤ → ℤ → ℤ
| m (of_nat n) := m.nat_abs.gcd_b n
| m -[1+ n]    := -m.nat_abs.gcd_b n.succ

theorem gcd_eq_gcd_ab (x y : ℤ) : (gcd x y : ℤ) = x * gcd_a x y + y * gcd_b x y :=
begin
  cases x; cases y,
  { apply nat.gcd_eq_gcd_ab },
  { change (_ : ℤ) = _ + -y.succ * -_, rw neg_mul_neg,
    apply nat.gcd_eq_gcd_ab },
  { change (_ : ℤ) = -x.succ * -_ + _, rw neg_mul_neg,
    apply nat.gcd_eq_gcd_ab },
  { change (_ : ℤ) = -x.succ * -_ + -y.succ * -_, rw [neg_mul_neg, neg_mul_neg],
    apply nat.gcd_eq_gcd_ab },
end

end int

[Mario Carneiro]

added in #6212