TC slowness

Stream: mathlib4

[Yuyang Zhao]

I've found two particularly slow examples recently. Neither of these instances should be inferred, but they take too many heartbeats to fail.

import Mathlib

count_heartbeats in -- Used 19118 heartbeats
example {n : ℕ} : CovariantClass (Fin (n + 1)) (Fin (n + 1)) (· + ·) (· < ·) := by
  try infer_instance
  sorry

count_heartbeats in -- Used 20115 heartbeats
example : IsEmpty ((ι → ℝ) → ℝ) := by
  try infer_instance
  sorry

For the first example, I tried to remove some redundant instances in #9252. At the beginning the build failed. I realized that Lean tries to search for an instance that contains a metavariable. I found a similar example at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Instance.20search.20without.20type, but instead of getting a :boom:, I got a :cross_mark:. I think it's because the TC search wasn't failing fast enough, so I added some meaningless high-priority instances, and then the build succeeded. Of course that didn't really solve the problem, and Lean still made a lot of attempts that seem unnecessary to me.

I don't think I have enough TC knowledge to continue to understand these two examples, so I'd like to show them to someone who knows more about TC.

[Yaël Dillies]

I think we should turn all uses of CovariantClass/ContravariantClass into custom structures. With the current situation, all new instances slow down all existing uses.

[Eric Wieser]

As in, a new typeclass for each operator and relation?

[Yaël Dillies]

Yes, exactly. There is only two operators and two relations we care about, so that makes 4 new typeclasses.

[Newell Jensen]

IIUC, this actually might help me out with the typeclass I need to define for OrderedSemifield(see here for discussion) because right now if I try to extend PosMulMono etc. I get errors that they are not structures.

[Eric Wieser]

The solution there is to not use extends and just create a OrderedSemifield.toPosMulMono instance after the clsas

[Yuyang Zhao]

We have

import Mathlib

count_heartbeats in -- Used 21265 heartbeats
example {n : ℕ} : CovariantClass (Fin (n + 1)) (Fin (n + 1)) (· + ·) (· < ·) := by
  try infer_instance
  sorry

count_heartbeats in -- Used 20349 heartbeats
example : IsEmpty ((ι → ℝ) → ℝ) := by
  try infer_instance
  sorry

on branch#f09d5297.
And now

import Mathlib

count_heartbeats in -- Used 15897 heartbeats
example {n : ℕ} : CovariantClass (Fin (n + 1)) (Fin (n + 1)) (· + ·) (· < ·) := by
  try infer_instance
  sorry

count_heartbeats in -- Used 20014 heartbeats
example : IsEmpty ((ι → ℝ) → ℝ) := by
  try infer_instance
  sorry

on branch#45bd0a21

lean4#4003 didn't completely resolve the first example. I checked the TC search and found that the instance parameters are not syntactically the same in duplicate attempts. Can this difference instance parameters be ignored during TC searches? If it's possible, TC searches might be several times faster than before (at least in my first example). Here is a #mwe

class A (t : Nat)
class B (n : Nat) [A 0] [A 1] [A 2] [A 3] [A 4] [A 5] [A 6] [A 7]

instance a1 : A t where

instance b [A 0] [A 1] [A 2] [A 3] [A 4] [A 5] [A 6] [A 7] [B n] : B n.succ where
instance b0 [A 1] [A 2] [A 3] [A 4] [A 5] [A 6] [A 7] [B n] [A 0] : B n.succ where
instance b1 [A 0] [A 2] [A 3] [A 4] [A 5] [A 6] [A 7] [B n] [A 1] : B n.succ where
instance b2 [A 0] [A 1] [A 3] [A 4] [A 5] [A 6] [A 7] [B n] [A 2] : B n.succ where
instance b3 [A 0] [A 1] [A 2] [A 4] [A 5] [A 6] [A 7] [B n] [A 3] : B n.succ where
instance b4 [A 0] [A 1] [A 2] [A 3] [A 5] [A 6] [A 7] [B n] [A 4] : B n.succ where
instance b5 [A 0] [A 1] [A 2] [A 3] [A 4] [A 6] [A 7] [B n] [A 5] : B n.succ where
instance b6 [A 0] [A 1] [A 2] [A 3] [A 4] [A 5] [A 7] [B n] [A 6] : B n.succ where
instance b7 [A 0] [A 1] [A 2] [A 3] [A 4] [A 5] [A 6] [B n] [A 7] : B n.succ where

