Zulip Chat Archive

Stream: maths

Topic: Integer gcd issues


Neil Strickland (May 06 2019 at 22:00):

Suppose we have x,y : ℤ. If I understand correctly:

  • int.gcd x y has type ; in particular int.gcd 0 (-2) = 2.
  • There is an instance of gcd_domain for which defines gcd_domain.gcd x y = int.of_nat (int.gcd x y). In particular, we have gcd_domain.gcd 0 (-2) = 2. This is more or less forced by the axioms for gcd_domain.
  • There is an instance of euclidean_domain for , and a function euclidean_domain.gcd defined using the euclidean algorithm. This always satisfies euclidean_domain.gcd 0 y = y (independent of any choices about rounding up or down in the division algorithm). In particular, we have euclidean_domain.gcd 0 (-2) = -2 ≠ gcd_domain.gcd 0 (-2).
  • mathlib currently has no results about the compatibility of these gcd functions.
  • Because of this, there is no immediate way to produce a and b such that int.gcd x y = a * x + b * y; we need to do some messing about with cases on the signs of x and y.

I assume that we have essentially the same issues with gcd of polynomials over a field.

This does not seem very satisfactory. Some possible ways to improve the situation:

  • Just add a bunch of compatibility lemmas specific to
  • Add an instance to show that a normalization domain that is also a euclidean domain can be regarded as a gcd domain, with gcd_domain.gcd x y being the normalization of euclidean_domain.gcd x y. Delete the direct gcd_domain instance for .
  • Modify the definition of euclidean_domain so as to include a normalization function that is allowed to be the identity. Define euclidean_domain.gcd to incorporate this function, so that it is possible for euclidean_domain.gcd to be part of a gcd_domain structure.

The second of these seems most promising to me. Am I missing anything?

Kevin Buzzard (May 06 2019 at 22:27):

@Chris Hughes @Mario Carneiro does this accurately represent the current state of things?


Last updated: Dec 20 2023 at 11:08 UTC