Zulip Chat Archive

Stream: Is there code for X?

Topic: different gcd's?


view this post on Zulip Alex Kontorovich (Feb 12 2021 at 22:16):

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

view this post on Zulip Alex J. Best (Feb 12 2021 at 22:23):

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

view this post on Zulip Mario Carneiro (Feb 12 2021 at 22:24):

It is surprising there is no theorem about this though

view this post on Zulip Mario Carneiro (Feb 12 2021 at 22:24):

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

view this post on Zulip Mario Carneiro (Feb 12 2021 at 22:25):

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

view this post on Zulip Alex Kontorovich (Feb 12 2021 at 22:31):

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

view this post on Zulip Alex J. Best (Feb 12 2021 at 22:32):

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.

view this post on Zulip Mario Carneiro (Feb 12 2021 at 22:39):

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

view this post on Zulip Mario Carneiro (Feb 12 2021 at 22:50):

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

view this post on Zulip Paul van Wamelen (Feb 12 2021 at 23:01):

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.

view this post on Zulip Mario Carneiro (Feb 12 2021 at 23:04):

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

view this post on Zulip Mario Carneiro (Feb 12 2021 at 23:04):

to wit:

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

view this post on Zulip Mario Carneiro (Feb 12 2021 at 23:05):

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

view this post on Zulip Alex Kontorovich (Feb 13 2021 at 01:14):

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!

view this post on Zulip Mario Carneiro (Feb 13 2021 at 01:42):

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

view this post on Zulip Mario Carneiro (Feb 13 2021 at 01:57):

added in #6212


Last updated: May 19 2021 at 03:22 UTC