instance a2 : A t where

#synth B 7 -- (deterministic) timeout at `typeclass`

(My naive thought is that (most of the time?) the definition of the instance parameter doesn't matter during TC searches, so maybe it's ok to do this (in most cases)......)

[Yuyang Zhao]

After modifying the TC search the first example takes only less than 2000 heartbeats and shake found some unused imports. But the whole Mathlib is not significantly faster...

[Utensil Song]

At least the good news is Mathlib builds successfully after the modification. Where is the modified TC search code?

[Utensil Song]

#12810 looks significant faster?

[Yuyang Zhao]

That's because bump/nightly-2024-05-09 is faster than master.

[Yuyang Zhao]

I haven't found the reason why Mathlib.LinearAlgebra.Semisimple is faster. @Meow implemented something like lean4#4003 and this advantage disappeared when I removed it.

[Yuyang Zhao]

Removing some instances also speeds up the first example, but it needs a hack to work... See #9252

[Yuyang Zhao]

Yuyang Zhao said:

and shake found some unused imports.

#12830

[Yuyang Zhao]

Currently the first example is 10262 heartbeats. In #13124, we have

import Mathlib

count_heartbeats in -- Used 3826 heartbeats
example {n : ℕ} : AddLeftStrictMono (Fin (n + 1)) := by
  try infer_instance
  sorry

It's not as good as #12810, but it's still faster and does not need to modify Lean4.

[Yuyang Zhao]

There are still some unnecessary duplicate checks.

[Meta.synthInstance] ❌ AddLeftStrictMono (Fin (n + 1)) ▼
  [] new goal AddLeftStrictMono (Fin (n + 1)) ▶
  [] ✅ apply @IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono to AddLeftStrictMono (Fin (n + 1)) ▶
  [] ✅ apply @IsCancelAdd.toIsLeftCancelAdd to IsLeftCancelAdd (Fin (n + 1)) ▶
  [] ✅ apply Fin.instIsCancelAdd to IsCancelAdd (Fin (n + 1)) ▶
  [resume] propagating IsCancelAdd (Fin (n + 1)) to subgoal IsCancelAdd (Fin (n + 1)) of IsLeftCancelAdd (Fin (n + 1)) ▶
  [resume] propagating IsLeftCancelAdd (Fin (n + 1)) to subgoal IsLeftCancelAdd (Fin (n + 1)) of AddLeftStrictMono (Fin (n + 1)) ▶
  [] ❌ apply OrderedAddCommGroup.to_covariantClass_left_le to AddLeftMono (Fin (n + 1)) ▶
  [] ❌ apply @OrderedAddCommMonoid.toCovariantClassLeft to AddLeftMono (Fin (n + 1)) ▶
  [] ✅ apply @addLeftMono_of_addLeftReflectLT to AddLeftMono (Fin (n + 1)) ▶
  [] ❌ apply @OrderedCancelAddCommMonoid.toContravariantClassLeft to AddLeftReflectLT (Fin (n + 1)) ▶
  [] ✅ apply @addLeftReflectLT_of_addLeftMono to AddLeftReflectLT (Fin (n + 1)) ▶
  [] ❌ apply OrderedAddCommGroup.to_covariantClass_left_le to AddLeftMono (Fin (n + 1)) ▶
  [] ❌ apply @OrderedAddCommMonoid.toCovariantClassLeft to AddLeftMono (Fin (n + 1)) ▶
  [] ✅ apply @addLeftMono_of_addLeftReflectLT to AddLeftMono (Fin (n + 1)) ▶
  [] ✅ apply @AddGroup.addLeftReflectLT_of_addLeftStrictMono to AddLeftReflectLT (Fin (n + 1)) ▶
  [] ✅ apply @IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono to AddLeftStrictMono (Fin (n + 1)) ▶
  [] ✅ apply @IsCancelAdd.toIsLeftCancelAdd to IsLeftCancelAdd (Fin (n + 1)) ▶
  [] ✅ apply Fin.instIsCancelAdd to IsCancelAdd (Fin (n + 1)) ▶
  [resume] propagating IsCancelAdd (Fin (n + 1)) to subgoal IsCancelAdd (Fin (n + 1)) of IsLeftCancelAdd (Fin (n + 1)) ▶
  [resume] propagating IsLeftCancelAdd (Fin (n + 1)) to subgoal IsLeftCancelAdd (Fin (n + 1)) of AddLeftStrictMono (Fin (n + 1)) ▶
  [] ❌ apply OrderedAddCommGroup.to_covariantClass_left_le to AddLeftMono (Fin (n + 1)) ▶
  [] ❌ apply @OrderedAddCommMonoid.toCovariantClassLeft to AddLeftMono (Fin (n + 1)) ▶
  [] ✅ apply @addLeftMono_of_addLeftReflectLT to AddLeftMono (Fin (n + 1)) ▶
  [] ❌ apply @OrderedCancelAddCommMonoid.toContravariantClassLeft to AddLeftReflectLT (Fin (n + 1)) ▶
  [] ✅ apply @addLeftReflectLT_of_addLeftMono to AddLeftReflectLT (Fin (n + 1)) ▶
  [] ❌ apply OrderedAddCommGroup.to_covariantClass_left_le to AddLeftMono (Fin (n + 1)) ▶
  [] ❌ apply @OrderedAddCommMonoid.toCovariantClassLeft to AddLeftMono (Fin (n + 1)) ▶
  [] ✅ apply @addLeftMono_of_addLeftReflectLT to AddLeftMono (Fin (n + 1)) ▶
  [] ✅ apply @AddGroup.addLeftReflectLT_of_addLeftStrictMono to AddLeftReflectLT (Fin (n + 1)) ▶

