Cancelling in the Integers

Stream: new members

[Andre Hernandez-Espiet (Rutgers)]

I was wondering if there is a tactic that takes care of cancelling and dividing over the integers. For example, a tactic that would solve the following examples (the first only accepted field_simp after the manipulation):

example {a b c: ℤ } (h: a≠ 0) : c*(a*b)/a = c*b:=
begin
  rw ← mul_assoc, rw mul_comm c a,rw mul_assoc,field_simp,
end

example  {a b c: ℤ} (a0:a≠  0)(h: a*b=a*c) : b=c := (mul_right_inj' a0).mp h

[Adam Topaz]

I think field_simp; ring shouuld solve such things

[Adam Topaz]

oh it's in Z

[Ruben Van de Velde]

Has ratify (qify?) landed?

[Adam Topaz]

division in $\mathbb{Z}$ can behave in unexpected ways

[Adam Topaz]

I'm a bit surprised that field_simp makes any progress at all!

[Kevin Buzzard]

I usually deal with division by using a high-powered tactic like ring to rearrange the term into a form where a cancelling lemma like mul_div_cancel applies. For example here I would do

import tactic

example {a b c : ℤ} (h: a ≠ 0) : c * (a * b) / a = c * b :=
begin
  rw (show c * (a * b) = (c * b) * a, by ring),
  exact int.mul_div_cancel _ h,
end

I like this approach because you somehow don't have to move your brain to deal with the problem.

[Andre Hernandez-Espiet (Rutgers)]

I see. I'll try to do more stuff like that in the future.