slow `positivity`

Stream: mathlib4

[Heather Macbeth]

I have a positivity call that seems very slow. Maybe an expert (@David Renshaw @Mario Carneiro ?) could look at it? Or perhaps I could do some diagnosis myself if someone can suggest some tools (e.g. is there a way to time how long variations on this take)?

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

example {a b : ℚ} (h1 : a ≥ 0) (h2 : b ≥ 0) (h3 : a + b ≤ 8) :
    0 ≤ 2 * b ^ 2 + a ^ 2 := by
  positivity

[David Renshaw]

It apparently spends a long time trying to decide whether 2 * b^2 + a^2 is definitionally equal to 8:

[Meta.isDefEq] [7.146166s] ❌ 2 * b ^ 2 + a ^ 2 =?= 8
  [Meta.isDefEq] [7.146093s] ❌ instHAdd.1 (2 * b ^ 2) (a ^ 2) =?= Rat.instOfNatRat.1
    [Meta.isDefEq] [7.146072s] ❌ Add.add (2 * b ^ 2) (a ^ 2) =?= ↑(Int.ofNat 8)
      [Meta.isDefEq] [7.146044s] ❌ Add.add (2 * b ^ 2) (a ^ 2) =?= IntCast.intCast (Int.ofNat 8)
        [Meta.isDefEq] [7.146019s] ❌ Rat.instAddRat.1 (2 * b ^ 2) (a ^ 2) =?= Rat.instIntCastRat.1 (Int.ofNat 8)
          [Meta.isDefEq] [7.146008s] ❌ Rat.add (2 * b ^ 2) (a ^ 2) =?= Rat.ofInt (Int.ofNat 8)
            [Meta.isDefEq] [7.145997s] ❌ Rat.add (2 * b ^ 2) (a ^ 2) =?= Rat.mk' (Int.ofNat 8) 1
              [Meta.isDefEq] [0.000000s] ✅ ℚ =?= ℚ
              [Meta.isDefEq] [1.434544s] ❌ (Rat.add (2 * b ^ 2) (a ^ 2)).num =?= Int.ofNat 8
                [Meta.isDefEq] [1.434532s] ❌ (Rat.add (2 * b ^ 2) (a ^ 2)).1 =?= Int.ofNat 8
                  [Meta.isDefEq.onFailure] [0.956389s] ❌ (Rat.add (2 * b ^ 2) (a ^ 2)).1 =?= Int.ofNat 8
...

[David Renshaw]

ah, with_reducible positivity goes a lot faster

[David Renshaw]

(so, similar to https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/congr.20tactic.20hitting.20max.20recursion.20depth/near/322619083 )

[David Renshaw]

This takes a long time to fail:

example {a b : ℚ} : 2 * b^2 + a^2 = 8 := rfl

[David Renshaw]

A bit more minimal:

import Mathlib.Data.Rat.Basic

-- I expect this to fail quickly with a `type mismatch` error or similar.
-- Instead, I get, after waiting many seconds:
--   timeout at 'whnf', maximum number of heartbeats (200000) has been reached
example {a : ℚ} : 2 * a^2 + a = 8 := rfl

[Sebastien Gouezel]

Would lean4#2003 be useful here?

[Kevin Buzzard]

That should be a meme

[James Gallicchio]

image.png as requested

[David Renshaw]

even more minimal

import Mathlib.Data.Rat.Basic

-- I expect this to fail quickly with a `type mismatch` error or similar.
-- Instead, I get, after waiting many seconds:
--   timeout at 'whnf', maximum number of heartbeats (200000) has been reached
example {a : ℚ} : 1 * a^2 + 1 = 0 := rfl

[Mario Carneiro]

what does #whnf do on that example?

[David Renshaw]

what exact syntax do you want me to type? I'm unfamiliar with #whnf

[Mario Carneiro]

#whnf is like #simp, #eval, etc you give it a term and it whnfs it

[Mario Carneiro]

import Mathlib.Data.Rat.Basic
variable {a : ℚ}
#whnf 1 * a^2 + 1

I guess

[David Renshaw]

import Mathlib.Data.Rat.Basic

