rfl repeating itself

Stream: lean4

[Kevin Buzzard]

I'm trying to debug a slow erw and I noticed the following. I have some definition foobar and this is slow (4 seconds):

set_option trace.profiler true in
example : foobar n A (n + 1 + 1) = foobar n A (n + 2) := rfl

But the trace looks like this:

[Elab.command] [4.021643s] example : foobar n A (n + 1 + 1) = foobar n A (n + 2) :=
      rfl ▼
  [step] [0.904533s] expected type: Sort ?u.127734, term
      foobar n A (n + 1 + 1) = foobar n A (n + 2) ▶
  [step] [1.555596s] expected type: GroupCohomology.foobar n A (n + 1 + 1) = GroupCohomology.foobar n A (n + 2), term
      rfl ▼
    [Meta.isDefEq] [1.555313s] ✅ GroupCohomology.foobar n A (n + 1 + 1) = GroupCohomology.foobar n A (n + 2) =?= ?m.131706 = ?m.131706 ▼
      [] [1.555200s] ✅ GroupCohomology.foobar n A (n + 2) =?= GroupCohomology.foobar n A (n + 1 + 1) ▶
  [Meta.isDefEq] [1.542510s] ✅ GroupCohomology.foobar n A (n + 1 + 1) =
        GroupCohomology.foobar n A
          (n + 1 + 1) =?= GroupCohomology.foobar n A (n + 1 + 1) = GroupCohomology.foobar n A (n + 2) ▼
    [] [1.542491s] ✅ GroupCohomology.foobar n A (n + 1 + 1) =?= GroupCohomology.foobar n A (n + 2) ▶

The [Elab.command] becomes two [step]s and a [Meta.isDefEq]. The final [Meta.isDefEq] expands into a [] which is this (and takes 1.5 seconds):

    [] [1.542491s] ✅ GroupCohomology.foobar n A (n + 1 + 1) =?= GroupCohomology.foobar n A (n + 2)

But the second [step] expands intp a [Meta.isDefEq] and then a [] which is this:

[] [1.555200s] ✅ GroupCohomology.foobar n A (n + 2) =?= GroupCohomology.foobar n A (n + 1 + 1)

and that's taking another 1.5 seconds to answer the same equation up to isDefEq.symm. In particular the system is doing twice as much work as needed here. Is this expected?

[Sebastian Ullrich]

Note that by rfl avoids this. It might still be worth filing an issue for this but generally speaking it is expected that tactics have more fine-grained control over what's happening than general elaboration has.

[Sebastian Ullrich]

Indeed using even more control as in by with_reducible rfl makes the proof time insignificant, only the type elaboration is left in the trace. By allowing fewer definitions to be unfolded by Lean, we force it to consider earlier that the function applications foobar ... (n + 1 + 1) =?= foobar ... (n + 2) are defeq because the arguments n + 1 + 1 =?= n + 2 are defeq.

[Kevin Buzzard]

I was surprised by your diagnosis because I had not even supplied a mwe, but indeed by rfl is twice as quick and by with_reducible rfl even quicker (under a second). Thanks!

[Sebastian Ullrich]

I assumed it would be easier to use your full example from the other thread than to build my own :)

[Mario Carneiro]

@Kevin Buzzard said:

But the second [step] expands intp a [Meta.isDefEq] and then a []

By the way, the symbology here is that a [] step has the same label as its parent, so these are both Meta.isDefEq traces