refl taking 20 seconds

Stream: general

[Justus Springer]

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!

Code

def Spec.functor_to_SheafedSpace : CommRingᵒᵖ ⥤ SheafedSpace CommRing :=
{ obj := λ R, {
    carrier := Spec.Top_functor.obj R,
    ..structure_sheaf (unop R : CommRing)
  },
  map := λ R S f, {
    base := Spec.Top_functor.map f,
    c := {
      app := λ U, structure_sheaf.comap f.unop (unop U)
        ((topological_space.opens.map (Spec.Top_functor.map f)).obj (unop U)) (λ p, iff.rfl),
      naturality' := λ U V i, ring_hom.ext $ λ s, subtype.eq $ funext $ λ p,
      begin
        dsimp only [PresheafedSpace.mk_coe],
        rw [category_theory.comp_apply, structure_sheaf.comap_apply],
        refl,
      end
      }
    },
  map_id' := λ R, PresheafedSpace.ext _ _ (Spec.Top_functor.map_id R) $
    category_theory.nat_trans.ext _ _ $ funext $ λ U,
  begin
    dsimp only [PresheafedSpace.mk_coe,
      Top.presheaf.pushforward_obj_obj, Top.presheaf.pushforward_obj_map,
      functor.op_obj, functor.op_map, functor.comp_obj,
      nat_trans.comp_app, nat_trans.op_app,
      SheafedSpace.id_base, SheafedSpace.id_c_app,
      whisker_right_app, topological_space.opens.map_iso_inv_app,
      unop_op, unop_id],
    erw [PresheafedSpace.id_c_app, structure_sheaf.comap_id], swap,
    { rw [Spec.Top_functor.map_id, topological_space.opens.map_id_obj_unop] },
    rw [eq_to_hom_op, eq_to_hom_map, eq_to_hom_trans],
    refl,
  end,
  map_comp' := λ R S T f g,
    PresheafedSpace.ext _ _ (Spec.Top_functor.map_comp f g) $
    category_theory.nat_trans.ext _ _ $ funext $ λ U,
  begin
    dsimp only [PresheafedSpace.mk_coe,
      Top.presheaf.pushforward_obj_obj, Top.presheaf.pushforward_obj_map,
      functor.op_obj, functor.op_map, functor.comp_obj,
      nat_trans.comp_app, nat_trans.op_app,
      SheafedSpace.comp_base, SheafedSpace.comp_c_app,
      whisker_right_app, topological_space.opens.map_iso_inv_app,
      unop_op, unop_comp, eq_to_hom_refl, category_theory.op_id],
    rw [Top.presheaf.pushforward.comp_inv_app, ← category.assoc],
    dsimp only [Top.presheaf.pushforward_obj_obj, functor.op_obj, unop_op],
    rw ← (structure_sheaf (unop R : CommRing)).presheaf.map_id,
    erw structure_sheaf.comap_comp g.unop f.unop _
      ((topological_space.opens.map (Spec.Top_functor.map g)).obj (unop U)) _ _ _,
    change (_ ≫ _) ≫ _ = (_ ≫ _) ≫ _,
    refl,
  end
}

[Eric Wieser]

Does using dsimp before refl help?

[Justus Springer]

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

[Johan Commelin]

@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]

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

[Johan Commelin]

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

[Adam Topaz]

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

[Bryan Gin-ge Chen]

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]

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

[Justus Springer]

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]

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