int.gcd_add_self_right

Stream: Is there code for X?

[Kevin Buzzard]

We have nat.gcd_add_self_right : ∀ (m n : ℕ), m.gcd (n + m) = m.gcd n. One of the students in my class just wanted the int version of that and neither they nor I could find it. I have written a proof for them but I followed a path of least resistance:

import tactic
import data.int.gcd

theorem int.nat_abs_def (a : ℤ) : (a.nat_abs : ℤ) = if 0 ≤ a then a else -a :=
begin
  cases a,
  { simp, },
  { ring, },
end

theorem int.add_nat_abs (a b : ℤ) :
  (a + b).nat_abs = a.nat_abs + b.nat_abs ∨
  a.nat_abs = (a + b).nat_abs + b.nat_abs ∨
  b.nat_abs = (a + b).nat_abs + a.nat_abs :=
begin
  zify,
  simp [int.nat_abs_def],
  split_ifs,
  { left, ring, },
  { right, left, ring, },
  { right, right, ring, },
  { linarith, },
  { linarith, },
  { right, right, ring, },
  { right, left, ring, },
  { left, ring },
end

theorem int.gcd_add_self_right  (m n : ℤ) :
m.gcd (n + m) = m.gcd n :=
begin
  change (m.nat_abs).gcd (n + m).nat_abs = (m.nat_abs).gcd n.nat_abs,
  rcases int.add_nat_abs n m with (h | h | h);
  rw h,
  { rw nat.gcd_add_self_right },
  { rw nat.gcd_add_self_right },
  { rw [nat.gcd_add_self_left, add_comm, nat.gcd_add_self_left, nat.gcd_comm ] },
end

This proof was very easy to write: |a+b| is either going to be |a|+|b| or |a|-|b| or |b|-|a| (proof by mindless cases) so you can reduce to nat (as int.gcd a b := nat.gcd |a|,|b|) and then in all three cases it's going to be basically in the library. The problem with this approach of course is that I suspect this proof would not be acceptable for something so high up the import tree (did I get this right? This "tree" is an upside-down tree with the trunk at the top and leafs at the bottom, right? You wacky computer scientists...). There are variants too such as m.gcd (m + n) and (m + n).gcd m etc etc (and some of these don't even seem to be available for nat), but these are probably all painless the moment one has one of them, so the question is how to get the first one in an appropriate way (assuming this way isn't appropriate).

[Alex J. Best]

I would expect this to be proved for all Euclidean domains and maybe the proof can use docs#euclidean_domain.gcd_val

[Ruben Van de Velde]

I'm wondering if these two generalize:

 theorem nat.gcd_rec (m n : ℕ) : m.gcd n = (n % m).gcd m
 theorem nat.gcd_add_mul_right_right (m n k : ℕ) : m.gcd (n + k * m) = m.gcd n