Should nlinarith know about x^2 \geq 0 when x is real?

Stream: Is there code for X?

[Terence Tao]

nlinarith is failing to solve this problem:

import Mathlib
import Mathlib.Tactic

example (a : ℝ) : a^2 ≥ 0 := by
  nlinarith

But replacing a^2 by a*a is fine, as is replacing a : \R with a : \N. So I suspect the problem is with Real:rpow not being recognized by nlinarith.

I can fix it with

example (a : ℝ) : a^2 ≥ 0 := by
  have h : a^2 = a*a := by ring
  rw [h]
  nlinarith

but perhaps nlinarith should just natively be happy with real squares being non-negative?

Incidentally, I am surprised to not see a method in mathlib that directly asserts that squares of real numbers are non-negative (at least, I was not able to locate it with various searches). This is like the most fundamental inequality in all of analysis.

[Heather Macbeth]

Seems like a bug, it's working in the most recent mathlib3 (which is the quickest way I could pull up an alternate version ... someone should bisect).

Terence Tao said:

Incidentally, I am surprised to not see a method in mathlib that directly asserts that squares of real numbers are non-negative (at least, I was not able to locate it with various searches). This is like the most fundamental inequality in all of analysis.

Have you seen positivity?

[Heather Macbeth]

... Ohhh ... I think this is the real-powers bug.

[Terence Tao]

I'm getting a similar issue with positivity.

image.png

[Heather Macbeth]

Short version: the mumbo-jumbo

local macro_rules | `($x ^ $y)   => `(HPow.hPow $x $y)

fixes this:

import Mathlib

local macro_rules | `($x ^ $y)   => `(HPow.hPow $x $y)

example (a : ℝ) : (0:ℝ) ≤ a^2 := by nlinarith
example (a : ℝ) : (0:ℝ) ≤ a^2 := by positivity

[Terence Tao]

It definitely does seem to be using real powers here.

image.png

[Terence Tao]

Heather Macbeth said:

Short version: the mumbo-jumbo

local macro_rules | `($x ^ $y)   => `(HPow.hPow $x $y)

fixes this:

import Mathlib

local macro_rules | `($x ^ $y)   => `(HPow.hPow $x $y)

example (a : ℝ) : (0:ℝ) ≤ a^2 := by nlinarith
example (a : ℝ) : (0:ℝ) ≤ a^2 := by positivity

Actually it produces a different error message!

image.png

[Heather Macbeth]

Long version: in Lean 4 it was initally planned to make a^b preferentially parse as if b were of the same type as a -- so a^b for a real was interpreted to have b real, too (unless further specified). This wasn't the case in Lean 3, and of course it's not what we expect in math. The local macro_rules is a temporary fix while we wait for lean4#2667 from core, or similar.

[Heather Macbeth]

Terence Tao said:

Actually it produces a different error message!

Note the (0:ℝ) where my code differs from yours ... the quick fix has unwanted side effects in other aspects of parsing.

[Terence Tao]

OK that fix works now. Anyway I now have enough workarounds for my current application, thanks. (Though I still find it odd that there isn't a theorem such as Real.mul_self_ge_zero in Mathlib. Surely I wasn't the first to have wanted to use it!)

[Mario Carneiro]

there certainly is

[Heather Macbeth]

Well, docs#sq_nonneg does exist (saying a ^ (2:ℕ) is nonnegative), but there doesn't exist a lemma saying a ^ (2:ℝ) is nonnegative (which, due to the powers bug, is what Terry was initially writing).

[Terence Tao]

Ah, I found LinearOrderedRing.mul_self_nonneg at least.

[Mario Carneiro]

docs#mul_self_nonneg

[Mario Carneiro]

@Joachim Breitner any idea why this doesn't work:

@loogle 0 ≤ ?a * ?a

[loogle]

:shrug: nothing found

[Mario Carneiro]

@Terence Tao one thing to keep in mind is that mathlib always uses \le instead of \ge in theorem statements, which usually doesn't matter but affects lemma naming. The other thing you would need to know to predict this name is that 0 ≤ has the special name nonneg in lemma statements instead of zero_le

[Mario Carneiro]

(similarly for pos, neg and nonpos)

[Heather Macbeth]

Anyway: open up any analysis file in mathlib currently and you'll see the hack

local macro_rules | `($x ^ $y)   => `(HPow.hPow $x $y)

at the top -- you'll likely want to do the same in your code.