Could positivity handle sums of squares?

Stream: mathlib4

[Terence Tao]

I was expecting positivity to be able to directly establish

import Mathlib
import Mathlib.Algebra.BigOperators.Basic

open Finset
open BigOperators

example (n : ℕ) (a : ℕ → ℤ): 0 ≤ ∑ j in range n, a j^2 := by
  apply sum_nonneg
  intro j _
  positivity

without needing to explicitly invoke sum_nonneg. Would it be feasible to extend positivity to be able to handle this sort of expression? It's not a huge pain to add these extra two lines of code, but it would be a minor convenience not to have to do so. (Recently I had a whole stack of positivity conditions to verify and wanted to finish them all off with all_goals { positivity }, but this issue presented a speed bump in doing so.)

[Yaël Dillies]

I've tried exactly this in Lean 3 and failed! I am still hoping to crank up my metaprogramming fu and get positivity to work, but that hasn't happened yet.

[Yaël Dillies]

If you look through LeanAPAP, you will see that I make heavy use of positivity and that a bunch of calls could be shortened with a few extra positivity extensions.

[Yaël Dillies]

The reason this is harder to write than other extensions is because you need to introduce extra variables to the context, call positivity there, then zoom back.

[Heather Macbeth]

This was also proposed by @Moritz Doll soon after the tactic first appeared -- Moritz, did you ever try it? I still think it's a good idea ...

[Moritz Doll]

Heather Macbeth said:

This was also proposed by Moritz Doll soon after the tactic first appeared -- Moritz, did you ever try it? I still think it's a good idea ...

No, I did not. I don't have much time to spend on mathlib at the moment. I agree that it should be possible (and probably not too hard, the telescoping function should take care of introducing the variables just fine) - if nobody does it this week I might be motivated next weekend to look into this

[Alex J. Best]

Here is a basic version of this:

import Mathlib.Tactic.Positivity.Core
import Mathlib.Algebra.BigOperators.Order

open Finset
open BigOperators

open Qq
open Mathlib.Meta.Positivity Lean Meta

