Tactic for Divisibility

Stream: new members

[Andre Hernandez-Espiet (Rutgers)]

I was wondering if there is a tactic that takes care of simple modular conditions. For example, a tactic that would solve the following, which is trivial on paper:

example {q a b x abar: ℤ } (div: q∣a*x+b) (abar_is: q∣ abar*a-1) : q∣ x+abar*b :=
begin
  cases div with z hz,
  cases abar_is with zz hzz,
  have := congr_arg (has_mul.mul abar) hz,
  rw [mul_add , ← mul_assoc] at this,
  use (abar*z-zz*x),
  rw [mul_sub,← mul_assoc q zz,← hzz, mul_comm abar z, ← mul_assoc, ← hz],
  ring,
end

[Ruben Van de Velde]

How about

example {q a b x abar: ℤ} (div : q ∣ a * x + b) (abar_is : q ∣ abar * a - 1) : q ∣ x + abar * b :=
begin
  convert div.linear_comb abar_is abar (-x) using 1,
  ring,
end

[Andre Hernandez-Espiet (Rutgers)]

Yes, that works! Very creative. I didn't even know convert could work with divides statements.

[Kevin Buzzard]

convert works with anything! tactic#convert let's see if there's a useful description in the docs. Edit: there is!