simp_all out of control

Stream: mathlib4

[Kevin Buzzard]

I was experimenting with how far one could simp NNG away (starting at 1 just for fun). The last simp_all takes over 4 seconds on my machine with mathlib imported, and 0.2 seconds without it. I know it's not an appropriate goal for simp_all but when I look at the logs with mathlib imported they are really wild, talking about advanced stuff which is absolutely nothing to do with anything. Is this expected? Have I just committed too much simp abuse for some reason? Sample trace output then mathlib code:

...
          [Meta.Tactic.simp.unify] @HilbertBasis.coe_mk:1000, failed to unify
                fun i => ↑(LinearIsometryEquiv.symm (HilbertBasis.mk ?hv ?hsp).repr) (lp.single 2 i 1)
              with
                k * b = c * k → b = c
          [Meta.Tactic.simp.unify] @HilbertBasis.coe_mkOfOrthogonalEqBot:1000, failed to unify
                fun i => ↑(LinearIsometryEquiv.symm (HilbertBasis.mkOfOrthogonalEqBot ?hv ?hsp).repr) (lp.single 2 i 1)
              with
                k * b = c * k → b = c
          [Meta.Tactic.simp.unify] @OrthonormalBasis.coe_toHilbertBasis:1000, failed to unify
                fun i => ↑(LinearIsometryEquiv.symm (OrthonormalBasis.toHilbertBasis ?b).repr) (lp.single 2 i 1)
              with
                k * b = c * k → b = c
          [Meta.Tactic.simp.unify] @coe_fourierBasis:1000, failed to unify
                fun i => ↑(LinearIsometryEquiv.symm fourierBasis.repr) (lp.single 2 i 1)
              with
                k * b = c * k → b = c
          [Meta.Tactic.simp.unify] @Combinatorics.Line.map_apply:1000, failed to unify
                (fun x i => Option.getD (Combinatorics.Line.idxFun (Combinatorics.Line.map ?f ?l) i) x) (?f ?x)
              with
                k * b = c * k → b = c
          [Meta.Tactic.simp.unify] @Combinatorics.Line.vertical_apply:1000, failed to unify
                (fun x i => Option.getD (Combinatorics.Line.idxFun (Combinatorics.Line.vertical ?v ?l) i) x) ?x
              with
                k * b = c * k → b = c
...

import Mathlib -- if you dare

inductive MyNat
| one : MyNat
| S : MyNat → MyNat

notation (name := MyNatNotation) (priority := 1000000) "ℕ" => MyNat

namespace MyNat

instance ofNat : OfNat MyNat 1 where
  ofNat := one

-- test
theorem one_eq_1 : one = 1 := rfl

-- use it for `one`
@[simp] theorem one_def : one = 1 := rfl

def add : MyNat → MyNat → MyNat
  | a, one  => S a
  | a, S b => S (add a b)

instance instAdd : Add MyNat where
  add := MyNat.add

@[simp]
theorem add_one (a : MyNat) : a + 1 = S a := by rfl

@[simp]
theorem add_S (a b : MyNat) : a + (S b) = S (a + b) := by rfl

theorem add_assoc (a b c : MyNat) : (a + b) + c = a + (b + c) := by
  induction c with
  | one => simp
  | S _ h => simp [h]

@[simp]
theorem one_add (a : ℕ) : 1 + a = S a := by
  induction a with
  | one => simp
  | S _ h => simp [h]

@[simp]
theorem S_add (a b : ℕ) : S a + b = S (a + b) := by
  induction b with
  | one => simp
  | S _ h => simp [h]

@[simp]
theorem add_comm (a b : ℕ) : a + b = b + a := by
  induction b with
  | one => simp
  | S _ h => simp [h]

@[simp]
theorem add_left_comm (a b c : ℕ) : a + b + c = a + c + b := by
  rw [add_assoc, add_comm b, add_assoc]

namespace MyNat

def mul : MyNat → MyNat → MyNat
  | a, 1   => a
  | a, b + 1 => (mul a b) + a

instance : Mul MyNat where
  mul := MyNat.mul

@[simp]
theorem mul_one (a : MyNat) : a * 1 = a := by rfl