@[positivity Finset.sum _ _] def evalSum : PositivityExt where eval {u β2} zβ pβ e := do
  let ⟨v, l, r⟩ ← inferTypeQ' <| (Expr.getAppArgs (← withReducible (whnf e))).get! 1
  let .app (.app (.app (.app (.app f (β : Q(Type u))) (α : Q(Type u))) (a : Q(AddCommMonoid $β))) (s : Q(Finset $α))) (b : Q($α → $β)) ← withReducible (whnf e) | throwError "not sum"
  haveI' : $β =Q $β2 := ⟨⟩
  haveI' : $e =Q Finset.sum $s $b := ⟨⟩
  let (lhs, _, (rhs : Q($β))) ← lambdaMetaTelescope b
  let rb ← core zβ pβ rhs
  match rb with
  | .nonnegative pb => do
    let pα' ← synthInstanceQ (q(OrderedAddCommMonoid $β) : Q(Type u))
    assertInstancesCommute
    let pr : Q(∀ (i : $α), 0 ≤ $b i) ← mkLambdaFVars lhs pb
    pure (.nonnegative q(@sum_nonneg.{u, u} $α $β $pα' $b $s (fun i h => $pr i)))
  | _ => pure .none

set_option trace.Tactic.positivity true

lemma oops (n : ℕ) (a : ℕ → ℤ): 0 ≤ ∑ j in range n, a j^2 := by
  positivity

#print axioms oops

lemma oops' (n : ℕ) (a : ℕ → ℤ): 0 ≤ ∑ j in range n, ∑ i in range n, a j^2 + i ^ 2 := by
  positivity

it has some limitations (I couldn't get universes to play nice so I just assume u = v and hope for the best, it currently doesn't use the fact that the element lies in the finset being summed over (maybe that would help in some situations), and it only does nonnegativity, as for positivity we need to know the sum is nonempty etc

[Yaël Dillies]

A really important case to get right for strict positivity is when the sum is over a nonempty fintype. Can you hardcode that?

[Alex J. Best]

Yaël Dillies said:

A really important case to get right for strict positivity is when the sum is over a nonempty fintype. Can you hardcode that?

Sure!

import Mathlib.Tactic.Positivity.Core
import Mathlib.Algebra.BigOperators.Order

open Finset
open BigOperators

open Qq
open Mathlib.Meta.Positivity Lean Meta

@[positivity Finset.sum _ _] def evalSum : PositivityExt where eval {u β2} zβ pβ e := do
  let ⟨v, l, r⟩ ← inferTypeQ' <| (Expr.getAppArgs (← withReducible (whnf e))).get! 1
  let .app (.app (.app (.app (.app f (β : Q(Type u))) (α : Q(Type u))) (a : Q(AddCommMonoid $β))) (s : Q(Finset $α))) (b : Q($α → $β)) ← withReducible (whnf e) | throwError "not sum"
  haveI' : $β =Q $β2 := ⟨⟩
  haveI' : $e =Q Finset.sum $s $b := ⟨⟩
  let (lhs, _, (rhs : Q($β))) ← lambdaMetaTelescope b
  let rb ← core zβ pβ rhs

  let so : Option Q(Finset.Nonempty $s) ← do -- TODO if i make a typo it doesn't complain.?
    try {
      let fi ← synthInstanceQ (q(Fintype $α) : Q(Type u))
      let no ← synthInstanceQ (q(Nonempty $α) : Q(Prop))
      match s with
      | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $α)))
      | _ => pure none }
    catch e =>
      pure none
  match rb, so with
  | .nonnegative pb, _ => do
    let pα' ← synthInstanceQ (q(OrderedAddCommMonoid $β) : Q(Type u))
    assertInstancesCommute
    let pr : Q(∀ (i : $α), 0 ≤ $b i) ← mkLambdaFVars lhs pb
    pure (.nonnegative q(@sum_nonneg.{u, u} $α $β $pα' $b $s (fun i h => $pr i)))
  | .positive pb, .some (fi : Q(Finset.Nonempty $s)) => do
    let pα' ← synthInstanceQ (q(OrderedCancelAddCommMonoid $β) : Q(Type u))
    assertInstancesCommute
    let pr : Q(∀ (i : $α), 0 < $b i) ← mkLambdaFVars lhs pb
    pure (.positive q(@sum_pos.{u, u} $α $β $pα' $b $s (fun i h => $pr i) $fi))
  | _, _ => pure .none

set_option trace.Tactic.positivity true

lemma oops (n : ℕ) (a : ℕ → ℤ): 0 ≤ ∑ j in range n, a j^2 := by
  positivity

#print axioms oops

#check sum_pos

lemma oops' (n : ℕ) (a : ℕ → ℤ): 0 ≤ ∑ j : Fin 8, ∑ i in range n, a j^2 + i ^ 2 := by
  positivity


lemma oops'' (n : ℕ) (a : ℕ → ℤ): 0 < ∑ j : Fin (n + 1), (a j^2 + 1) := by
  positivity

[Yaël Dillies]

Finally, we really should let positivity look for local Finset.Nonempty assumptions. Heather and Mario previously complained that this was scope-creep, and I replied we could let positivity take extra assumptions (as in eg positivity [hs, ha.trans hab] where hs : s.Nonempty, ha : 0 < a, hab : a < b) that it is then allowed to search through, both as positivity assumptions and as assumptions that do not fit the positivity framework.

[Yaël Dillies]

Do you think you could hack something like that?

[Rob Lewis]

Yaël Dillies said:

Finally, we really should let positivity look for local Finset.Nonempty assumptions. Heather and Mario previously complained that this was scope-creep

This would be local to the Finset.sum positivity handler, right? Not sure I agree that this is scope creep, it seems reasonable enough

[Alex J. Best]

import Mathlib.Tactic.Positivity.Core
import Mathlib.Algebra.BigOperators.Order

open Finset
open BigOperators

open Qq
open Mathlib.Meta.Positivity Lean Meta

@[positivity Finset.sum _ _] def evalSum : PositivityExt where eval {u β2} zβ pβ e := do
  let ⟨v, l, r⟩ ← inferTypeQ' <| (Expr.getAppArgs (← withReducible (whnf e))).get! 1
  let .app (.app (.app (.app (.app f (β : Q(Type u))) (α : Q(Type u))) (a : Q(AddCommMonoid $β))) (s : Q(Finset $α))) (b : Q($α → $β)) ← withReducible (whnf e) | throwError "not sum"
  haveI' : $β =Q $β2 := ⟨⟩
  haveI' : $e =Q Finset.sum $s $b := ⟨⟩
  let (lhs, _, (rhs : Q($β))) ← lambdaMetaTelescope b
  let rb ← core zβ pβ rhs

  let so : Option Q(Finset.Nonempty $s) ← do -- TODO if i make a typo it doesn't complain.?
    try {
      let fi ← synthInstanceQ (q(Fintype $α) : Q(Type u))
      let no ← synthInstanceQ (q(Nonempty $α) : Q(Prop))
      match s with
      | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $α)))
      | _ => pure none }
    catch e => do
      let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
      pure (some (.fvar fv))
  match rb, so with
  | .nonnegative pb, _ => do
    let pα' ← synthInstanceQ (q(OrderedAddCommMonoid $β) : Q(Type u))
    assertInstancesCommute
    let pr : Q(∀ (i : $α), 0 ≤ $b i) ← mkLambdaFVars lhs pb
    pure (.nonnegative q(@sum_nonneg.{u, u} $α $β $pα' $b $s (fun i h => $pr i)))
  | .positive pb, .some (fi : Q(Finset.Nonempty $s)) => do
    let pα' ← synthInstanceQ (q(OrderedCancelAddCommMonoid $β) : Q(Type u))
    assertInstancesCommute
    let pr : Q(∀ (i : $α), 0 < $b i) ← mkLambdaFVars lhs pb
    pure (.positive q(@sum_pos.{u, u} $α $β $pα' $b $s (fun i h => $pr i) $fi))
  | _, _ => pure .none

set_option trace.Tactic.positivity true

lemma oops (n : ℕ) (a : ℕ → ℤ): 0 ≤ ∑ j in range n, a j^2 := by
  positivity

#print axioms oops

#check sum_pos

lemma oops' (n : ℕ) (a : ℕ → ℤ): 0 ≤ ∑ j : Fin 8, ∑ i in range n, a j^2 + i ^ 2 := by
  positivity


lemma oops'' (n : ℕ) (a : ℕ → ℤ): 0 < ∑ j : Fin (n + 1), (a j^2 + 1) := by
  positivity

lemma oops''' (n : ℕ) (a : ℕ → ℤ): 0 < ∑ j in ({1} : Finset ℕ), (a j^2 + 1) := by
  have : Finset.Nonempty {1} := singleton_nonempty 1
  positivity

[Yaël Dillies]

Yes. It would be local to the Finset.sum extension. In fact, mathlib already has a local positivity tactic which looks for local assumptions (note the three distinct uses of "local" in the past two sentences): docs3#tactic.positivity_szemeredi_regularity. I see that Kyle Miller translated it to a plain custom tactic: docs#SzemerediRegularity.Positivity.tacticSz_positivity

[Heather Macbeth]

Yaël Dillies said:

Finally, we really should let positivity look for local Finset.Nonempty assumptions. Heather and Mario previously complained that this was scope-creep,

To be more precise: Mario previously complained. (You're talking about !3#16632, right?). But if Mario had concerns I think we should take them seriously ...

[Terence Tao]

Just a note that I am trying out Alex's positivity extension on my project https://github.com/teorth/symmetric_project and so far it is working fine. (Thanks to Alex for the pull request.) Will let people know here if there are issues.

I wonder if the same code that now lets positivity handle sums and products could also handle universal quantifiers? For instance, in

example : ∀ (n : ℤ), 0 ≤ n^2 := by
  intro _
  positivity

whether positivity could perform the intro automatically.

[Kevin Buzzard]

Ooh is that scope creep? :-)

[Yaël Dillies]

How should I have interpreted your first comment on that same PR then, Heather?

[Heather Macbeth]

@Yaël Dillies I still don't think $0<a-b$ is in scope for positivity, but personally I don't object to having Finset.nonempty hypotheses being used for card-positivity, it seems in the same spirit as other positivity. (But if Mario does, I think we should discuss it seriously.)

[Yaël Dillies]

Ah! Then what difference are you drawing between those two scenarios?

[Heather Macbeth]

To me, positivity of $0<a-b$ given an ambient $b<a$ hypothesis does not follow the positivity spec of "clear from the syntax of the epxression".

[Yaël Dillies]

Does it not? Would you then rather expect an extension for 0 < a → b ≤ 0 → 0 < a - b?

[Yaël Dillies]

Incidentally, Bhavik and I were talking about making positivity support ≤ 0 and < 0 assumptions. This actually shows up in our calculations and adding the logic to positivity is pretty easy without slowdown.

[Yaël Dillies]

I must also add that in most cases we have a goal of the form 0 < a - 1 and an assumption 1 < a. Namely, b is usually fixed.

[Terence Tao]

Kevin Buzzard said:

Ooh is that scope creep? :-)

Well, yes, but if we are already automatically clearing Finset.sum_nonneg; intros and Finset.prod_nonneg; intros, why not also just automatically clear intros? There are plenty of other tools besides Finset.sum_nonneg and Finset.prod_nonneg that produce universally quantified positivity hypotheses; in my own project I have encountered ConvexOn.map_sum_le, Real.finset_prod_rpow, and geom_mean_le_arith_mean_weightedfor instance, and I am sure there are many others. I have taken to using a whole bunch of these tools in a row to manipulate various complex inequalities or equalities, accumulating a stack of a dozen positivity hypotheses outstanding, and it would be convenient to clear them all at once with all_goals {positivity}.

[Heather Macbeth]

@Terence Tao It's possible to write a tactic of the form "do the obvious logical stuff, then run tactic X" using the tactic aesop.
Here's my quick attempt, which I am sure others can improve:

first file contains

import Aesop

declare_aesop_rule_sets [Positivity]

macro (name := lpositivity) "lpositivity" c:Aesop.tactic_clause* : tactic =>
`(tactic|
  aesop $c* (options := { introsTransparency? := some .default, terminal := true })
  (rule_sets [$(Lean.mkIdent `Positivity):ident]))

second file contains

import Mathlib.Tactic.Positivity
import [first file]

open Lean Elab Tactic
@[aesop safe tactic (rule_sets [Positivity])]
def PositivityForAesop : TacticM Unit :=
  liftMetaTactic fun g => do Mathlib.Meta.Positivity.positivity g; pure []

Then this works:

example : ∀ (n : ℤ), 0 ≤ n^2 := by lpositivity
-- `lpositivity` for "logic + positivity"

[Heather Macbeth]

It will also solve e.g.

example (n m : ℤ) : 0 ≤ n^2 ∧ 0 ≤ m ^ 4 + 3 := by lpositivity

[Jireh Loreaux]

You could also just do this if you only care about introducing new variables: all_goals {intros; positivity}, but Heather's aesop configuration would be a more sophisticated approach that can do more.

[Heather Macbeth]

And if you want to abbreviate Jireh's version, you can name it with a macro:

import Mathlib.Tactic.Positivity

macro "lpositivity" : tactic => `(tactic | (intros; positivity))

example : ∀ (n : ℤ), 0 ≤ n^2 := by lpositivity
example (n : ℤ) : 0 ≤ n^2 := by lpositivity

[Terence Tao]

Jireh Loreaux said:

You could also just do this if you only care about introducing new variables: all_goals {intros; positivity}, but Heather's aesop configuration would be a more sophisticated approach that can do more.

Ah, I didn't realize that intros doesn't fail if there is nothing to introduce. That solves my immediate use case nicely - thanks!

There could still be some value I think though in a more aggressive cousin positivity! of positivity that applies a few more "obvious" reductions in a search for establishing positivity.

[Jireh Loreaux]

If you want to use a tactic that could fail (e.g., intro) then you could do it this way: (try intro); positivity.

[Jireh Loreaux]

I think the solution to that is ultimately aesop as Heather suggests, but I think @Jannis Limperg is working on a method to allow tactic calls within aesop, am I correct?

[Mario Carneiro]

To clarify what I meant about scope creep, I think it is fine if positivity uses typeclass inference for nonempty assumptions, but having the nonempty subgoals be mutually recursive with other kinds of goals is going to make it a kitchen sink tactic because there is no clear bound on what subgoals should be considered, and at that point you have just reinvented apply_rules.

[Yaël Dillies]

Okay but surely depth 1 is not scope-creep?

[Jannis Limperg]

Jireh Loreaux said:

I think the solution to that is ultimately aesop as Heather suggests, but I think Jannis Limperg is working on a method to allow tactic calls within aesop, am I correct?

It's already possible to call arbitrary tactics in Aesop (all rules are ultimately tactics). It's just that the syntax is currently very ugly.

[Yaël Dillies]

@Alex J. Best, I just tried your positivity extension but it seems to mishandle universes. In my use cases, I get errors of the form

application type mismatch
  @sum_nonneg ι
argument has type
  Type u_1
but function has type
  ∀ {ι N : Type} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ i ∈ s, 0 ≤ f i) → 0 ≤ ∑ i ∈ s, f i

[Yaël Dillies]

Here's a MWE:

import Mathlib.Analysis.Normed.Field.Basic

open Finset
open BigOperators

open Qq Lean Meta

@[positivity Finset.sum _ _]
def Mathlib.Meta.Positivity.evalSum : PositivityExt where eval {u β2} zβ pβ e := do
  let ⟨_v, _l, _r⟩ ← inferTypeQ' <| (Expr.getAppArgs (← withReducible (whnf e))).get! 1
  let .app (.app (.app (.app (.app _f (β : Q(Type u))) (α : Q(Type u))) (_a : Q(AddCommMonoid $β)))
    (s : Q(Finset $α))) (b : Q($α → $β)) ← withReducible (whnf e) | throwError "not `Finset.sum`"
  haveI' : $β =Q $β2 := ⟨⟩
  haveI' : $e =Q Finset.sum $s $b := ⟨⟩
  let (lhs, _, (rhs : Q($β))) ← lambdaMetaTelescope b
  let rb ← core zβ pβ rhs

  let so : Option Q(Finset.Nonempty $s) ← do -- TODO: if I make a typo it doesn't complain?
    try {
      let _fi ← synthInstanceQ (q(Fintype $α) : Q(Type u))
      let _no ← synthInstanceQ (q(Nonempty $α) : Q(Prop))
      match s with
      | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $α)))
      | _ => pure none }
    catch _e => do
      let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
      pure (some (.fvar fv))
  match rb, so with
  | .nonnegative pb, _ => do
    let pα' ← synthInstanceQ (q(OrderedAddCommMonoid $β) : Q(Type u))
    assertInstancesCommute
    let pr : Q(∀ (i : $α), 0 ≤ $b i) ← mkLambdaFVars lhs pb
    pure (.nonnegative q(@sum_nonneg.{u, u} $α $β $pα' $b $s (fun i _h => $pr i)))
  | .positive pb, .some (fi : Q(Finset.Nonempty $s)) => do
    let pα' ← synthInstanceQ (q(OrderedCancelAddCommMonoid $β) : Q(Type u))
    assertInstancesCommute
    let pr : Q(∀ (i : $α), 0 < $b i) ← mkLambdaFVars lhs pb
    pure (.positive q(@sum_pos.{u, u} $α $β $pα' $b $s (fun i _h => $pr i) $fi))
  | _, _ => pure .none

example {ι : Type*} (s : Finset ι) (f : ι → ℝ) : 0 ≤ ∑ i in s, ‖f i‖ := by positivity -- fails

[Yaël Dillies]

This is very easily explained by the (β : Q(Type u))) (α : Q(Type u))) in the second line of your extension, but I don't know how one can pattern-match on universe levels to fix it.

[Alex J. Best]

My recollection is that I also couldn't get things to work more universe polymorphically which is why I hardcoded it. I can make another attempt sometime but I'm not sure I will fare any better than the first time around

[Yaël Dillies]

It would be quite annoying for me to force everything in Type, especially because I'm writing code that I hope will end up in mathlib, so I'd greatly appreciate any effort to save universe polymorphism!

[Yaël Dillies]

Maybe @Gabriel Ebner can impart us some wisdom too.

[Yaël Dillies]

Update: I managed to make it polymorphic thanks to Mario's advice! I just replaced the first two let with

  let .app (.app (.app (.app (.app (.const _ [_, v]) (β : Q(Type u))) (α : Q(Type v)))
    (_a : Q(AddCommMonoid $β))) (s : Q(Finset $α))) (b : Q($α → $β)) ← withReducible (whnf e)

and now everything works.