positivity failure

Stream: mathlib4

[Alex Meiburg]

I noticed something weird with positivity:

example (x : ℝ) (hx : 0 < x) : 0 < 5 + x := by
  positivity --works :)

example : 0 < 5 - (-3) := by
  positivity --works :)

example (x : ℝ) (hx : 0 < x) : 0 < 5 - (-x) := by
  positivity --Doesn't work!

I don't understand why the first two work but the third doesn't. My current understanding, which (checking the source) is also what it looks like it tries to do and what the docs describe it as, is to classify each subexpression as "positive" or "zero" or "negative" (or some combination of them), and then propagate these structurally. I would expect that, in the third case, -x is structurally negative, and 5 is structurally positive, so that 5 - (-x) is a positive minus a negative and so is positive.

[Alex Meiburg]

In this case rw [sub_neg_eq_add]; positivity works, but I would like to understand the general case (where it might not be so obvious)

[Daniel Weber]

It seems like the lemma 0 < x -> y < 0 -> 0 < x - y is simply missing

[Kevin Buzzard]

That might not be a lemma in mathlib because the hypotheses are too strong (either could be weakened to <=)

[David Renshaw]

classify each subexpression as "positive" or "zero" or "negative"

No, the three categories are positive, nonnegative and nonzero: https://github.com/leanprover-community/mathlib4/blob/496527772ac807ef3d1ddd4868f2048f9ea478e1/Mathlib/Tactic/Positivity/Core.lean#L35-L40

[David Renshaw]

example : 0 < 5 - (-3) := by
  positivity --works :)

This example works because positivity invokes some NormNum logic, which here successfully evaluates the right hand side to a natural number.

[David Renshaw]

Adding nonnegative and negative variants to Positivity.Strictness seems to me like it could work, but I think it would require updating many positivity extensions.

[Mario Carneiro]

I believe this is a deliberate design decision, @Heather Macbeth can probably explain it better. The short version of it is that positivity is intended for solving positivity goals which are positive for "obvious reasons", and expects you to preprocess the goal until it is obvious.

[Mario Carneiro]

it's supposed to correspond to the lines of a calc proof on paper which can be discharged with no further justification. In a case like this I think you would rewrite the a - (-b) to a + b first

[Michael Stoll]

To piggyback on this thread: can positivity be made to accept additional hypotheses (like, e.g., linarith does) as in the following?

import Mathlib

lemma foo (x : ℝ) : 0 < x := sorry

example (x : ℝ) : 0 < x := by
  positivity -- fails as expected

example (x : ℝ) : 0 < x := by
  have := foo x
  positivity -- works as expected

example (x : ℝ) : 0 < x := by
  positivity [foo x] -- syntax error, but would be nice to have

[Daniel Weber]

I wonder if we could have some with [term1, term2] <tactic> which adds the terms as temporary local variables for the tactic (perhaps also with some syntax to give them names)

[Alex Meiburg]

And that would effectively act as have := term1; have := term2; tactic <;> (clear this; clear this) or so?

[Daniel Weber]

Yes

[Heather Macbeth]

positivity is used a lot, including silently as a side-goal discharger in field_simp, gcongr, etc. One proof of mine which I was profiling recently used positivity 100 times. It's supposed to be "stupid" but fast and predictable.

[Heather Macbeth]

Michael Stoll said:

To piggyback on this thread: can positivity be made to accept additional hypotheses

This seems reasonable enough (but it wouldn't be relevant in the major use case, which is when positivity is used silently).

[Daniel Weber]

Daniel Weber said:

I wonder if we could have some with [term1, term2] <tactic> which adds the terms as temporary local variables for the tactic (perhaps also with some syntax to give them names)

Maybe there could also be with only which hides everything else from the tactic