@[simp] -- I only want it simp for now
theorem mul_S (a b : MyNat) : a * (S b) = a * b + a := by rfl

@[simp]
theorem one_mul (a : ℕ) : 1 * a = a := by
  induction a with
  | one => simp [mul_one]
  | S _ h => simp [mul_S, h]

@[simp]
theorem S_mul (a b : ℕ) : S a * b = a * b + b := by
  induction b with
  | one =>
    simp
  | S k h =>
    simp [h, mul_S, ← add_assoc]

@[simp]
theorem mul_comm (a b : ℕ) : a * b = b * a := by
  induction b with
  | one =>
    simp
  | S k hk =>
    simp [mul_S, hk]

set_option trace.profiler true in
--set_option trace.Meta.Tactic.simp true in
example (c k : ℕ) (hk: ∀ (b : ℕ), k * b = k * c → b = c) (b: ℕ) (h: S k * b = S k * c) :
  b = c := by
  simp_all
  sorry

end MyNat

[Mauricio Collares]

I think there are many lemmas/typeclass searches contributing here:

• Mathlib/Algebra/GroupWithZero/Basic.lean has six simp lemmas in section CancelMonoidWithZero (assuming [CancelMonoidWithZero M₀]), and they all slow things down a bit. It feels as if some cache is being reset often.
• Of the other half, the four simp lemmas in Mathlib/Algebra/Group/Basic.lean which take LeftCancelMonoid or RightCancelMonoid instances seem to be responsible for a lot of the search time, in the same manner as described above (each of the four lemmas cause a fourth of the total slowdown attributable to this file).

[Kevin Buzzard]

Oh nice detective work!

[Mauricio Collares]

Updated the first bullet point (I had previously claimed a NeZero instance was causing slowdowns, which wasn't the case).

[Kevin Buzzard]

Ironically, zero is the one thing I don't have in this file :-)

[Kevin Buzzard]

So this is probably a mathlib issue?

[Mauricio Collares]

I'm way out of my depth here, but I'd say this is a Lean issue. Mathlib adds many simp lemmas whose conclusions would be useful in your example, but Lean spends an unreasonable amount of time figuring out that the required instances aren't available. the Meta.synthInstance trace reports a lot of cache hits but there must be some expensive uncached steps (probably unrelated to typeclass inference). Let me try to record a perf trace.

[Mauricio Collares]

I inadvertently profiled with a debug build (which is slower for everything) and got a big surprise: https://gist.github.com/collares/a5cad26f73072c09694250ba6a21d5a0 -- you can simulate this with set_option trace.profiler true and set_option trace.profiler.threshold 1.

[Mauricio Collares]

Look at how many essentially-equal isDefEq checks! I know there probably is no caching due to the metavariables, but it's still a very surprising number of calls.

[Mauricio Collares]

In total, there are 2091 very similar isDefEq checks. ?a * ?b = ?a =?= k * (k * b) = c * k and ?a * ?b = ?b =?= k * (k * b) = c * k are the leaders with 104 times each.

[Mauricio Collares]

Probably best to use set_option pp.all true to see stuff like

        [Meta.isDefEq] [0.001818s] ❌ @Eq.{?u.10505 + 1} ?M₀
              (@HMul.hMul.{?u.10505, ?u.10505, ?u.10505} ?M₀ ?M₀ ?M₀
                (@instHMul.{?u.10505} ?M₀
                  (@MulZeroClass.toMul.{?u.10505} ?M₀
                    (@MulZeroOneClass.toMulZeroClass.{?u.10505} ?M₀
                      (@MonoidWithZero.toMulZeroOneClass.{?u.10505} ?M₀
                        (@CancelMonoidWithZero.toMonoidWithZero.{?u.10505} ?M₀ ?inst✝)))))
                ?a ?b)
              ?a =?= @Eq.{1} MyNat
              (@HMul.hMul.{0, 0, 0} MyNat MyNat MyNat (@instHMul.{0} MyNat MyNat.MyNat.instMulMyNat) k b)
              (@HMul.hMul.{0, 0, 0} MyNat MyNat MyNat (@instHMul.{0} MyNat MyNat.MyNat.instMulMyNat) c k)