How does nlinarith work?

Stream: lean4

[Shange Tang]

I saw somewhere the following lean code:

import Mathlib
import Aesop

set_option maxHeartbeats 0

open BigOperators Real Nat Topology Rat

example (a : ℝ) (h : 0 < a) (h_eq : a^3 = 6 * (a + 1)) : ¬ ∃ x : ℝ, x^2 + a * x + a^2 - 6 = 0 := by
  intro h_contra
  rcases h_contra with ⟨x, hx⟩
  nlinarith [sq_nonneg (x + a / 2)]

But I am confused about how nlinarith solve the goal.

[Shange Tang]

Also a similar question:

theorem algebra_sqineq_unitcircatbpamblt1
  (a b: ℝ)
  (h₀ : a^2 + b^2 = 1) :
  a * b + (a - b) ≤ 1 := by

  nlinarith [sq_nonneg (a - b)]

[Kim Morrison]

Some questions for you, so someone can answer effectively:

• do you know what linarith does?
• have you read the help text (e.g. available by hovering) for linarith and nlinarith?

[Leni Aniva]

A quick search in mathlib4 shows:

A variant, nlinarith, adds an extra preprocessing step to handle some basic nonlinear goals.
There is a hook in the LinarithConfig configuration object to add custom preprocessing routines.

The only difference in the frontend is this line:

let cfg := { cfg with
      preprocessors := cfg.preprocessors.concat nlinarithExtras }

so I looked at this function, and it says

• For every term t such that t^2 or t*t appears in the input, adds a proof of t^2 ≥ 0
  or t*t ≥ 0.

• For every pair of comparisons t1 R1 0 and t2 R2 0, adds a proof of t1*t2 R 0.

All of this can be found quickly by searching nlinarith in the mathlib codebase.

$ rg --iglob "**Frontend**" nlinarith
Mathlib/Tactic/Linarith/Frontend.lean
100:A variant, `nlinarith`, adds an extra preprocessing step to handle some basic nonlinear goals.
129:linarith, nlinarith, lra, nra, Fourier-Motzkin, linear arithmetic, linear programming
425:A variant, `nlinarith`, does some basic preprocessing to handle some nonlinear goals.
438:which are inherited by `nlinarith`; that is, `nlinarith!` and `nlinarith only [h1, h2]` all work as
447:syntax (name := nlinarith) "nlinarith" "!"? linarithArgsRest : tactic
448:@[inherit_doc nlinarith] macro "nlinarith!" rest:linarithArgsRest : tactic =>
449:  `(tactic| nlinarith ! $rest:linarithArgsRest)
479:  | `(tactic| nlinarith $[!%$bang]? $[$cfg]? $[only%$o]? $[[$args,*]]?) => withMainContext do
480:    let args ← ((args.map (TSepArray.getElems)).getD {}).mapM (elabLinarithArg `nlinarith)
483:      preprocessors := cfg.preprocessors.concat nlinarithExtras }
488:-- { name       := "nlinarith",
490:--   decl_names := [`tactic.interactive.nlinarith],