variable (a : ℚ)
#whnf 1 * a^2 + 1
/-
Decidable.rec
  (fun h =>
    (fun hg =>
        let den := (1 * a ^ 2).den / Nat.gcd (1 * a ^ 2).den 1.den * 1.den;
        let num :=
          (1 * a ^ 2).num * ↑(1.den / Nat.gcd (1 * a ^ 2).den 1.den) +
            1.num * ↑((1 * a ^ 2).den / Nat.gcd (1 * a ^ 2).den 1.den);
        let g1 := Nat.gcd (Int.natAbs num) (Nat.gcd (1 * a ^ 2).den 1.den);
        let_fun den_nz := (_ : (1 * a ^ 2).den / Nat.gcd (1 * a ^ 2).den 1.den * 1.den ≠ 0);
        let_fun e :=
          (_ :
            let den := (1 * a ^ 2).den / Nat.gcd (1 * a ^ 2).den 1.den * 1.den;
            let num :=
              (1 * a ^ 2).num * ↑(1.den / Nat.gcd (1 * a ^ 2).den 1.den) +
                1.num * ↑((1 * a ^ 2).den / Nat.gcd (1 * a ^ 2).den 1.den);
            Nat.gcd (Int.natAbs num) (Nat.gcd (1 * a ^ 2).den 1.den) = Nat.gcd (Int.natAbs num) den);
        Rat.maybeNormalize num den g1 (_ : den / g1 ≠ 0) (_ : Nat.coprime (Int.natAbs (Int.div num ↑g1)) (den / g1)))
      h)
  (fun h =>
    (fun hg =>
        let_fun den_nz := (_ : (1 * a ^ 2).den * 1.den ≠ 0);
        let_fun reduced :=
          (_ :
            Nat.gcd (Int.natAbs ((1 * a ^ 2).num * ↑1.den + 1.num * ↑(1 * a ^ 2).den)) ((1 * a ^ 2).den * 1.den) = 1);
        Rat.mk' ((1 * a ^ 2).num * ↑1.den + 1.num * ↑(1 * a ^ 2).den) ((1 * a ^ 2).den * 1.den))
      h)
  (Nat.instDecidableCoprime (1 * a ^ 2).den 1.den)
-/

[David Renshaw]

Kevin Buzzard said:

That should be a meme

We may have found a new universal New Yorker cartoon caption.
lean4-2003.png

[Mario Carneiro]

oh interesting, I can't reproduce the issue in std

[Mario Carneiro]

a ^ 2 isn't valid using only std, and a * a doesn't exhibit the issue

[David Renshaw]

yep, I noticed that too

[Mario Carneiro]

and example {a : ℚ} : a^2 = a * a := rfl is also slow

[Mario Carneiro]

well I guess the definition is example {a : ℚ} : a^2 = a * (a * 1) := rfl and this works (quickly)

[Mario Carneiro]

here's a mathlib-free version:

import Std.Data.Rat.Basic

def Rat.npow : Nat → Rat → Rat
  | 0, _ => 1
  | n + 1, a => a * Rat.npow n a

example {a : Rat} : 1 * Rat.npow 2 a + 1 = 0 := rfl

[Heather Macbeth]

Thanks for looking into this. This:

David Renshaw said:

ah, with_reducible positivity goes a lot faster

solves all the problems in my use case (maybe that should be the default behaviour of positivity anyway?).

[Heather Macbeth]

However, the minimized example is pretty horrifying, hope we fix it!

[Mario Carneiro]

it's already fixed in std

[James Gallicchio]

(What was the fix?)

[Ruben Van de Velde]

https://github.com/leanprover/std4/commit/04b3c9831e0c141713a70e68af7e40973ec9a1ff

[Heather Macbeth]

I opened mathlib4#1767 to get that change into mathlib, hope I did it right.

[Ruben Van de Velde]

Looks like Mathlib/Data/Rat/Defs.lean no longer compiles

[Heather Macbeth]

Hopefully it's a matter of adding a few delta Rat.mul? I don't have time today but would be grateful if someone else wants to pick it up.

[Ruben Van de Velde]

Yeah, fixed. (Too bad there's no Rat.inv_zero lemma in Std)

[Mario Carneiro]

PR's welcome..

[Ruben Van de Velde]

I was avoiding that under the assumption that you'd be moving a lot of mathlib code anyway at some point, but could do

[James Gallicchio]

I'm guessing lots of Rat lemmas would fall in Std purview, but it takes a lot of work to figure out which can / can't be disentangled from mathlib

[Mario Carneiro]

all of them should be disentanglable, except for the ones that involve mathlib typeclasses in the statement

[Jon Eugster]

David Renshaw said:

It apparently spends a long time trying to decide whether 2 * b^2 + a^2 is definitionally equal to 8:

[Meta.isDefEq] [7.146166s] ❌ 2 * b ^ 2 + a ^ 2 =?= 8
  [Meta.isDefEq] [7.146093s] ❌ instHAdd.1 (2 * b ^ 2) (a ^ 2) =?= Rat.instOfNatRat.1
    [Meta.isDefEq] [7.146072s] ❌ Add.add (2 * b ^ 2) (a ^ 2) =?= ↑(Int.ofNat 8)
      [Meta.isDefEq] [7.146044s] ❌ Add.add (2 * b ^ 2) (a ^ 2) =?= IntCast.intCast (Int.ofNat 8)
        [Meta.isDefEq] [7.146019s] ❌ Rat.instAddRat.1 (2 * b ^ 2) (a ^ 2) =?= Rat.instIntCastRat.1 (Int.ofNat 8)
          [Meta.isDefEq] [7.146008s] ❌ Rat.add (2 * b ^ 2) (a ^ 2) =?= Rat.ofInt (Int.ofNat 8)
            [Meta.isDefEq] [7.145997s] ❌ Rat.add (2 * b ^ 2) (a ^ 2) =?= Rat.mk' (Int.ofNat 8) 1
              [Meta.isDefEq] [0.000000s] ✅ ℚ =?= ℚ
              [Meta.isDefEq] [1.434544s] ❌ (Rat.add (2 * b ^ 2) (a ^ 2)).num =?= Int.ofNat 8
                [Meta.isDefEq] [1.434532s] ❌ (Rat.add (2 * b ^ 2) (a ^ 2)).1 =?= Int.ofNat 8
                  [Meta.isDefEq.onFailure] [0.956389s] ❌ (Rat.add (2 * b ^ 2) (a ^ 2)).1 =?= Int.ofNat 8
...

Hi @David Renshaw how do I get the time info like you did when calling set_option trace.Meta.synthInstance true or
set_option trace.Meta.isDefEq true?

[Kevin Buzzard]

set_option profiler true

[Jon Eugster]

Thx!