field_simp made no progress

Stream: mathlib4

[Asei Inoue]

why this raise an error?

import Mathlib.Tactic

variable (x y : ℝ)

example : x * y ≤ (x ^ 2 + y ^ 2) / 2 := by
  /-
  simp made no progress
  -/
  field_simp

[Damiano Testa]

To me, it does seem that (field_)simp made no progress, so I don't find the error strange.

[Asei Inoue]

my expectation: goal is changed to 2 * x * y ≤ (x ^ 2 + y ^ 2)
actual: no progress

[Damiano Testa]

I have nothing else but this example to go by, but it seems that "your" normal form is not one chosen by field_simp. I know that there has been talk about re-vamping field_simp, but I do not know what the, possibly future, normal form for this expression would be.

[Ruben Van de Velde]

This seems like a logical expectation. Does it work with equality?

[Michael Stoll]

Yes. I think inequalities are out of scope for field_simp.

[Michael Stoll]

(They require some order structure in addition, so cannot be dealt with using only field properties.)

[Asei Inoue]

indeed.

[Asei Inoue]

mere field does not have order….

[Asei Inoue]

is there a tactic can handle order relation in field?

[Kevin Buzzard]

nlinarith