Qq/positivity confusion

Stream: metaprogramming / tactics

[Moritz Doll]

I've tried to write a positivity extension with Qq and I ran into a weird problem:

import Mathlib.Algebra.Order.Group.PosPart

namespace Mathlib.Meta.Positivity

open Qq Lean Meta LinearOrder

@[positivity PosPart.pos _]
def evalPosPart : PositivityExt where eval {u α} zα pα e := do
  match e with
  | ~q(@PosPart.pos _ $inst1 $a) =>
    let instαLattice ← synthInstanceQ q(Lattice $α)
    let instαAddGroup ← synthInstanceQ q(AddGroup $α)
    assertInstancesCommute
    return .nonnegative q(@posPart_nonneg $α $instαLattice $instαAddGroup $a)
  | _ => throwError "not PosPart.pos"

example {α : Type*} [Lattice α] [AddGroup α] (a : α) : 0 ≤ a⁺ := by positivity

end Mathlib.Meta.Positivity

The return fails with error:

type mismatch
  posPart_nonneg «$a»
has type
  0 ≤ «$a»⁺ : Prop
but is expected to have type
  0 ≤ «$e» : Prop

even though the matching ensures that these two are equal. I don't know how to use the matching hypothesis to make Qq happy and I haven't seen a similar issue in any of the other positivity extensions

[Yaël Dillies]

You're using the wrong function?

[Yaël Dillies]

See #10256

[Yaël Dillies]

Anyway, I have those extensions written. I can PR them

[Eric Wieser]

set_option autoImplicit false makes the error clearer (you're missing the import of PositivityExt)

[Eric Wieser]

To decode Yael's comment, you should be using posPart not PosPart.pos

[Eric Wieser]

So this works:

@[positivity posPart _]
def evalPosPart : PositivityExt where eval {u α} zα pα e := do
  match e with
  | ~q(@posPart _ $inst1 $inst2 $a) =>
    assertInstancesCommute
    return .nonnegative q(posPart_nonneg $a)
  | _ => throwError "not PosPart.pos"

[Yaël Dillies]

#10681

[Yaël Dillies]

There is a bug here: core q(inferInstance) q(inferInstance) a fails instead of returning none when no 0 ≤ a or 0 < a assumption is in context.

[Moritz Doll]

Thanks you. That was very silly of me.

[Moritz Doll]

Yael there are at least two instance where positivity should be able to replace explicit calls to posPart_nonneg and a third one where one needs a positivity-extension for integrals (I wrote a PR for that)

[Yaël Dillies]

You mean two occurrences in mathlib? I didn't know posPart was used at all yet.

[Moritz Doll]

yes, in MeasureTheory.Decomposition.Jordan and Probability.Martingale.Upcrossing

[Moritz Doll]

this is how I found posPart in the first place: I was search&replacing integral_nonneg and Upcrossing had these posPart_nonneg that we not used by positivity.