Zulip Chat Archive

Stream: general

Topic: refl taking 20 seconds

Justus Springer (May 27 2021 at 11:39):

On my branch spec_functor, I have a working version of the spectrum functor, from commutative rings to sheafed spaces (see below). Unfortunately, it is very slow and I don't know how to optimize it further... The bulk of the time is consumed by the very last refl in the proof of map_comp, which takes almost 20 seconds on my machine. I included a change right before to match up the terms, without that, it takes almost 40 seconds!

One problem is that I can't use rw with the involved definitional equalities directly (mainly Spec.Top_functor.map_comp), because the motive is not type correct. My questions are: Can I trace what refl is doing somehow? And can I "give some hints" to the unifier to speed things up somehow? Thanks in advance for any help!


Eric Wieser (May 27 2021 at 11:39):

Does using dsimp before refl help?

Justus Springer (May 27 2021 at 11:42):

Unfortunately not, dsimp fails, nothing gets simplified...

Johan Commelin (May 27 2021 at 12:07):

@Justus Springer What I usually do is to split the definition into smaller pieces. So I would start by giving

{  carrier := Spec.Top_functor.obj R,
    ..structure_sheaf (unop R : CommRing) },

it's own name. And if you stick @[simps] above that definition, Lean will automatically generate some useful simp-lemmas.

Johan Commelin (May 27 2021 at 12:07):

Then I would define map separately, and again stick @[simps] above it.

Johan Commelin (May 27 2021 at 12:08):

Those freshly generated simp-lemmas will then hopefully help to make the proofs of map_id' and map_comp' more manageable

Adam Topaz (May 27 2021 at 14:52):

Don't we have something on the website about this so-called heavy refl?

Bryan Gin-ge Chen (May 27 2021 at 15:50):

For tracing what Lean is doing in a rfl proof (which should also work with refl), you can use:

  • set_option trace.type_context.is_def_eq true
  • set_option trace.type_context.is_def_eq_detail true

(@Kevin Buzzard posted a list of helpful options here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/your.20favourite.20set_option.20option/near/201825547)

Bryan Gin-ge Chen (May 27 2021 at 15:50):

It would be good to add some of this info to our website too!

Justus Springer (May 27 2021 at 17:32):

Thanks for the replies!
I did not know about these options. As soon as I turn on trace.type_context.is_def_eq_detail, I get a timeout, which is probably not a good sign...

Justus Springer (May 27 2021 at 17:32):

I will try to split things up into smaller pieces, as Johan suggested.

Last updated: Aug 03 2023 at 10:10 UTC