Regression in simp

Stream: mathlib4

[Bhavik Mehta]

import Mathlib

set_option trace.profiler true

example : (fun i : Nat => 3) ≠ fun i : Nat => 4 := by simp [Function.funext_iff]

This takes a concerning amount of time for me - around 2 seconds. The Lean 3 version takes around 10ms. What's making simp so slow on something this simple? The profiler trace seems to print out a bunch of decidable instances.

(Also, in Lean 3 it works with just simp, but not in Lean 4! The difference seems to be that docs4#Function.const_inj isn't firing for some reason...?)

[Eric Wieser]

(config := {decide := false}) makes it twice as fast

[Eric Wieser]

Though the web editor runs 3x faster than your quoted time either way

[Scott Morrison]

I have tried a few times to change the default to {decide := false}, and in principle there is agreement to merge such a change. If anyone would like to attempt this again, feel free to ping me on a PR. :-)

[Bhavik Mehta]

Eric Wieser said:

Though the web editor runs 3x faster than your quoted time either way

I think that's my laptop being slow! But I did the mathlib3 and mathlib4 timing on the same machine, so hopefully the ratio is consistent

[Bhavik Mehta]

Eric Wieser said:

(config := {decide := false}) makes it twice as fast

That's still much slower than the Lean 3 version though, so I'm not sure this is much of a fix...

[Mauricio Collares]

Eric Wieser said:

(config := {decide := false}) makes it twice as fast

Even disabling decide, you can see in the trace that Lean spends a bunch of time trying to synthesize various Singleton instances. This is because eq_iff_true_of_subsingleton was inadvertently added to the simp set in Mathlib.Logic.Unique, see #7678.

[Mauricio Collares]

Unrelated to this, I wonder why synthesizing CharZero ℕ takes more than 100ms. Enabling set_option trace.Meta.synthInstance true results in a hilarious trace, though.

[Mauricio Collares]

The CharZero problem is that there are two "lower priority instances", instance (priority := 100) charZero_of_expChar_one' [hq : ExpChar R 1] : CharZero R (in Mathlib.Algebra.CharP.ExpChar) and instance (priority := 100) StrictOrderedSemiring.to_charZero [StrictOrderedSemiring α] : CharZero α (in Mathlib.Algebra.Order.Ring.CharZero). The former gets tried first and is comparatively very slow (and fails), while the latter succeeds (actually NumberField.to_charZero is also tried, but it is fast to fail).

[Mauricio Collares]

Would bumping the priority of StrictOrderedSemiring.to_charZero to 200 be OK? #7777

[Alex J. Best]

That's weird, I can't see any instances of ExpChar in mathlib, so while silly I don't understand how that can be slow

[Mauricio Collares]

You're right, but this instance is in a section containing variable [Nontrivial R] and variable [Semiring R], and Lean does something very weird while trying to synthesize Nontrivial Nat

[Mauricio Collares]

This is the synthInstance trace for finding the CharZero Nat instance currently: https://gist.github.com/collares/8590a08c79eed16879a823233b03ba70

[Mauricio Collares]

I wonder if it tries every possible way to get a Nontrivial instance ([Infinite.instNontrivial, @GroupWithZero.toNontrivial, @CommGroupWithZero.toNontrivial, @LinearOrderedAddCommGroupWithTop.toNontrivial, @IsDomain.toNontrivial, @StrictOrderedSemiring.toNontrivial, @StrictOrderedRing.toNontrivial, @LinearOrderedCommGroupWithZero.toNontrivial, @instNontrivial, @DivisionSemiring.toNontrivial, @DivisionRing.toNontrivial, @Semifield.toNontrivial, @Field.toNontrivial, @IsSimpleOrder.toNontrivial, Nat.nontrivial]), and for each one figures out that ExpChar instances don't exist. It tries Nat.nontrivial first, which is fast, but then it keeps going once it doesn't find the ExpChar instance.

[Alex J. Best]

I see! perhaps we need a new rule of thumb "put the more likely to fail instance parameters first when defining instances"

[Alex J. Best]

Or a smarter search algorithm of course

[Mauricio Collares]

Do you think

