bug in `positivity`?

Stream: mathlib4

[Heather Macbeth]

@Gabriel Ebner 's PR !4#2685 rewrites positivity thanks to some very nice new Qq functionality. It seems to have broken certain positivity applications, though. Here is a test case: a positivity call occurring as a discharger inside solve_by_elim is broken.

It's not broken when I try to replicate the behaviour with the positivity call outside the solve_by_elim application, so I'm having trouble tracking it down further.

import Mathlib.Tactic.SolveByElim
import Mathlib.Tactic.Positivity

open Lean Meta Mathlib

attribute [dummy_label_attr] le_refl add_le_add mul_le_mul_of_nonneg_right

-- works
example {x y : ℤ} (hx : x ≥ 12) : y + x * x ≥ y + 12 * x := by
  apply_rules only [hx] using dummy_label_attr
  positivity

def PositivityDischarge (g : MVarId) : MetaM (Option (List MVarId)) :=
do withTransparency .reducible (Meta.Positivity.positivity g); pure (some []) <|> pure none

-- works before #2685, fails on #2685 with "not a positivity goal"
example {x y : ℤ} (hx : x ≥ 12) : y + x * x ≥ y + 12 * x := by
  solve_by_elim (config := { discharge := PositivityDischarge }) only [hx] using dummy_label_attr

[Gabriel Ebner]

This is the goal that positivity is called on. I'm not sure how this worked before.

example {x y : ℤ} (hx : x ≥ 12) : False := by positivity

[Heather Macbeth]

It used to be called on 0 ≤ x (to make the mul_le_mul_of_nonneg_right application work).

[Heather Macbeth]

That is, apply mul_le_mul_of_nonneg_right generates two subgoals and positivity discharged one of them.

[Gabriel Ebner]

This doesn't work either:

example {x y : ℤ} (hx : x ≥ 12) : x ≤ 0 := by positivity

[Heather Macbeth]

Wait, that's with x negative though!

[Gabriel Ebner]

Oh :face_palm:

[Gabriel Ebner]

Apparently, it can't prove that two typeclass instances are defeq:

[isDefEq] ❌ CommMonoidWithZero.toZero =?= MonoidWithZero.toZero

[Heather Macbeth]

I just reached the same conclusion myself, and had come over to report it :-)

[Gabriel Ebner]

Fixed:

import Mathlib.Tactic.Positivity
open Lean Meta Mathlib

attribute [dummy_label_attr] le_refl add_le_add mul_le_mul_of_nonneg_right

def PositivityDischarge (g : MVarId) : MetaM (Option (List MVarId)) := do
  withDefault (Meta.Positivity.positivity g)
  pure (some [])

example {x y : ℤ} (hx : x ≥ 12) : y + x * x ≥ y + 12 * x := by
  solve_by_elim (config := { discharge := PositivityDischarge }) only [hx] using dummy_label_attr

[Heather Macbeth]

Thank you! I don't understand the fix, though -- is it the withDefault? What does that do?

[Heather Macbeth]

It replaces the withTransparency .reducible in my version?

[Heather Macbeth]

Or do I want them both?

[Gabriel Ebner]

Yes, it's defined as withTransparency .default

[Gabriel Ebner]

(There's also withReducible)

[Gabriel Ebner]

The withReducible is too strong, positivity expect(s/ed) the transparency to be default. It compares a lot of type class instances using isDefEq (thus requiring default transparency), and adds withReducible itself.

[Mario Carneiro]

is this what that assertInstancesCommute macro does?

[Mario Carneiro]

because if so I would like to remove it from the places it's been added and put assumeInstancesCommute instead

[Gabriel Ebner]

Yes, the assertInstancesCommute macro adds isDefEq calls.

[Gabriel Ebner]

because if so I would like to remove it from the places it's been added and put assumeInstancesCommute instead

Why?

[Mario Carneiro]

because that's the number one performance issue in these tactics

[Mario Carneiro]

plus asserting that the instances themselves are equal is more than needed in most cases

[Mario Carneiro]

we only need to know that some projections off the instances are equal

[Mario Carneiro]

If this defeq call saved work later that would be a different situation, but here it is pure overhead

[Gabriel Ebner]

We don't check that the projections are equal though.

[Gabriel Ebner]

The result of isDefEq is also cached.

[Mario Carneiro]

no, we just go right ahead and construct the term and it crashes and burns in the kernel if it's not defeq

[Mario Carneiro]

I don't think improving the error message when there is an instance diamond is worth the performance degradation in normal uses of the tactic

[Mario Carneiro]

because you will be breaking out a debugger when something goes wrong in these tactics in any case

[Mario Carneiro]

yes, the result of isDefEq is cached, that's what I tell myself but the profiler doesn't lie, it is very hot code

[Gabriel Ebner]

There's plenty of cases with type tags like WithTop etc. where you can run into noncanonical instances.

[Mario Carneiro]

if the instances are not defeq then we're going to fail anyway

[Gabriel Ebner]

because if so I would like to remove it from the places it's been added and put assumeInstancesCommute instead

isDefEq is obviously hot, because it also does unification with lots of backtracking, has super expensive nested TC synthesis etc. All of this doesn't happen here.

[Mario Carneiro]

I mean, I ran a profiler with and without the isDefEq call and it was a significant improvement

[Mario Carneiro]

this is how ring was originally written after all

[Gabriel Ebner]

In any case, there's an assumeInstancesCommute now.