feature request: field_simp in Nat

Stream: mathlib4

[Asei Inoue]

import Mathlib.Tactic

example (n m : Nat) : n * m = ((n + m) ^ 2 - n ^ 2 - m ^ 2 ) / 2 := by
  -- `field_simp` fails.
  -- Why doesn't `field_simp` use `Nat.div_eq_of_eq_mul_right` here?
  try field_simp

  symm
  apply Nat.div_eq_of_eq_mul_right
  . norm_num
  rw [show (n + m) ^ 2 = n ^ 2 + 2 * n * m + m ^ 2 from by ring]
  calc n ^ 2 + 2 * n * m + m ^ 2 - n ^ 2 - m ^ 2
    _ = (n ^ 2 - n ^ 2) + 2 * n * m + (m ^ 2 - m ^ 2) := by simp [add_assoc]
    _ = 0 + 2 * n * m + 0 := by congr 2 <;> simp_arith
    _ = 2 * (n * m) := by simp [mul_assoc]

example (n m : Rat) : n * m = ((n + m) ^ 2 - n ^ 2 - m ^ 2 ) / 2 := by
  -- `field_simp` works! :)
  field_simp
  ring

[Johan Commelin]

Because Rat is a field and Nat is not.

[Asei Inoue]

My point is that it would be useful if field_simp could also can be used in Nat.

[Johan Commelin]

It is out of scope. Division on Nat is pretty pathological

[Eric Wieser]

As is subtraction

[Ruben Van de Velde]

You can rify or qify first, but you'll need to show that you're not in a pathological case for that to work

[Asei Inoue]

I know it's not field_simp's job to do this.

Just having a tactic to try Nat.div_eq_of_eq_mul_right and Nat.div_eq_of_eq_mul_left would be useful for me.

It would be nice to have a tactic that hits the commonly performed operation of 'erasing the denominator'.

[Asei Inoue]

@Ruben Van de Velde

You can rify or qify first, but you'll need to show that you're not in a pathological case for that to work

Thank you ... But I didn't know how to do it. I would like to see an example code.

[Bolton Bailey]

Well, I think the issue with trying to use qify here is that you will run into the non-obviousness of the fact that ((n + m) ^ 2 - n ^ 2 - m ^ 2 ) is evenly divisible by 2.

[Kim Morrison]

omega is not very good at dealing with polynomials, but

import Mathlib.Tactic

example (n m : Nat) : n * m = ((n + m) ^ 2 - n ^ 2 - m ^ 2 ) / 2 := by
  ring_nf
  generalize n * m = nm
  omega

does work.

[Kim Morrison]

Actually, the need for generalize there seems to be a straight up omega bug. I'll investigate.

[Kim Morrison]

Ah, I see, omega has no way of knowing:

import Mathlib.Tactic

example (n m : Nat) : n * m = ((n + m) ^ 2 - n ^ 2 - m ^ 2) / 2 := by
  ring_nf
  have : 0 ≤ (n : Int) * (m : Int) := sorry
  omega -- works

[Kim Morrison]

(This is essentially the difference between linarith and nlinarith.)

[Kim Morrison]

I think this is far enough afield that I am not going to pursue it now. We had talked about adding an extensible mechanism for telling omega new facts about atoms, but have decided not to implement that immediately.

If someone is keen to push on this I'm happy to explain what would be required.

[Kevin Buzzard]

Asei Inoue said:

It would be nice to have a tactic that hits the commonly performed operation of 'erasing the denominator'.

I would say that natural division is not at all common and was arguably a code smell. a = b / c is sometimes what you want but far more common is the strictly stronger statement a * c = b which is what people would usually use rather than division.