Why does `nlinarith` succeed?

Stream: mathlib4

[Martin Dvořák]

For reasons I don't understand, nlinarith succeeds here:

example {x : ℝ} : 2*x^2 - 6*x + 9 ≥ 0 := by
  nlinarith

However, it does not work here:

example {x : ℝ} : x^2 - 6*x + 9 ≥ 0 := by
  nlinarith

If I hint a proof, everything is all right again:

example {x : ℝ} : x^2 - 6*x + 9 ≥ 0 := by
  convert_to (x - 3) ^ 2 ≥ 0
  · ring
  nlinarith

In my attempt to narrow down where nlinarith clicks, I multiplied the original inequality by ten. This works:

example {x : ℝ} : 20*x^2 - 60*x + 90 ≥ 0 := by
  nlinarith

This does not:

example {x : ℝ} : 19*x^2 - 60*x + 90 ≥ 0 := by
  nlinarith

I made a few more attempts but I failed to learn to predict whether nlinarith succeeds.

I am not complaining about cases where nlinarith cannot close the goal automatically.
I am puzzled by what nlinarith does to succeed in cases 2*x^2 - 6*x + 9 ≥ 0 and similar.

[Mario Carneiro]

nlinarith is not complete for nonlinear arithmetic (I don't think it is decidable). The algorithm is described in the doc string:

The preprocessing is as follows:

• For every subterm a ^ 2 or a * a in a hypothesis or the goal,
  the assumption 0 ≤ a ^ 2 or 0 ≤ a * a is added to the context.
• For every pair of hypotheses a1 R1 b1, a2 R2 b2 in the context, R1, R2 ∈ {<, ≤, =},
  the assumption 0 R' (b1 - a1) * (b2 - a2) is added to the context (non-recursively),
  where R ∈ {<, ≤, =} is the appropriate comparison derived from R1, R2.

[Mario Carneiro]

But every subterm means every subterm, not just x^2 ≥ 0 but also (x^2)^2 ≥ 0 and (2*x^2 - 6*x + 9)^2 ≥ 0, as well as x^2 * (2*x^2 - 6*x + 9) ≤ 0 because we are assuming by contradiction that 2*x^2 - 6*x + 9 < 0. It turns out that linarith was able to find a very clever contradiction from these facts:

The expression
      81 * -1 +
      18 * (2 * x ^ 2 - 6 * x + 9) +
      4 * -(-x ^ 2 * -x ^ 2) +
      4 * -(-x ^ 2 * (2 * x ^ 2 - 6 * x + 9)) +
      -((2 * x ^ 2 - 6 * x + 9) * (2 * x ^ 2 - 6 * x + 9))
should be both 0 and negative

[Martin Dvořák]

How do you generate the explanation?

[Mario Carneiro]

set_option trace.linarith true

[Kevin Buzzard]

Note that this option is explicitly mentioned in the docstring.