grind failure/performance issue: timing out on slow instance

Stream: general

[Alex Meiburg]

I have a hard time getting mwe, but I noticed an issue like this:

example {d : Type*} {S T : Submodule ℂ (EuclideanSpace ℂ d)} (h : S ≤ T) (i : ℝ) :
    i ∈ Set.Ioi 1 ∩ {a | ¬a = 1} ↔ i ∈ Set.Ioi 1 := by
  #count_heartbeats --33726166
  grind

example {d : Type*} {S T : Submodule ℂ (EuclideanSpace ℂ d)} (h : S ≤ T) (i : ℝ) :
    i ∈ Set.Ioi 1 ∩ {a | ¬a = 1} ↔ i ∈ Set.Ioi 1 := by
  clear h
  #count_heartbeats --777105
  grind

This is a silly little side-goal about i involving set membership over reals that grind should be able to dispatch quickly. The S and T are irrelevant. By removing the goal h, grind runs about 40x faster. Actually, on the local (not-minimzed) version, it's the difference between succeeding or not: without the clear, grind fails with

failed to synthesize
  LE (Lean.Grind.IntModule.OfNatModule.Q (Submodule ℂ (WithLp 2 (d → ℂ))))
(deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached

In the end, I can clear hypotheses, sure, but it feels a bit annoying to do by clear foo; grind when I want to just have by grind in a sidegoal. Is there a flag I can pass to grind to turn this off? I tried grind -ring but it didn't help. I'm also not sure if there's anything I can really do, because linear inequality solving is part of the actual final goal.

An interesting heuristic to explore would be to have grind explore what it can prove only with the "relevant" variables first (relevant in the same sense that extract_goal uses - those connected by some variables to the conclusion), and then when that gets stuck, it starts processing disconnected hypotheses.

[Jovan Gerbscheid]

I think that Mathlib's type classes are to blame here. The following takes 0.8 seconds to fail, which is part of your slow grind call:

module
import Mathlib

variable {d : Type*}
set_option trace.profiler true
set_option trace.Meta.synthInstance true

#synth Lean.Grind.OrderedAdd (Submodule ℂ (WithLp 2 (d → ℂ)))

[Jovan Gerbscheid]

I've made #35563 to address this slow failing synthesis.

[Jovan Gerbscheid]

Now that this PR has been merged, the grind calls you posted have both become a bit faster, and presumably it won't time out anymore in your non-minimized version.

However, the original problem remains. One issue I've noticed is that it seems that whenever grind encounters the type ENNReal, it wastes about 0.8s synthesizing type classes:

module import Mathlib

example (x y : ENNReal) (h : x ≤ 2 * y) : x ≤ 2 * y := by
  #count_heartbeats -- 8344000
  grind

And although it doesn't look like it, you example secretly contains the type ENNReal, namely via WithLp.instAddCommGroup.

[Kim Morrison]

@Jovan Gerbscheid, might you be able to add another test to MathlibTest/slow_instances.lean, to validate/guard against regressions from your #35563?

[Jovan Gerbscheid]

Sure, I've opened #35667