Speculative inequality tactics

Stream: mathlib4

[Heather Macbeth]

(Among other things, we don't have a negativity discharger tactic.)

[Jovan Gerbscheid]

Though if we had such a discharger tactic, I would expect it to be implemented as part of the positivity tactic.

[Jovan Gerbscheid]

So that it could for example also do this:

example (n m : ℤ) (hn : n < 0) (hm : m < 0) : 0 < n * m := by
  positivity

[Aaron Liu]

that feels like some sort of negativity

[Aaron Liu]

should we still call it positivity if it's doing negativity too?

[Jovan Gerbscheid]

Yes? It's already doing non-zero-ness as well, and we don't call it positivity_non_zero_ness

[Jovan Gerbscheid]

Although maybe one day we will have a tactic subsuming gcongr and positivity, and then we'll need a new name for it.

[Notification Bot]

7 messages were moved here from #PR reviews > #29364 `field_simp` for inequalities by Heather Macbeth.

[Lawrence Wu (llllvvuu)]

sign? would also solve the name length issue

[Michael Rothgang]

From a user's POV, I'd rather have user-facing tactics positivity and negativity. Internally, these might be implemented as some kind of sign tactic.

[Jovan Gerbscheid]

Would you still want to call it negativity if the goal was -bla < 0, where bla is some complicated expression which is positive by the positivity tactic?

[Michael Rothgang]

Yes - the goal is to prove something is negative after all. (And indeed, in the example you give, negativity should probably do something equivalent to positivity on bla.)