positivity regression

Stream: mathlib4

[Yaël Dillies]

I have an issue with docs#Mathlib.Tactic.Positivity.evalMul (which came from @Mario Carneiro's #578). This line means that the extension only works in StrictOrderedSemirings, except that docs#mul_nonneg works more generally in ordered semirings.

[Yaël Dillies]

This is relevant to me since I am using positivity to prove goals of the form 0 ≤ f * g where f g : ι → ℝ, and ι → ℝ is not a strictly ordered semiring.

[Yaël Dillies]

Is there an easy fix?

[Ruben Van de Velde]

So what's the issue? Does weakening that line break its support for 0 < goals?

[Eric Wieser]

Isn't the easy fix replacing that synthesis line?

[Ruben Van de Velde]

If that's the case, could we move the synthesis into each of the match arms?

[Yaël Dillies]

That's what I would think. But I have no Lean 4 metaprogramming experience, and even less experience with Qq!

[Eric Wieser]

I think we might need to tweak the code slightly to look more like what I wrote in #7089

[Eric Wieser]

That is, to find the initial instances by unification so that we can call core on them, before looking for stronger instances in the match arms

[Yaël Dillies]

While I'm at it, is there any obvious reason why the following extension doesn't work?

import Mathlib.Data.Rat.Order
import Mathlib.Tactic.Positivity

lemma Rat.num_ne_zero {q : ℚ} : q.num ≠ 0 ↔ q ≠ 0 := Rat.num_eq_zero.not

namespace Mathlib.Meta.Positivity
open Lean Meta Qq Function Rat

alias ⟨_, num_pos_of_pos⟩ := num_pos_iff_pos
alias ⟨_, num_nonneg_of_nonneg⟩ := num_nonneg_iff_zero_le
alias ⟨_, num_ne_zero_of_ne_zero⟩ := num_ne_zero

/-- The `positivity` extension which identifies expressions of the form `Rat.num a`,
such that `positivity` successfully recognises `a`. -/
@[positivity (Rat.num _)]
def evalRatnum : PositivityExt where eval {_u _α} _zα _pα e := do
  let .app _ (a : Q(ℚ)) ← withReducible (whnf e) | throwError "not Rat.num"
  let zα' : Q(Zero ℚ) := q(inferInstance)
  let pα' : Q(PartialOrder ℚ) := q(inferInstance)
  let ra ← core zα' pα' a
  match ra with
  | .positive pa =>
    pure (.positive (q(num_pos_of_pos $pa) : Expr))
  | .nonnegative pa =>
    pure (.nonnegative (q(num_nonneg_of_nonneg $pa) : Expr))
  | .nonzero pa =>
    pure (.nonzero (q(num_ne_zero_of_ne_zero $pa) : Expr))
  | .none =>
    pure .none

/-- The `positivity` extension which identifies expressions of the form `Rat.den a`. -/
@[positivity Rat.den _]
def evalRatden : PositivityExt where eval {_u _α} _zα _pα e := do
  let .app _ (a : Q(ℚ)) ← withReducible (whnf e) | throwError "not Rat.den"
  pure (.positive (q(den_pos $a) : Expr))

variable {q : ℚ}

example (hq : 0 < q) : 0 < q.num := by positivity -- failed
example (hq : 0 ≤ q) : 0 ≤ q.num := by positivity -- failed
example (hq : q ≠ 0) : q.num ≠ 0 := by positivity -- failed
example : 0 < q.den := by positivity -- failed

end Mathlib.Meta.Positivity

[Yaël Dillies]

