Zulip Chat Archive

Stream: mathlib4

Topic: slow `positivity`


Heather Macbeth (Jan 22 2023 at 05:39):

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 (Jan 22 2023 at 12:50):

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 (Jan 22 2023 at 12:51):

ah, with_reducible positivity goes a lot faster

David Renshaw (Jan 22 2023 at 12:54):

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

David Renshaw (Jan 22 2023 at 13:33):

This takes a long time to fail:

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

David Renshaw (Jan 22 2023 at 13:41):

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 (Jan 22 2023 at 14:24):

Would lean4#2003 be useful here?

Kevin Buzzard (Jan 22 2023 at 14:25):

That should be a meme

James Gallicchio (Jan 22 2023 at 15:05):

image.png as requested

David Renshaw (Jan 22 2023 at 15:53):

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 (Jan 22 2023 at 15:55):

what does #whnf do on that example?

David Renshaw (Jan 22 2023 at 15:56):

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

Mario Carneiro (Jan 22 2023 at 15:56):

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

Mario Carneiro (Jan 22 2023 at 15:57):

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

I guess

David Renshaw (Jan 22 2023 at 15:57):

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 (Jan 22 2023 at 16:27):

Kevin Buzzard said:

That should be a meme

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

Mario Carneiro (Jan 22 2023 at 16:34):

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

Mario Carneiro (Jan 22 2023 at 16:34):

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

David Renshaw (Jan 22 2023 at 16:34):

yep, I noticed that too

Mario Carneiro (Jan 22 2023 at 16:35):

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

Mario Carneiro (Jan 22 2023 at 16:35):

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

Mario Carneiro (Jan 22 2023 at 16:41):

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 (Jan 22 2023 at 17:09):

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 (Jan 22 2023 at 17:09):

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

Mario Carneiro (Jan 22 2023 at 17:27):

it's already fixed in std

James Gallicchio (Jan 22 2023 at 17:31):

(What was the fix?)

Ruben Van de Velde (Jan 22 2023 at 17:35):

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

Heather Macbeth (Jan 22 2023 at 18:29):

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

Ruben Van de Velde (Jan 22 2023 at 19:04):

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

Heather Macbeth (Jan 22 2023 at 19:08):

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 (Jan 22 2023 at 19:54):

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

Mario Carneiro (Jan 22 2023 at 20:04):

PR's welcome..

Ruben Van de Velde (Jan 22 2023 at 21:50):

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 (Jan 22 2023 at 23:38):

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 (Jan 23 2023 at 04:46):

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

Jon Eugster (Feb 04 2023 at 07:29):

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 (Feb 04 2023 at 07:32):

set_option profiler true

Jon Eugster (Feb 04 2023 at 07:33):

Thx!


Last updated: Dec 20 2023 at 11:08 UTC