Zulip Chat Archive

Stream: general

Topic: Intermediate `have` speeds up elaboration


Oliver Nash (Mar 27 2021 at 17:20):

I am surprised by the difference in elaboration speed in smooth.div_slow and smooth.div_fast in the below:

import geometry.manifold.algebra.lie_group

variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
          {H : Type*} [topological_space H]
          {E : Type*} [normed_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H}
          {G : Type*} [topological_space G] [charted_space H G] [group G] [lie_group I G]
          {E' : Type*} [normed_group E'] [normed_space 𝕜 E']
          {H' : Type*} [topological_space H'] {I' : model_with_corners 𝕜 E' H'}
          {M : Type*} [topological_space M] [charted_space H' M]

set_option profiler true

@[to_additive]
lemma smooth.div_slow {f g : M  G} -- elaboration of smooth.div took 6.38s
  (hf : smooth I' I f) (hg : smooth I' I g) : smooth I' I (f / g) :=
begin
  rw div_eq_mul_inv,
  exact (smooth_mul I).comp (hf.prod_mk hg.inv),
end

lemma smooth.div_fast {f g : M  G} -- elaboration of smooth.div took 79.1ms
  (hf : smooth I' I f) (hg : smooth I' I g) : smooth I' I (f / g) :=
begin
  rw div_eq_mul_inv,
  have h := (smooth_mul I).comp (hf.prod_mk hg.inv),
  exact h,
end

Oliver Nash (Mar 27 2021 at 17:21):

By introducing a pointless intermediate have, elaboration speeds up by a factor of 80! Is there an explanation for this and/or a guide for how to deal with this?

Kevin Buzzard (Mar 27 2021 at 17:22):

Does exact ((smooth_mul I).comp (hf.prod_mk hg.inv) : _) make it fast?

Oliver Nash (Mar 27 2021 at 17:22):

Yes!

Oliver Nash (Mar 27 2021 at 17:22):

131ms elaboration time.

Kevin Buzzard (Mar 27 2021 at 17:22):

I've seen this trick before :-)

Oliver Nash (Mar 27 2021 at 17:23):

This is black magic to me. I'd love if there was a thread I could read about it somewhere.

Johan Commelin (Mar 27 2021 at 17:24):

@Oliver Nash When you do exact some_expr, Lean will check that this expression has the expected type.

Kevin Buzzard (Mar 27 2021 at 17:24):

The exact version attempts to elaborate (smooth_mul I).comp (hf.prod_mk hg.inv) with the type of the goal, which apparently gets the elaborator confused. The have h version elaborates it with whatever type comes out, and then the exact attempts to make that type equal to the goal, which sometimes produces very different results!

Eric Wieser (Mar 27 2021 at 17:24):

Adding the : _) means roughly "elaborate this expression as much as possible before continuing"

Johan Commelin (Mar 27 2021 at 17:24):

But with have or the (some_expr : _) variant, you ask Lean to infer the type, and then check this type is defeq to what Lean expects.

Johan Commelin (Mar 27 2021 at 17:25):

And the order in which the infer and check happen, matters a lot for speed.

Oliver Nash (Mar 27 2021 at 17:25):

OK I more or less understand. Library note?

Oliver Nash (Mar 27 2021 at 17:25):

I should also say: thanks. I didn't expect a barrage of such helpful answers so quickly :-)

Johan Commelin (Mar 27 2021 at 17:26):

I wouldn't be enough of an expert to write more than the two lines I just wrote. But someone who actually understands type theory and Lean can maybe help us out (-;

Oliver Nash (Mar 27 2021 at 17:26):

Maybe I'll create a library note PR and tag someone on GH so that they can actually fill it in with a bit more?


Last updated: Dec 20 2023 at 11:08 UTC