-instance (priority := 100) charZero_of_expChar_one' [hq : ExpChar R 1] : CharZero R := by
+instance (priority := 100) charZero_of_expChar_one' [hq : ExpChar R 1] [Nontrivial R] : CharZero R := by

is a better fix than increasing StrictOrderedSemiring.to_charZero's priority?

[Mauricio Collares]

Alex J. Best said:

I see! perhaps we need a new rule of thumb "put the more likely to fail instance parameters first when defining instances"

The way the variable command works really encourages the other way around.

[Alex J. Best]

I'd be happy to just remove that instance (ie. make it a theorem with a note) as the bandaid, if there are no instances of ExpChar around then clearly it will not be useful with the current state of the library, so mayaswell be removed

[Alex J. Best]

I think

class Foo (a : Type) : Type
class Bar (a : Type) : Type
class Baz (a : Type) : Type

def a : Type := sorry

instance a1 : Foo a := sorry
instance a2 : Foo a := sorry

instance (R : Type) [Foo R] [Bar R] : Baz R := sorry

set_option trace.Meta.synthInstance true
#synth Baz a

would be an ok RFC for the lean 4 repo (assuming it's not there already)

[Mauricio Collares]

Must an RFC contain a proposed solution? I don't think I'm qualified to write one (better than "better heuristics plzzz") if so, and I'd be happy if you or someone else filed the issue. I can certainly file a bug report, though.

[Mauricio Collares]

I guess just aborting the whole search if some class ia found to have no instances would be the bare minimum, but this wouldn't cover the case where there are several Foo instances none of which apply.

[Alex J. Best]

I don't think you need to propose a solution, just be clear about what the issue is and why a better heuristic should be possible. Maybe making a second synthetic example with a1 - a1000 to show that is can be slow or something

[Mauricio Collares]

Scott Morrison said:

I have tried a few times to change the default to {decide := false}, and in principle there is agreement to merge such a change. If anyone would like to attempt this again, feel free to ping me on a PR. :-)

lean4#2722 is green, but I think the Std4 fallout should be fixed by adding more simp lemmas instead of adding decide := true to all relevant simp calls there.

[Mauricio Collares]

I pushed a bunch of fixes to branch#lean-pr-testing-2722, but there's still a lot of work to do.

[Scott Morrison]

@Mauricio Collares, thanks for tackling this!

Could you open a draft PR based on branch#lean-pr-testing-2722 to make it easier to review changes, and see CI output?

[Scott Morrison]

(and so once it compiles we can benchmark!)

[Mauricio Collares]

Done: #7834

[Mauricio Collares]

All done, except that test/ComputeDegree.lean fails because ComputeDegree is less powerful now because its simp calls (either direct or indirect via norm_num) don't do decidability and can't simplify stuff like 6 ≤ WithBot.unbot' 0 48. I don't know what an appropriate solution for this is, so I will leave it to somebody else.

[Alex J. Best]

Can't you just make compute_degree use simp (decide := true) in the interim?

[Mauricio Collares]

I can alter it to make the direct calls use it, but norm_num does not have configuration options (test/norm_num_ext.lean also fails for the same reason). I'm sure there's a way to change norm_num as well (although I personally would not be able to find it easily), but I don't know if the change is wanted and because of that I'd rather not do the change myself.

[Damiano Testa]

Speaking for compute_degree, I think that it is the version with ! that is affected by this. The !-version essentially tries norm_num <;> assumption on all the goals that compute_degree would leave. I would expect compute_degree! to work on the test cases, but really because I would expect norm_num to be the actually finishing tactic...

[Mauricio Collares]

I guess the problem here is that rfl or decide solve the goal below, but simp by itself does not:

import Mathlib

example : WithBot.unbot' 0 (40 : WithBot ℕ) = 40 := by
  simp -- fails when decide := false

[Damiano Testa]

I would say that whether or not this is within simp's remit, I would definitely expect norm_num to solve this!

[Damiano Testa]

Though maybe the solution is to add a simp-lemma?

[Mauricio Collares]

Agreed! It doesn't at the moment (it does on master, but that's because it calls simp and simp calls decide).

