efficiently dealing with / vs .div

Stream: mathlib4

[Jonathan Protzenko]

my goal contains this term: -↑R * x / ↑R * ↑R , and I also have ↑R ∣ -↑R in my context, so I'm trying to do rw [ Int.mul_div_assoc (-↑R: Int) ] to put this expression in a form that can be further simplified, but the lemma relies on .div while my goal uses / -- how can I reconcile the two? this seems to be an instance of a general pattern where I've previously had to deal with notations (e.g. writing lemmas of the form (↑R)⁻¹ = ZMod.inv q (↑ R) just to "evaluate away" the notation...) perhaps there is a good way to deal with these discrepancies?

FYI I get:

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  Int.div (-↑R * ?m.27345) ?m.27346

[Eric Wieser]

docs#Int.mul_ediv_assoc is what you want

[Eric Wieser]

.div and / are different operations (they round differently)

[Jonathan Protzenko]

ah that explains it. thanks!

[Eric Wieser]

It's a little confusing, because lemmas in Std about / are generally named ediv, while lemmas in mathlib use div in the name

[Eric Wieser]

I think there's a proposal to rename .div to .tdiv such that ediv can be called div and the confusion is gone

[Jonathan Protzenko]

thanks Eric! and I'd be remiss if I didn't ask: is there an efficient tactic in mathlib that might help simplify this expression? (just trying to remove the R / R part...)

[Jonathan Protzenko]

the proposal sounds good, but now that I now there's a confusing notation, I'll pay more attention to which one of the two I'm dealing with, thanks

[Eric Wieser]

I'm afraid that's not really answerable without a #mwe

[Jonathan Protzenko]

no problem, let me work a little more on that, thanks

[Jonathan Protzenko]

this is the original thing I was setting out to prove when I ran into / vs .div:

import Mathlib.Data.Int.ModEq

example (a: Int) (x: Int) (r: Int) (q: Int) (h_R: 0 < R) (h: a ≡ -R * x / R * R [ZMOD q]): a ≡ - x * R [ZMOD q] := by
  sorry

[Kevin Buzzard]

Can you make it a #mwe ? (read the link)

[Jonathan Protzenko]

ah yes thanks I didn't realize #mwe was clickable and I needed all of the imports... should be good now. I mean I did manage to prove that, but I'm wondering if there's a tactic that will do it in one step rather than my own painful 10 lines that involve proving divisibility and then re-arranging the terms rather tediously by hand

[Jireh Loreaux]

docs#Int.ediv_mul_cancel should get you there almost instantly.

[Jireh Loreaux]

As for automation, no, we don't really have any for that because integer division isn't well-behaved.

[Jonathan Protzenko]

yeah that's basically what I ended up doing

[Jonathan Protzenko]

good to know that there isn't anything more principled

[Jonathan Protzenko]

thanks!