Should there be a Nonnegative class?

Stream: Is there code for X?

[Terence Tao]

Working with NNReal and various non-negativity side conditions are somewhat annoying, though with the advent of positivity and gcongr things are better. I wonder if perhaps it's worth it to make a Nonnegative class (similar other classes such as Finite or Nonempty) so that one could take advantage of instance inference to automate much of the nonnegativity side condition work. That is, to have some basic wrapper code such as

import Mathlib

class Nonnegative (x: ℝ) : Prop
where
  nonneg : 0 ≤ x

lemma nonnegative_of_nonneg {x:ℝ} (hx: 0 ≤ x) : Nonnegative x where
  nonneg := hx

lemma nonneg (x:ℝ) [Nonnegative x] : 0 ≤ x := Nonnegative.nonneg

instance : Nonnegative 0 where nonneg := Eq.le rfl

instance : Nonnegative 1 where nonneg := zero_le_one

instance : Nonnegative 2 where nonneg := zero_le_two

instance {n:ℕ} : Nonnegative n where nonneg := Nat.cast_nonneg n

instance {x:NNReal} : Nonnegative x where nonneg := x.2

instance {x y: ℝ} [hx:Nonnegative x] [hy:Nonnegative y] : Nonnegative (x+y) where nonneg := add_nonneg hx.nonneg hy.nonneg

instance {x y: ℝ} [hx:Nonnegative x] [hy:Nonnegative y] : Nonnegative (x*y) where nonneg := mul_nonneg hx.nonneg hy.nonneg

instance {x: ℝ} : Nonnegative (x^2) where nonneg := sq_nonneg x

@[simp]
lemma abs_of_nonneg' (x:ℝ) [Nonnegative x] : |x| = x := abs_of_nonneg (nonneg x)

etc., and then one obtains automatic nonnegativity statements such as

example (x y:ℝ) : Nonnegative (x^2 + y^2) := by infer_instance

example (x y:ℝ) : 0 ≤ x^2 + y^2 := nonneg _

example (x:ℝ) : 2 * x^2 - |2*x^2| = 0 := by simp

and so forth, thus bypassing a lot of appeals to the positivity tactic. Are there any downsides to introducing such a class?

Incidentally, while playing around with this concept, I discovered that Complex.abs_nonneg does not seem to exist:

import Mathlib

lemma Complex.abs_nonneg (z:ℂ) : 0 ≤ Complex.abs z := by
  positivity

I don't know if this was by design or is a simple omission.

[Matt Diamond]

re: your last point, I'm wondering if perhaps the intention was for docs#AbsoluteValue.nonneg to be used (since Complex.abs returns an AbsoluteValue)

[Terence Tao]

Matt Diamond said:

re: your last point, I'm wondering if perhaps the intention was for docs#AbsoluteValue.nonneg to be used (since Complex.abs returns an AbsoluteValue)

Indeed, AbsoluteValue.nonneg _ z is a term for the lemma. (For some reason exact? timed out before finding it, though.) Mathlib/Data/Complex/Abs.lean also contains a Complex.abs_nonneg' lemma that establishes exactly this, but it has been set to private for some reason.

[Eric Rodriguez]

I think this is usually avoided, there's a note somewhere related to docs#Fact that says something along the lines of "the type-class system is not meant to be a general FOL solver"; on the other hand I think docs#NeZero has been success since it was introduced in FLT-regular to deal with casts not being zeros. I think there's a difficult balance to be found.

[Yury G. Kudryashov]

We have positivity tactic instead of the Nonnegative/Positive typeclass.

[Yury G. Kudryashov]

And you can use, e.g., simp (disch := positivity) [my_lemmas]

[Sébastien Gouëzel]

In general, we avoid typeclasses for this kind of things, for performance and flexibility reasons. That's why also we don't have a measurable typeclass, which could be used to discharge automatically measurability goals. More precisely, typeclasses will try all the possible ways to get to the desired goal given the registered instances (which in many situations can lead to very bad performance), and they will only use the registered instances (which means that in many situations it won't be able to solve the goal). This means more fancy stuff using facts in the context or some kind of universal arguments can not be discharged with typeclasses -- for instance, you can't have a typeclass that will notice that x^n is nonnegative for any concrete even number n.

In this respect, lemmas with usual arguments but a default tactic discharger (like we did with finiteness in the PFR project) is often a better design.