[Damiano Testa]

Honestly, I find simp; rfl a bit of an anti-pattern and would like to have a way flag simp to try rfl...

[Mauricio Collares]

norm_cast solves the goal, though

[Damiano Testa]

Good! norm_cast also should prove it!

[Damiano Testa]

Anyway, from the point of view of compute_degree, I would expect the current tests to work. I do not mind if this entails reworking the discharger for compute_degree, though.

[Damiano Testa]

Likely, this means simply adapting this line

https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/ComputeDegree.lean#L456

to solve the goals in the test file.

[Mauricio Collares]

@Kyle Miller Do you think it would be OK to comment out https://github.com/leanprover-community/mathlib4/blob/49b7459e781c2cea928235d669585fb02ff89efe/test/norm_num_ext.lean#L338-L349 in #7834? I think the List/Multiset tests aren't testing norm_num extensions, but are calling decide via simp (replacing by norm_num only with by decide makes them pass).

[Mauricio Collares]

@Scott Morrison The PR builds now. I had to comment a few norm_num_ext tests when I think weren't testing norm_num extensions (see above), let's see if Kyle thinks that's OK.

[Mauricio Collares]

(The ComputeDegree test now passes, I combined Alex's and Damiano's suggestions to fix it. Thanks!)

[Scott Morrison]

@Mauricio Collares, you will need to rebase lean4#2722 onto master many spurious diffs are showing up on the PR. I can start reviewing it after you've done that.

[Kyle Miller]

@Mauricio Collares I just ported those tests from mathlib3. Commenting them out makes sense -- if you do, then please add a comment that it's because by decide suffices. A reason not to delete them is that there might be a norm_num extension for these at some later point.

[Mauricio Collares]

Status update: #7777 was just merged (thanks Rob Lewis and Alex Best!), and #7678 and lean4#2722 are pending.

[Scott Morrison]

I've just merged lean4#2722 earlier today. Thank you for this, we're excited to see this finally happen!

[Mauricio Collares]

Thank you so much!

[Mauricio Collares]

I'll bump #7834 as soon as the new lean nightly appears (seems like there was a problem there due to a recent force push), and then after std4#312 is merged into the bump/v4.4.0 branch.

[Scott Morrison]

Sorry, the latest nightly release has been delayed due to me .... breaking various aspects of Lean CI tonight. :-) Working on it!

[Scott Morrison]

(In fact, it may just be delayed until tomorrow's run.)

[Mauricio Collares]

Thank you very much for this work as well! Juggling all the different PR branches sounds exhausting

[Mauricio Collares]

Rebased #7834

[Scott Morrison]

I'll merge #7834 (just into bump/v4.4.0 for now, it needs to wait a while for master) once std#312 has been merged.

[Mauricio Collares]

Great, thanks! What should I do wrt reviews after #7834 is merged? I would open a separate PR targeting master, but I think CI might not be too happy with that.

[Scott Morrison]

Sorry, reviews of what?

[Scott Morrison]

#7834 has been approved and merged now, so I don't think there's any further scope for reviews?

[Mauricio Collares]

Ah, even better then! I thought it would need to go through a separate review process to be approved for mathlib master.

[Kevin Buzzard]

(Looks like it hasn't actually been merged btw)

[Scott Morrison]

Ah, thanks. Solution: merge master into bump/v4.4.0 (always allowed!) and merge bump/v4.4.0 into #7834. Phew.

[Mauricio Collares]

Merging master caused a new build failure, fixed now.

[Mauricio Collares]

One pending thing here is to decide is norm_num should call simp with decide := true by default, and perhaps add an option to configure this behaviour (regardless of the default).

[Mauricio Collares]

On mathlib master:

[Elab.command] [0.046074s] example : (fun i : Nat => 3) ≠ fun i : Nat => 4 := by simp [Function.funext_iff]
  [Elab.step] [0.042768s] simp [Function.funext_iff]
    [Elab.step] [0.042752s] simp [Function.funext_iff]
      [Elab.step] [0.042731s] simp [Function.funext_iff]
        [Meta.synthInstance] [0.011645s] ✅ CharZero ℕ