(actually, feel free to move this to #metaprogramming / tactics, I forgot that stream existed)

[Yaël Dillies]

Update: Just added my attempt for Rat.den, which is even easier but which I still failed miserably :sob:

[Eric Wieser]

I'll have a go at those in half an hour

[Eric Wieser]

This works:

import Mathlib.Data.Rat.Order
import Mathlib.Tactic.Positivity

namespace Mathlib.Meta.Positivity
open Lean Meta Qq Function Rat

alias ⟨_, num_pos_of_pos⟩ := num_pos_iff_pos
alias ⟨_, num_nonneg_of_nonneg⟩ := num_nonneg_iff_zero_le
alias ⟨_, num_ne_zero_of_ne_zero⟩ := num_ne_zero

/-- The `positivity` extension which identifies expressions of the form `Rat.num a`,
such that `positivity` successfully recognises `a`. -/
@[positivity (Rat.num _)]
def evalRatnum : PositivityExt where eval {_u _α} _zα _pα (e : Q(ℤ)) := do
  let ~q(Rat.num $a) := e | throwError "not Rat.num"
  let zα' : Q(Zero ℚ) := q(inferInstance)
  let pα' : Q(PartialOrder ℚ) := q(inferInstance)
  -- TODO: what's the right way to write these `: Expr`s?
  match ← core zα' pα' a with
  | .positive pa =>
    return .positive (q(num_pos_of_pos $pa) : Expr)
  | .nonnegative pa =>
    return .nonnegative (q(num_nonneg_of_nonneg $pa) : Expr)
  | .nonzero pa =>
    return .nonzero (q(num_ne_zero_of_ne_zero $pa) : Expr)
  | .none =>
    pure .none

/-- The `positivity` extension which identifies expressions of the form `Rat.den a`. -/
@[positivity Rat.den _]
def evalRatden : PositivityExt where eval {_u _α} _zα _pα (e : Q(ℕ)) := do
  let ~q(Rat.den $a) := e | throwError "not Rat.den"
  return .positive (q(den_pos $a) :)

variable {q : ℚ}

example (hq : 0 < q) : 0 < q.num := by positivity -- ok!
example (hq : 0 ≤ q) : 0 ≤ q.num := by positivity -- ok!
example (hq : q ≠ 0) : q.num ≠ 0 := by positivity -- ok!
example : 0 < q.den := by positivity -- ok!

end Mathlib.Meta.Positivity

[Eric Wieser]

These : Exprs feel like one of:

• A design flaw in PositivityExt
• A Qq bug
• Me not knowing what I'm doing with Qq

[Yaël Dillies]

So my mistake was the match?

[Yaël Dillies]

Aaah, I see. Am I right in thinking it's because I didn't type-ascript e, so Qq couldn't derive the type-correctness of my subsequent match?

[Eric Wieser]

Yes, the match isn't even well-typed if you don't first lie about the type of e

[David Renshaw]

in what sense is that ascription a "lie"?

[David Renshaw]

My understanding of (e : Q(ℕ)) is that we are asserting that e is an expression of type ℕ.

[Eric Wieser]

Right, but we've been told it's of type _α : Q(Type u) (we also aren't told that u = level.zero)

[Eric Wieser]

Which we're ignoring because we "know better" (about the internals of the positivity tactic and how it promises to call us)

[Mario Carneiro]

it's more about the fact that your let ~q(Rat.num $a) := e implies some things about u and alpha which the type system doesn't know

[Eric Wieser]

Is it something that the type system could know?

[Mario Carneiro]

working on it

[Eric Wieser]

It seems like we could refactor positivity extensions somehow so that the match and lookup are simultaneous

[Yury G. Kudryashov]

positivity extension for docs#Real.sqrt doesn't work for me.

[Yury G. Kudryashov]

How do I debug it?

[Yury G. Kudryashov]

More details:

example (x : ℝ) (hx : 0 < x) : 0 < Real.sqrt x := by positivity -- works
example (x : ℝ) : 0 ≤ Real.sqrt x := by positivity -- fails

[Yury G. Kudryashov]

It looks like the function doesn't get past the let ra ← core zα' pα' a line without (_ : 0 < x).

[Yury G. Kudryashov]

Probably, the call to core fails instead of returning none.

[David Renshaw]

Yep:
https://github.com/leanprover-community/mathlib4/blob/b56efa53d7479fda9740f364170cbaef34699dee/Mathlib/Tactic/Positivity/Core.lean#L304

[David Renshaw]

This fixes it:

diff --git a/Mathlib/Data/Real/Sqrt.lean b/Mathlib/Data/Real/Sqrt.lean
index 970b33638..ca73aab94 100644
--- a/Mathlib/Data/Real/Sqrt.lean
+++ b/Mathlib/Data/Real/Sqrt.lean
@@ -380,7 +380,7 @@ def evalSqrt : PositivityExt where eval {_ _} _zα _pα e := do
   let (.app _ (a : Q(Real))) ← whnfR e | throwError "not Real.sqrt"
   let zα' ← synthInstanceQ (q(Zero Real) : Q(Type))
   let pα' ← synthInstanceQ (q(PartialOrder Real) : Q(Type))
-  let ra ← core zα' pα' a
+  let ra ← catchNone <| core zα' pα' a
   assertInstancesCommute
   match ra with

[David Renshaw]

But makes me wonder why the throwNone exists in the first place

[David Renshaw]

mathlib4#8014

[Yury G. Kudryashov]

Thanks a lot!