Integer gcd issues

Stream: maths

[Neil Strickland]

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]

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