Zulip Chat Archive

Stream: new members

Topic: Tactic for Divisibility

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

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: qa*x+b) (abar_is: q abar*a-1) : q x+abar*b :=
  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],

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

How about

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

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

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

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

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

Last updated: Dec 20 2023 at 11:08 UTC