ring tactic and division

Stream: general

[Matthew Pocock]

Is there a variant on the ring tactics that understand division?

example (a b c : ℕ) : a * (b / c) = b * (a / c) := by
  ring_nf -- fails to make any progress, but also does not produce a failure message

[Anne Baanen]

You might want to try the field_simp tactic. No idea if it makes progress here though.

[Anne Baanen]

It doesn't, because this is over the natural numbers and (as the name suggests) field_simp works over a field. But is this equality even true over the natural numbers?

[Anne Baanen]

The slim_check tactic reports:

===================
Found problems!
a := 1
b := 5
c := 2
issue: 2 = 0 does not hold
(4 shrinks)
-------------------

[Matthew Pocock]

Anne Baanen said:

You might want to try the field_simp tactic. No idea if it makes progress here though.

Doesn't seem to. I found mul_div_left_comm which seems to be the correct shape, but it is complaining that it can't find an instance of DivisionCommMonoid ℕ.

[Anne Baanen]

So the error is basically saying that division on the natural numbers is not very well behaved, and slim_check tells us your goal as stated is actually false :( If you try to prove it over ℚ instead, then field_simp works fine.

[Eric Rodriguez]

(deleted)

[Matthew Pocock]

ah ok -

Anne Baanen said:

So the error is basically saying that division on the natural numbers is not very well behaved, and slim_check tells us your goal as stated is actually false :( If you try to prove it over ℚ instead, then field_simp works fine.

Got it! I my specific case, c (in fact, all the numbers) are guaranteed greater than 1, but I guess even this may not help.

[Eric Rodriguez]

@loogle ?a * (?b / ?c) = ?b * (?a / ?c)

[loogle]

:search: mul_div_left_comm

[Eric Rodriguez]

I thought there was a nat lemma for this :/ but seems not

[Eric Rodriguez]

most things about nat division are rolled by hand and have various divisibility hypotheses

[Matthew Pocock]

Is this version at least true? (a b c : ℕ) : 0 < c -> a * (b / c) = b * (a / c)

[Eric Rodriguez]

no, try 3 * 2 / 3 vs 2 * 3/3

[Eric Rodriguez]

nat division is the floor of the normal division

[Patrick Massot]

Nothing is true about natural number subtraction and division.

[Patrick Massot]

Eric, that's a really weird way of stating it. It is the quotient in Euclidean division.

[Patrick Massot]

But there is a reason why people invented integers and rational numbers.

[Matthew Pocock]

Thanks for the help - I now understand why I should be doing this bit in ℚ :D It is a little alarming that part of my larger calculation will be going via ℚ but then will have an ultimate result guaranteed to be in ℕ -- I guess I will just have to add in some extra machinery to convince me that's correct.

[Alex J. Best]

See also the qify tactic which tries to automatically handle the transfer from Z to Q, assuming you have the right divisibility statements locally for it to make sense

[Matthew Pocock]

Alex J. Best said:

See also the qify tactic which tries to automatically handle the transfer from Z to Q, assuming you have the right divisibility statements locally for it to make sense

Is there some way to get a list of all available tactics? I keep on discovering there are more of them!

[Luigi Massacci]

I don’t know if there’s a more complete version, but I’m going by this one: https://github.com/haruhisa-enomoto/mathlib4-all-tactics/blob/main/all-tactics.md