Zulip Chat Archive

Stream: new members

Topic: Cancelling in the Integers

Andre Hernandez-Espiet (Rutgers) (Nov 04 2022 at 19:15):

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:=
  rw  mul_assoc, rw mul_comm c a,rw mul_assoc,field_simp,

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

Adam Topaz (Nov 04 2022 at 19:15):

I think field_simp; ring shouuld solve such things

Adam Topaz (Nov 04 2022 at 19:16):

oh it's in Z

Ruben Van de Velde (Nov 04 2022 at 19:17):

Has ratify (qify?) landed?

Adam Topaz (Nov 04 2022 at 19:17):

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

Adam Topaz (Nov 04 2022 at 19:18):

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

Kevin Buzzard (Nov 04 2022 at 20:09):

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 :=
  rw (show c * (a * b) = (c * b) * a, by ring),
  exact int.mul_div_cancel _ h,

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

Andre Hernandez-Espiet (Rutgers) (Nov 04 2022 at 20:15):

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

Last updated: Dec 20 2023 at 11:08 UTC