writing a positivity extension

Stream: mathlib4

[Jireh Loreaux]

I'm trying to write a positivity extension for docs#StarOrderedRing to make use of things like docs#mul_star_self_nonneg and docs#conjugate_nonneg. By cargo cult coding from the basic positivity extensions, I can make the former work fairly easily. However, when I try to generalize to make it handle multiple forms simultaneously by matching on the expression, I get errors. What am I doing wrong here in the second attempt?

import Mathlib

namespace Mathlib.Meta.Positivity
open Lean Meta Expr Qq

/-- The `positivity` extension which identifies expressions of the form `star a * a`. -/
@[positivity _ * _, Mul.mul _ _] def evalStarMul : PositivityExt where eval {u α} zα pα e := do
  let _a ← synthInstanceQ q(NonUnitalSemiring $α)
  let _a' ← synthInstanceQ q(StarOrderedRing $α)
  assumeInstancesCommute
  let .app (.app (f : Q($α → $α → $α)) (.app (s : Q($α → $α)) (a : Q($α)))) (b : Q($α)) ← withReducible (whnf e)
    | throwError "not *"
  let _e_eq : $e =Q $f ($s $a) $b := ⟨⟩
  let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ (u := u.succ) f q(HMul.hMul)
  let ⟨_s_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ (u := u.succ) s q(Star.star)
  let ⟨_a_eq_b⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ (u := u) a b
  pure (.nonnegative q(star_mul_self_nonneg $a))

example (a : ℝ) : 0 ≤ star a * a := by
  positivity -- works! yay!

@[positivity _ * _, Mul.mul _ _] def evalStarMul' : PositivityExt where eval {u α} zα pα e := do
  let e : Q($α) ← whnfR e
  let _inst₁ ← synthInstanceQ q(NonUnitalSemiring $α)
  let _inst₂ ← synthInstanceQ q(StarOrderedRing $α)
  assumeInstancesCommute
  match e with
  | ~q((star $a) * $b) =>
    let ⟨_a_eq_b⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ (u := u) a b
    let _e_eq : $e =Q (star $a) * $a := ⟨⟩
    pure (.nonnegative q(star_mul_self_nonneg $a))
    /-
    type mismatch
      star_mul_self_nonneg «$a»
    has type
      0 ≤ star «$a» * «$a» : Prop
    but is expected to have type
      0 ≤ $e✝ : Prop
    -/

[Jireh Loreaux]

Separate but connected question: is it possible to make positivity attributes scoped? when I tried to do that I got "invalid attribute positivity, must be global"

[Yaël Dillies]

It was the case in Lean 3. Not anymore :sad:

[Jireh Loreaux]

nevermind, this is just because I called it e again in the first let so the original was inaccessible. Ignore the noise.

[Jireh Loreaux]

Why can't it be scoped anymore?

[Yaël Dillies]

No clue. Probably it simply hasn't been implemented?

[Mario Carneiro]

scoped extensions have to be implemented individually, it's just a matter of implementation work

[Mario Carneiro]

it's also a bit slower/more complicated than global-only attributes

[Scott Morrison]

See Std.Tactic.LabelAttr for a minimal example of how to set up removable attributes.

(These label attributes are for cases where we're not doing any work when adding the attribute: we just need to know if it is there or not.)

Someone needs to add this functionality to the positivity attribute.

[Frédéric Dupuis]

(deleted)

[Yury G. Kudryashov]

I see that most positivity extensions fist tell the expression(s) they can handle in the @[positivity] argument, then match using Qq. Why do we need this?

[David Renshaw]

The match pattern in the attribute dictates when the extension is activated (via a DiscrTree lookup). The match inside the body is typically to extract subterms.

[Yury G. Kudryashov]

It would be nice to have an attribute that generates correct code for simple cases like src#Mathlib.Meta.Positivity.evalENNRealtoReal

[Yury G. Kudryashov]

In #9545, @Eric Wieser suggested that we use a different pattern in a very similar case.

[Yury G. Kudryashov]

And a generic function looks like a better way to handle this (rather than going through the library and making sure that all functions follow the same pattern)

[Eric Wieser]

I think part of the reason is that a DiscrTree lookup is not guaranteed to be a perfect match, and so we have to do a second check to be sure

[Yaël Dillies]

I don't know how relevant this is here, but note that you can overapply functions, eg you can do @[positivity (_ * _) _] to match applied pointwise multiplication.

[Eric Wieser]

Related to this conversation; #10196 starts cleaning up some of the matches to exploit the fixes in Lean v4.6.0-rc1.