[Yuyang Zhao]

Yaël Dillies said:

I think we should turn all uses of CovariantClass/ContravariantClass into custom structures. With the current situation, all new instances slow down all existing uses.

According to the benchmark results in #13124, should we try to remove CovariantClass/ContravariantClass? (If so, I'll reopen my PRs.)

[Yaël Dillies]

I think so, yeah

[Jireh Loreaux]

What exactly are all the existing uses of CovariantClass / ContravariantClass? Are there others besides ≤ / < and + / * ?

[Jireh Loreaux]

Also, perhaps we can actually leave those in, but make things on top of them be semireducible instead of reducible. And then only reference the semireducible definitions in practice. It would just be a shame to lose all the generality.

[Damiano Testa]

Jireh Loreaux said:

What exactly are all the existing uses of CovariantClass / ContravariantClass? Are there others besides ≤ / < and + / * ?

If I remember correctly, there are a couple of uses of div, \smul, and not much else. Junyan wanted to add some more, but the PR was never merged, I think.

[Damiano Testa]

Maybe, after advocating against introducing new names for the add, mul, le, lt and reflect versions, I should agree that it is better, since looking for fully general functions is unmaintainable...

[Jireh Loreaux]

I agree, that fully general functions is likely unmaintainable, but I was thinking we could still have the general versions in the background, just unused as a class so as not to duplicate proofs. But maybe it's the case that there are so few general theorems that even that use case is not worth the effort.

[Yuyang Zhao]

docs#Covariant and docs#Contravariant still exist.

[Jireh Loreaux]

okay, fair enough.

[Yuyang Zhao]

Subsequent PRs #13154 and #13124 are still not merged.

[Violeta Hernández]

Left a lot of style suggestions on #13154, mostly relating to rewrapping lines. The vast majority of these are in my opinion quick and uncontroversial improvements, but if you don't have the time to deal with bikeshedding feel free to ignore everything.

[Yuyang Zhao]

#13124 needs some extra beta-reduce. I guess this is because (· < ·) (· * ·) no longer appear directly in the type of typeclasses and won't be automatically eta-reduced. Should we write them directly as LT.lt etc., or no longer state *.elim using docs#Covariant and docs#Contravariant?

[Yaël Dillies]

I think we should no longer use Covariant and Contravariant