Positivity with hypotheses

Stream: Is there code for X?

[Alex Meiburg]

Today I tried using positivity for the first time, but it didn't work, and maybe I misunderstood how it works. I had the following state:

α: Type u_1
inst✝¹: LinearOrderedField α
P: α[X]
η: α
inst✝: DecidableEq α
hη: η > 0
dp1: ℕ
hP₁: coeff P dp1 < 0
hP₀: coeff P (dp1 + 1) > 0
⊢ 0 < coeff P (dp1 + 1) * η - coeff P dp1

I was expecting positivity to look at the expression coeff P dp1 and see that hP₁ guarantees that it's negative, etc. and the product of two positive numbers is positive, and a positive number minus a negative is a positive, qed. I guess that positivity doesn't use hypotheses? Any tips?

[Alex Meiburg]

To be clear, this isn't a hard one to solve.

have := mul_pos hP₀ hη
linarith

closes the goal. Just slightly disappointed. :)
Side note: it's odd that positivity only handles 0 < x, but not x < y or even x < 0.

[Kevin Buzzard]

#mwe ? (that way people will find it easier to debug)

[Alex Meiburg]

import Mathlib.Data.Real.Basic
import Mathlib.Data.Polynomial.Basic
import Mathlib.Data.Polynomial.RingDivision

open Polynomial

variable {α : Type*} [LinearOrderedField α] (P : Polynomial α) {η : α} [DecidableEq α]

lemma demo (hη : η > 0) (dp1 : ℕ) (hP₁ : coeff P dp1 < 0) (hP₀: coeff P (dp1 + 1) > 0)
  : 0 < coeff P (dp1 + 1) * η - coeff P dp1 := by
    -- have := mul_pos hP₀ hη
    -- linarith
    sorry

[Kevin Buzzard]

Here's the step it's stuck on (the issue is not hypotheses, positivity deals with these fine).

example (a b : ℝ) (ha : 0 < a) (hb : b < 0) : 0 < a - b := by positivity -- fails

[Ruben Van de Velde]

I thought the idea was that positivity dealt with things that are "structurally" positive, so subtraction is out of scope?

[Kevin Buzzard]

BTW

lemma demo (hη : η > 0) (dp1 : ℕ) (hP₁ : coeff P dp1 < 0) (hP₀: coeff P (dp1 + 1) > 0) :
    0 < coeff P (dp1 + 1) * η - coeff P dp1 := by
  nlinarith

[Kevin Buzzard]

Ruben Van de Velde said:

I thought the idea was that positivity dealt with things that are "structurally" positive, so subtraction is out of scope?

example (a b : ℝ) (ha : 0 < a) (hb : 0 < b) : 0 < a + b := by
  positivity

works but maybe subtraction is feature creep?

[Alex Meiburg]

Neat! I didn't know about nlinarith. It's always disappointingly hard to find a list of these great tactics :upside_down:

[Alex Meiburg]

The way I understood it, positivity recursively decides terms to be some subset of {positive, negative, zero} and then works its way up from there. Seems like it should be straightforward to add a rule that {positive,zero}-{negative,zero} is {positive,zero} and {positive}-{negative} is {negative}, no?

Maybe I should learn some more lean so I could do that...

[Alex Meiburg]

Oh, I misremembered. It's "positive", "nonnegative", "nonzero", or "none".

[Alex Meiburg]

@[positivity _ / _] def evalDiv : PositivityExt where eval {u α} zα pα e := do
  let .app (.app (f : Q($α → $α → $α)) (a : Q($α))) (b : Q($α)) ← withReducible (whnf e)
    | throwError "not /"
  let _e_eq : $e =Q $f $a $b := ⟨⟩
  let _a ← synthInstanceQ (q(LinearOrderedSemifield $α) : Q(Type u))
  assumeInstancesCommute
  let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ (u := u.succ) f q(HDiv.hDiv)
  let ra ← core zα pα a; let rb ← core zα pα b
  match ra, rb with

ha! nope. Nope, I'm messing around with that. No idea. :)

[Matt Diamond]

It's always disappointingly hard to find a list of these great tactics

mathlib 3 has https://leanprover-community.github.io/mathlib_docs/tactics.html, not sure if there's a similar page for mathlib 4

[Richard Copley]

There was some recent discussion here.

[Yaël Dillies]

Certainly I'd be happy with positivity handling negative inputs. It makes the logic of extensions slightly more complicated, but it does let us handle more cases that actually show up in practice.