Zulip Chat Archive

Stream: maths

Topic: Heavy rfl

Heather Macbeth (Sep 08 2024 at 20:15):

For a talk, I would like to have some examples of "heavy rfl" (EDIT: or "heavy show" or "heavy change"), ideally ones that are a little bit interesting mathematically. I'll discuss them as illustrations of a remark of Scholze:

You know this old joke where a professor gets asked whether some step really is obvious, and then he sits down for half an hour, after which he says “Yes, it is obvious”. It turns out that computers can be like that, too! Sometimes the computer asks you to prove that A=BA=B, and the argument is “That’s obvious — it’s true by definition of AA and BB.” And then the computer works for quite some time until it confirms. I found that really surprising.

Does anyone have either

  • examples they remember offhand
  • a metaprogramming way of searching mathlib for them?

Damiano Testa (Sep 08 2024 at 20:27):

I don't have an example. However, scouring mathlib might be done by replacing rfl with count_heartbeats rfl (or a similar syntax). You could probably write easily a linter that does that systematically, but you could also guess that such a heavy rfl would have a heartbeat bump and do that manually for bumped declarations.

Heather Macbeth (Sep 08 2024 at 20:28):

Nice idea, thanks!

Kyle Miller (Sep 08 2024 at 20:29):

An indirect source of these is decide, which works by doing a "heavy rfl" that the decision procedure for the proposition evaluates to true. That's not exactly what you're asking for, but maybe it's interesting too.

Heather Macbeth (Sep 08 2024 at 20:30):

I'd still like some examples of the "direct" kind, but this would indeed be an interesting tangent.

Kyle Miller (Sep 08 2024 at 20:33):

(Detail: decide creates the proof term of_decide_eq_true (rfl : decide theTargetProposition = true))

Patrick Massot (Sep 08 2024 at 20:44):

One way to search for old examples would be to search PR descriptions for “remove heavy rfl”.

Damiano Testa (Sep 09 2024 at 10:53):

I have been thinking for quite some time of a way of testing which tactic combination is faster, so I took this as an excuse to start on that!

#16626 has a very simple-minded approach to the question: every time that there is a tactic rfl, the linter times is and, if takes over 10^5 heartbeats, it tells you the number of heartbeats that it took.

Damiano Testa (Sep 09 2024 at 10:59):

It also has to skip some declarations, since they are too "weird", mostly having to do with the fact that the linter runs after the main declaration has been parsed and so it is hard to consistently rename the new declaration to parse. Nevertheless, you can see that it does flag some rfls that exceed the threshold. For instance, the two rfls in docs#TensorProduct.AlgebraTensorModule.assoc take 612520 and 607227 heartbeats respectively.

Damiano Testa (Sep 09 2024 at 11:06):

Once the linter will have finished its run, there might be some more structured report, but for the moment, I spotted AlgebraCat.forget₂_map_associator_inv whose by rfl proof takes 36,216,407 heartbeats.

Kim Morrison (Sep 09 2024 at 11:42):

Are you forgetting to divide by 1000 (some internal functions use heartbeats at a different granularity)? Given there are no maxHeartbeats options on those functions you numbers don't seem possible.

Damiano Testa (Sep 09 2024 at 11:50):

Probably: the heartbeat count for 0 = 0 := by rfl was in the region of 5k.

Damiano Testa (Sep 09 2024 at 11:59):

These should be the declarations that contain a tactic rfl that takes over 10^9 heartbeats (probably over 10^6 heartbeat, per Kim's comment above):

File Heartbeats Declaration
Geometry/RingedSpace/PresheafedSpace/Gluing.lean:399 1020361 AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π
Algebra/Category/ModuleCat/Monoidal/Symmetric.lean:48 1021317 ModuleCat.MonoidalCategory.hexagon_forward
LinearAlgebra/TensorProduct/Graded/External.lean:107 1049700 TensorProduct.gradedComm_symm
CategoryTheory/Abelian/RightDerived.lean:287 1110185 CategoryTheory.Functor.toRightDerivedZero
Geometry/RingedSpace/LocallyRingedSpace.lean:246 1123263 AlgebraicGeometry.LocallyRingedSpace.emptyTo
Analysis/InnerProductSpace/Calculus.lean:288 1326753 hasStrictFDerivAt_euclidean
Analysis/InnerProductSpace/Calculus.lean:294 1327102 hasFDerivWithinAt_euclidean
Algebra/Category/ModuleCat/Monoidal/Basic.lean:114 1783044 ModuleCat.MonoidalCategory.associator_naturality_aux
Analysis/Normed/Algebra/QuaternionExponential.lean:35 2127769 Quaternion.expSeries_even_of_imaginary
NumberTheory/NumberField/Units/Regulator.lean:66 2414031 NumberField.Units.abs_det_eq_abs_det
LinearAlgebra/TensorProduct/Basic.lean:1016 2459207 TensorProduct.tensorTensorTensorComm_symm
CategoryTheory/GradedObject/Trifunctor.lean:497 2993738 CategoryTheory.GradedObject.isColimitCofan₃MapBifunctorBifunctor₂₃MapObj
CategoryTheory/GradedObject/Trifunctor.lean:318 3299079 CategoryTheory.GradedObject.isColimitCofan₃MapBifunctor₁₂BifunctorMapObj
NumberTheory/NumberField/Units/Regulator.lean:59 4833252 NumberField.Units.regulator_eq_det'
Algebra/Lie/TensorProduct.lean:47 5400103 TensorProduct.LieModule.lieRingModule
Algebra/Category/AlgebraCat/Monoidal.lean:58 9445451 AlgebraCat.forget₂_map_associator_hom
AlgebraicGeometry/Spec.lean:111 11936345 AlgebraicGeometry.Spec.sheafedSpaceMap_comp
NumberTheory/NumberField/Discriminant.lean:72 19571673 NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis
Algebra/Category/AlgebraCat/Monoidal.lean:66 36216407 AlgebraCat.forget₂_map_associator_inv

Damiano Testa (Sep 09 2024 at 12:00):

By chance, I had spotted the heaviest just looking at the build, while it was in progress.

Damiano Testa (Sep 09 2024 at 12:03):

(Btw, filenames, line numbers, the heartbeat counts and the last segment of the declaration names are "correct".

Do not take the namespaces of the declarations too seriously, though: I had direct access to the name in the source, but not easily to the namespaces, so some are guesses. Some declarations are private too.)

Heather Macbeth (Sep 09 2024 at 21:45):

@Damiano Testa This is so cool! Thanks for writing this tooling, I am looking forward to investigating the monsters.

Damiano Testa (Sep 09 2024 at 21:52):

Honestly, I think that it requires more fine tuning, but I hope that it will be useful!

Damiano Testa (Sep 09 2024 at 21:53):

I would really like to have a way of testing large scale, local changes, such when is a terminal refine faster than an exact and similar modifications. Yours was a good excuse to get started!

Heather Macbeth (Sep 09 2024 at 21:55):

I actually have a very similar application I'm curious about (I am writing a linarith? which self-replaces to linear_combination, and although it seems likely that the linear_combinations are faster, I'd like to know the scale of the speedup more precisely). So I'll be glad to use future versions too.

Damiano Testa (Sep 09 2024 at 21:59):

Ok, I'll try to extract a test that takes as input a Syntax → CommandElabM (Array Syntax) and for each command, computes the array, and reports the times of the elaborations of each entry of the array.

Damiano Testa (Sep 09 2024 at 22:00):

I imagine that most replacements will be comparing the original command to a simple variation, but the setup naturally gives a CommandElabM for free.

Heather Macbeth (Sep 10 2024 at 20:16):

Kim Morrison said:

Are you forgetting to divide by 1000 (some internal functions use heartbeats at a different granularity)? Given there are no maxHeartbeats options on those functions you numbers don't seem possible.

Trying to reverse-engineer what the multiplier is here .... On the first one I tried (docs#hasFDerivWithinAt_euclidean), count_heartbeats says 37,577 and Damiano's table says 1,327,102. Is that factor of 35 what one would expect?

Heather Macbeth (Sep 10 2024 at 20:24):

By the way, @Damiano Testa, if you have time for a variant: could we also get the "heavy exacts"? Is this the only line which needs to be adjusted?

Heather Macbeth (Sep 10 2024 at 21:03):

Another observation about docs#hasFDerivWithinAt_euclidean: when I replace the whole proof (including the rfl) by sorry, the declaration still takes 34,053 heartbeats. Does this mean that it's not the rfl itself which is heavy, but rather typechecking the statement of the theorem?

Damiano Testa (Sep 10 2024 at 21:12):

I did not have a chance to implement today what I mention that I would.

Damiano Testa (Sep 10 2024 at 21:12):

There is another place where there is a change, namely here.

Damiano Testa (Sep 10 2024 at 21:14):

The line that you highlighted above is a check to speed things up: the linter will not do anything if the command does not contain a rfl. The rest of the code is what the linter will do, in case there is one. The line that I linked to is where you tell what syntax replacement it should do: if the node is a rfl, then you add count_heartbeats_over before it.

Damiano Testa (Sep 10 2024 at 21:15):

I have not thought about tactics that have more than one node (like exact and unlike rfl), but looking at the code, it may "just work".

Damiano Testa (Sep 10 2024 at 21:18):

Heather Macbeth said:

Another observation about docs#hasFDerivWithinAt_euclidean: when I replace the whole proof (including the rfl) by sorry, the declaration still takes 34,053 heartbeats. Does this mean that it's not the rfl itself which is heavy, but rather typechecking the statement of the theorem?

I guess so, although count_heartbeats_over is supposed to measure the execution of the tactic sequence that follows it (i.e. just rfl in this case), so I am not really sure what this means.

Heather Macbeth (Sep 10 2024 at 21:50):

Damiano Testa said:

I have not thought about tactics that have more than one node (like exact and unlike rfl), but looking at the code, it may "just work".

I just tried to search for "heavy exact", naively changing the important line to

  let repl ← stx.replaceM fun s => do
    match s with
      | .node _ ``Lean.Parser.Tactic.exact _ =>
        return some (← `(tactic| count_heartbeats_over $hbStx ($(⟨s⟩); done)))

and it seems to be producing a lot of false positives. The first thing it flagged was docs#Relation.church_rosser, which count_heartbeats says takes 396 heartbeats -- so in some way the 10 ^ 5 figure is off. Or it is counting something different?

Damiano Testa (Sep 10 2024 at 22:19):

Until Kim mentioned it, I was not aware that there were different heartbeats. The linter uses docs#Mathlib.CountHeartbeats.tacticCount_heartbeats_ (actually, a very small modification, since logInfo would not print).

Damiano Testa (Sep 10 2024 at 22:21):

As for the false positives, I would have to inspect what is the actual syntax that it uses. It took a few attempts to get rfl to work, mostly because I was trying to get something up and running. I would probably have to make a more structured change to get it to work more reliably.

Heather Macbeth (Sep 10 2024 at 22:23):

Bumping up from 10^5 to 10^7 radically reduces the output (unsurprisingly), and the examples produced seem to be genuine "heavy exacts". For example, in docs#instConditionallyCompleteLinearOrderTropical: this is 1,219 heartbeats if the two exacts are sorried, and 56,785 if they are not.

Damiano Testa (Sep 10 2024 at 22:24):

Actually, this appears to be the source of the heartbeat difference: https://github.com/leanprover-community/mathlib4/blob/65a6ba86609c8a2ab0d1de88a71063aa21ccbc23/Mathlib%2FUtil%2FCountHeartbeats.lean#L97.

Damiano Testa (Sep 10 2024 at 22:25):

I'm glad it is more reliable now! The whole linter is a prototype: I hope that it produces usable information, but it may not be fully reliable.

Heather Macbeth (Sep 10 2024 at 22:28):

Also, the second example I tried on your "heavy rfls" list, docs#TensorProduct.tensorTensorTensorComm_symm, seems to be "for real" even if the first one I tried is not. It's 659 heartbeats when sorried and 4,409 when not!

Heather Macbeth (Sep 10 2024 at 22:28):

Also:

-- Porting note: the proof here was `rfl` but that caused a timeout.

Heather Macbeth (Sep 10 2024 at 22:49):

@Damiano Testa Another question occurs to me: Your linter checks for tactic rfls which are slow. How different would a linter to find slow term rfls be?

Heather Macbeth (Sep 10 2024 at 23:41):

I finished running this linter to identify some "heavy exact"s in mathlib -- that is, effectively, term-mode proofs which take a long time to typecheck (but not all of them -- just the ones which form one line of a larger tactic-mode proof -- and with some false positives -- the ones including, e.g., a by simp).

Because of the caveats, I'm not sure how interesting this is, but here it is for the curious!

Heather Macbeth (Sep 11 2024 at 00:13):

Despite the false positives, there are some interesting examples of slow-typechecking proof terms here. For example, in docs#eVariationOn.comp_eq_of_monotoneOn, where filling one _ would cause a 25x speedup, cc @Sébastien Gouëzel:

import Mathlib.Topology.EMetricSpace.Basic

open Set ENNReal

variable {α : Type*} [LinearOrder α] {β : Type*} [LinearOrder β] {E : Type*} [PseudoEMetricSpace E]

noncomputable def eVariationOn (f : α → E) (s : Set α) : ℝ≥0∞ :=
  ⨆ p : ℕ × { u : ℕ → α // Monotone u ∧ ∀ i, u i ∈ s },
    ∑ i ∈ Finset.range p.1, edist (f (p.2.1 (i + 1))) (f (p.2.1 i))

theorem comp_le_of_monotoneOn (f : α → E) {s : Set α} {t : Set β} (φ : β → α) (hφ : MonotoneOn φ t)
    (φst : MapsTo φ t s) : eVariationOn (f ∘ φ) t ≤ eVariationOn f s :=
  sorry

-- 13741 heartbeats
example (f : α → E) {t : Set β} {φ : β → α} {ψ : α → β} (ψts : MapsTo ψ (φ '' t) t)
    (hψ : MonotoneOn ψ (φ '' t)) :
    eVariationOn (f ∘ φ ∘ ψ) (φ '' t) ≤ eVariationOn (f ∘ φ) t :=
  comp_le_of_monotoneOn _ ψ hψ ψts

-- 511 heartbeats
example (f : α → E) {t : Set β} {φ : β → α} {ψ : α → β} (ψts : MapsTo ψ (φ '' t) t)
    (hψ : MonotoneOn ψ (φ '' t)) :
    eVariationOn (f ∘ φ ∘ ψ) (φ '' t) ≤ eVariationOn (f ∘ φ) t :=
  comp_le_of_monotoneOn (f ∘ φ) ψ hψ ψts

Damiano Testa (Sep 11 2024 at 04:10):

Heather Macbeth said:

Damiano Testa Another question occurs to me: Your linter checks for tactic rfls which are slow. How different would a linter to find slow term rfls be?

This could also be done, but the solutions that I had in mind would have required more code:

  • writing a "term mode count heartbeats", or
  • replacing term-mode rfl with by count_heartbeats rfl -- and the proof may break, or
  • looking for declaration := rfl and prefixing it with count_heartbeats in that requires more extensive syntax-matching.

Nothing hard, just more time coding! :smile:

Heather Macbeth (Sep 11 2024 at 21:23):

Very interesting that the term-mode rfl is harder to filter for than the tactic-mode rfl!

Kim Morrison (Sep 11 2024 at 23:23):

I think actually looking for rfl is not that relevant. The real question is calling isDefEq, which many things do besides rfl. This information is available via set_option profile (and I'm sure is accessible via a wrapper command, although I've not tried this myself).

Heather Macbeth (Sep 12 2024 at 01:13):

That makes a lot of sense, thanks! Is there a way of filtering for all the declarations in the library which spend > x time on isDefEq?

Heather Macbeth (Sep 12 2024 at 01:14):

Or (probably even better, if possible) all individual isDefEq calls in the library which take > x time?

Kim Morrison (Sep 12 2024 at 04:35):

@Heather Macbeth, yes, of course anything is possible. :-) lean#5318 (just an experiment) instruments isDefEq and reports any call that takes over a specified number of heartbeats.

You can try this out in Mathlib by checking out the branch#lean-pr-testing-5318.

The default there is set to report any isDefEq problem taking more than 1000 heartbeats. It just prints the raw expressions, so sometimes the output is very long (I was a bit scared of calling the pretty printer from inside isDefEq!).

You can adjust the threshold locally with set_option profiler.isDefEq.threshold (or globally in the lakefile).

Kim Morrison (Sep 12 2024 at 04:36):

(e.g. go to Mathlib.Algebra.Field.IsField to see the first problem)

Damiano Testa (Sep 12 2024 at 09:32):

I did not know about isDefEq.threshold: seems very useful!

Damiano Testa (Sep 12 2024 at 09:32):

Heather, I guess that I re-purposed a non-existing tool for something that already existed!

Damiano Testa (Sep 12 2024 at 09:33):

Anyway, I still would like to make the linter that computes differences in elaboration more robust.

Kim Morrison (Sep 12 2024 at 10:18):

@Damiano Testa , this is brand new, implemented in response to Heather's query above. It won't be merged as is, but if we can make good use of it we can work out how to deliver something equivalent.

Damiano Testa (Sep 12 2024 at 11:06):

That's great! I think that fine-grained speed measurements are becoming more and more important to seriously inform what changes to make and this looks really useful!

Damiano Testa (Sep 12 2024 at 11:07):

I won't be able to do any Lean-related work for a few days, though, but I'll play with this when I can!

Kim Morrison (Sep 12 2024 at 11:37):

% lake build
ℹ [1465/5061] Built Mathlib.Algebra.Order.Pointwise
info: ././././Mathlib/Algebra/Order/Pointwise.lean:72:4: isDefEq took 50699 heartbeats
ℹ [1760/5061] Built Mathlib.Computability.PartrecCode
info: ././././Mathlib/Computability/PartrecCode.lean:827:32: isDefEq took 21277 heartbeats
info: ././././Mathlib/Computability/PartrecCode.lean:847:32: isDefEq took 21294 heartbeats
info: ././././Mathlib/Computability/PartrecCode.lean:865:9: isDefEq took 21257 heartbeats
ℹ [1987/5061] Built Mathlib.Data.Finset.Pointwise.Basic
info: ././././Mathlib/Data/Finset/Pointwise/Basic.lean:1813:9: isDefEq took 72263 heartbeats
info: ././././Mathlib/Data/Finset/Pointwise/Basic.lean:1818:9: isDefEq took 80645 heartbeats
ℹ [2019/5061] Built Mathlib.Order.Filter.Interval
info: ././././Mathlib/Order/Filter/Interval.lean:263:2: isDefEq took 28050 heartbeats
ℹ [2367/5061] Built Mathlib.ModelTheory.ElementaryMaps
info: ././././Mathlib/ModelTheory/ElementaryMaps.lean:87:9: isDefEq took 67855 heartbeats
ℹ [2553/5061] Built Mathlib.LinearAlgebra.PiTensorProduct
info: ././././Mathlib/LinearAlgebra/PiTensorProduct.lean:864:60: isDefEq took 28243 heartbeats
ℹ [2566/5061] Built Mathlib.Algebra.Polynomial.Basic
info: ././././Mathlib/Algebra/Polynomial/Basic.lean:252:46: isDefEq took 28281 heartbeats
info: ././././Mathlib/Algebra/Polynomial/Basic.lean:252:46: isDefEq took 28165 heartbeats
ℹ [2677/5061] Built Mathlib.Algebra.Module.LocalizedModule
info: ././././Mathlib/Algebra/Module/LocalizedModule.lean:492:9: isDefEq took 48650 heartbeats
ℹ [2725/5061] Built Mathlib.LinearAlgebra.TensorPower
info: ././././Mathlib/LinearAlgebra/TensorPower.lean:119:2: isDefEq took 124474 heartbeats
ℹ [2799/5061] Built Mathlib.Topology.Order.DenselyOrdered
info: ././././Mathlib/Topology/Order/DenselyOrdered.lean:235:2: isDefEq took 144015 heartbeats
ℹ [2808/5061] Built Mathlib.LinearAlgebra.Matrix.ToLin
info: ././././Mathlib/LinearAlgebra/Matrix/ToLin.lean:919:6: isDefEq took 96080 heartbeats
ℹ [2849/5061] Built Mathlib.Topology.EMetricSpace.Basic
info: ././././Mathlib/Topology/EMetricSpace/Basic.lean:167:18: isDefEq took 37875 heartbeats
info: ././././Mathlib/Topology/EMetricSpace/Basic.lean:174:18: isDefEq took 37875 heartbeats
ℹ [3140/5061] Built Mathlib.Algebra.Polynomial.BigOperators
info: ././././Mathlib/Algebra/Polynomial/BigOperators.lean:47:44: isDefEq took 54853 heartbeats
info: ././././Mathlib/Algebra/Polynomial/BigOperators.lean:47:44: isDefEq took 49760 heartbeats
ℹ [3184/5061] Built Mathlib.RingTheory.TensorProduct.MvPolynomial
info: ././././Mathlib/RingTheory/TensorProduct/MvPolynomial.lean:70:2: isDefEq took 35736 heartbeats
info: ././././Mathlib/RingTheory/TensorProduct/MvPolynomial.lean:74:2: isDefEq took 35735 heartbeats
info: ././././Mathlib/RingTheory/TensorProduct/MvPolynomial.lean:165:7: isDefEq took 20030 heartbeats
ℹ [3379/5061] Built Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
info: ././././Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean:40:9: isDefEq took 119575 heartbeats
ℹ [3381/5061] Built Mathlib.Topology.Algebra.UniformRing
info: ././././Mathlib/Topology/Algebra/UniformRing.lean:78:2: isDefEq took 29371 heartbeats
ℹ [3444/5061] Built Mathlib.Algebra.Category.AlgebraCat.Monoidal
info: ././././Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean:59:4: isDefEq took 43633 heartbeats
info: ././././Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean:59:4: isDefEq took 43497 heartbeats
info: ././././Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean:59:4: isDefEq took 43803 heartbeats
info: ././././Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean:67:4: isDefEq took 43648 heartbeats
info: ././././Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean:67:4: isDefEq took 43511 heartbeats
info: ././././Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean:67:4: isDefEq took 43827 heartbeats
info: ././././Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean:72:2: isDefEq took 36166 heartbeats
info: ././././Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean:82:8: isDefEq took 33679 heartbeats
info: ././././Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean:82:8: isDefEq took 33675 heartbeats
info: ././././Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean:84:13: isDefEq took 31286 heartbeats
info: ././././Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean:84:31: isDefEq took 22599 heartbeats
info: ././././Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean:84:31: isDefEq took 31260 heartbeats
info: ././././Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean:84:49: isDefEq took 31271 heartbeats
info: ././././Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean:84:77: isDefEq took 40416 heartbeats
info: ././././Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean:84:77: isDefEq took 31282 heartbeats
ℹ [3452/5061] Built Mathlib.Algebra.Polynomial.Degree.CardPowDegree
info: ././././Mathlib/Algebra/Polynomial/Degree/CardPowDegree.lean:79:2: isDefEq took 26276 heartbeats
info: ././././Mathlib/Algebra/Polynomial/Degree/CardPowDegree.lean:80:2: isDefEq took 26254 heartbeats
info: ././././Mathlib/Algebra/Polynomial/Degree/CardPowDegree.lean:80:2: isDefEq took 26269 heartbeats
ℹ [3461/5061] Built Mathlib.Topology.Connected.PathConnected
info: ././././Mathlib/Topology/Connected/PathConnected.lean:597:8: isDefEq took 20128 heartbeats

Kim Morrison (Sep 12 2024 at 11:37):

ℹ [3587/5061] Built Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
info: ././././Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean:135:22: isDefEq took 24195 heartbeats
info: ././././Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean:486:4: isDefEq took 38029 heartbeats
info: ././././Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean:503:10: isDefEq took 36583 heartbeats
info: ././././Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean:550:8: isDefEq took 89993 heartbeats
info: ././././Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean:622:4: isDefEq took 38040 heartbeats
info: ././././Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean:695:6: isDefEq took 48033 heartbeats
info: ././././Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean:704:4: isDefEq took 48157 heartbeats
info: ././././Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean:822:15: isDefEq took 22566 heartbeats
info: ././././Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean:823:59: isDefEq took 49497 heartbeats
ℹ [3637/5061] Built Mathlib.CategoryTheory.Monoidal.Tor
info: ././././Mathlib/CategoryTheory/Monoidal/Tor.lean:72:2: isDefEq took 28934 heartbeats
ℹ [3704/5061] Built Mathlib.Algebra.Category.ModuleCat.Presheaf
info: ././././Mathlib/Algebra/Category/ModuleCat/Presheaf.lean:527:8: isDefEq took 54517 heartbeats
ℹ [3751/5061] Built Mathlib.RingTheory.FiniteStability
info: ././././Mathlib/RingTheory/FiniteStability.lean:57:4: isDefEq took 47929 heartbeats
ℹ [3788/5061] Built Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
info: ././././Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean:85:35: isDefEq took 34823 heartbeats
info: ././././Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean:85:35: isDefEq took 34642 heartbeats
ℹ [3866/5061] Built Mathlib.LinearAlgebra.Eigenspace.Basic
info: ././././Mathlib/LinearAlgebra/Eigenspace/Basic.lean:232:2: isDefEq took 56628 heartbeats
info: ././././Mathlib/LinearAlgebra/Eigenspace/Basic.lean:471:30: isDefEq took 56644 heartbeats
ℹ [3953/5061] Built Mathlib.Analysis.Convex.Between
info: ././././Mathlib/Analysis/Convex/Between.lean:147:9: isDefEq took 144114 heartbeats
info: ././././Mathlib/Analysis/Convex/Between.lean:153:9: isDefEq took 144124 heartbeats
ℹ [3957/5061] Built Mathlib.Topology.Category.Profinite.Nobeling
info: ././././Mathlib/Topology/Category/Profinite/Nobeling.lean:1364:13: isDefEq took 34347 heartbeats
ℹ [3970/5061] Built Mathlib.RingTheory.Generators
info: ././././Mathlib/RingTheory/Generators.lean:496:28: isDefEq took 41845 heartbeats
ℹ [4063/5061] Built Mathlib.MeasureTheory.Measure.Restrict
info: ././././Mathlib/MeasureTheory/Measure/Restrict.lean:725:62: isDefEq took 37430 heartbeats
info: ././././Mathlib/MeasureTheory/Measure/Restrict.lean:725:62: isDefEq took 38223 heartbeats
ℹ [4094/5061] Built Mathlib.RingTheory.Kaehler.Basic
info: ././././Mathlib/RingTheory/Kaehler/Basic.lean:840:4: isDefEq took 21147 heartbeats
ℹ [4145/5061] Built Mathlib.RingTheory.Smooth.Kaehler
info: ././././Mathlib/RingTheory/Smooth/Kaehler.lean:115:9: isDefEq took 20145 heartbeats
ℹ [4153/5061] Built Mathlib.RingTheory.DedekindDomain.Ideal
info: ././././Mathlib/RingTheory/DedekindDomain/Ideal.lean:592:16: isDefEq took 20884 heartbeats
info: ././././Mathlib/RingTheory/DedekindDomain/Ideal.lean:592:16: isDefEq took 28637 heartbeats
info: ././././Mathlib/RingTheory/DedekindDomain/Ideal.lean:592:15: isDefEq took 28099 heartbeats
ℹ [4181/5061] Built Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
info: ././././Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean:77:37: isDefEq took 41246 heartbeats
ℹ [4300/5061] Built Mathlib.RepresentationTheory.GroupCohomology.Resolution
info: ././././Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean:188:53: isDefEq took 24585 heartbeats
info: ././././Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean:227:56: isDefEq took 23553 heartbeats
info: ././././Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean:247:56: isDefEq took 24205 heartbeats
ℹ [4332/5061] Built Mathlib.RingTheory.Perfection
info: ././././Mathlib/RingTheory/Perfection.lean:551:14: isDefEq took 50379 heartbeats
ℹ [4338/5061] Built Mathlib.Analysis.SpecialFunctions.Pow.Continuity
info: ././././Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean:406:2: isDefEq took 44319 heartbeats
ℹ [4439/5061] Built Mathlib.FieldTheory.IsAlgClosed.Basic
info: ././././Mathlib/FieldTheory/IsAlgClosed/Basic.lean:140:57: isDefEq took 74021 heartbeats
info: ././././Mathlib/FieldTheory/IsAlgClosed/Basic.lean:140:57: isDefEq took 67775 heartbeats
ℹ [4452/5061] Built Mathlib.MeasureTheory.Constructions.Prod.Basic
info: ././././Mathlib/MeasureTheory/Constructions/Prod/Basic.lean:475:2: isDefEq took 23496 heartbeats
ℹ [4461/5061] Built Mathlib.Analysis.NormedSpace.Multilinear.Curry
info: ././././Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean:599:2: isDefEq took 34569 heartbeats
ℹ [4511/5061] Built Mathlib.AlgebraicGeometry.GammaSpecAdjunction
info: ././././Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean:298:43: isDefEq took 27070 heartbeats
ℹ [4532/5061] Built Mathlib.Analysis.InnerProductSpace.Basic
info: ././././Mathlib/Analysis/InnerProductSpace/Basic.lean:2396:2: isDefEq took 38488 heartbeats
ℹ [4545/5061] Built Mathlib.Algebra.Lie.Weights.Chain
info: ././././Mathlib/Algebra/Lie/Weights/Chain.lean:135:6: isDefEq took 32276 heartbeats
ℹ [4608/5061] Built Mathlib.Analysis.Calculus.FDeriv.Mul
info: ././././Mathlib/Analysis/Calculus/FDeriv/Mul.lean:53:2: isDefEq took 49512 heartbeats
ℹ [4619/5061] Built Mathlib.Analysis.Analytic.Composition
info: ././././Mathlib/Analysis/Analytic/Composition.lean:504:6: isDefEq took 71241 heartbeats
ℹ [4678/5061] Built Mathlib.NumberTheory.Liouville.Basic
info: ././././Mathlib/NumberTheory/Liouville/Basic.lean:64:36: isDefEq took 30635 heartbeats
ℹ [4827/5061] Built Mathlib.MeasureTheory.Measure.ProbabilityMeasure
info: ././././Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean:419:8: isDefEq took 44714 heartbeats
info: ././././Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean:444:8: isDefEq took 75140 heartbeats
ℹ [4843/5061] Built Mathlib.Analysis.Calculus.ParametricIntegral
info: ././././Mathlib/Analysis/Calculus/ParametricIntegral.lean:296:11: isDefEq took 26826 heartbeats
ℹ [4937/5061] Built Mathlib.MeasureTheory.Function.Jacobian
info: ././././Mathlib/MeasureTheory/Function/Jacobian.lean:800:25: isDefEq took 41304 heartbeats
info: ././././Mathlib/MeasureTheory/Function/Jacobian.lean:800:25: isDefEq took 41215 heartbeats
info: ././././Mathlib/MeasureTheory/Function/Jacobian.lean:800:25: isDefEq took 39248 heartbeats
info: ././././Mathlib/MeasureTheory/Function/Jacobian.lean:922:25: isDefEq took 41295 heartbeats
info: ././././Mathlib/MeasureTheory/Function/Jacobian.lean:922:25: isDefEq took 41195 heartbeats
info: ././././Mathlib/MeasureTheory/Function/Jacobian.lean:922:25: isDefEq took 39232 heartbeats
ℹ [4980/5061] Built Mathlib.Probability.Kernel.Disintegration.Density
info: ././././Mathlib/Probability/Kernel/Disintegration/Density.lean:137:2: isDefEq took 106278 heartbeats
info: ././././Mathlib/Probability/Kernel/Disintegration/Density.lean:142:2: isDefEq took 106391 heartbeats
ℹ [4982/5061] Built Mathlib.NumberTheory.NumberField.Units.Basic
info: ././././Mathlib/NumberTheory/NumberField/Units/Basic.lean:142:10: isDefEq took 108159 heartbeats
ℹ [5033/5061] Built Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
info: ././././Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean:239:6: isDefEq took 31165 heartbeats
ℹ [5049/5061] Built Mathlib.NumberTheory.NumberField.Discriminant
info: ././././Mathlib/NumberTheory/NumberField/Discriminant.lean:366:34: isDefEq took 23313 heartbeats

Kim Morrison (Sep 12 2024 at 11:38):

Shall we institute an award for the heaviest rfl in Mathlib? :-)

Heather Macbeth (Sep 12 2024 at 20:26):

I've only looked at a few of these examples so far, but some are pretty mysterious. For example, this is a more-minimal WE of the example docs#AffineEquiv.sbtw_map_iff from Analysis/Convex:

import Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

variable (R : Type*) {V V' P P' : Type*}
variable [OrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P]
variable [AddCommGroup V'] [Module R V'] [AddTorsor V' P']

open AffineMap

def Sbtw (x y z : P) : Prop := y ∈ lineMap x y '' Set.Icc (0 : R) 1 ∧ y ≠ x ∧ y ≠ z

variable {R}

theorem Function.Injective.sbtw_map_iff {x y z : P} {f : P →ᵃ[R] P'} (hf : Function.Injective f) :
    Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z :=
  sorry

-- 146454 heartbeats
example {x y z : P} (f : P ≃ᵃ[R] P') : Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z :=
  let hf : Function.Injective f.toAffineMap := AffineEquiv.injective f
  Function.Injective.sbtw_map_iff hf

-- 762 heartbeats
example {x y z : P} (f : P ≃ᵃ[R] P') : Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z :=
  let hf : Function.Injective f.toAffineMap := AffineEquiv.injective f
  hf.sbtw_map_iff

Heather Macbeth (Sep 12 2024 at 20:27):

There is a mystifying discrepancy between the isDefEq time on Function.Injective.sbtw_map_iff hf and on hf.sbtw_map_iff. Could this issue somehow be about the pretty-printing of dot notation?

Matthew Ballard (Sep 12 2024 at 20:29):

Looks like there are more metavariables in unification problem 1 than 2

Heather Macbeth (Sep 12 2024 at 20:29):

@Matthew Ballard Interesting, how do you see this?

Matthew Ballard (Sep 12 2024 at 20:30):

set_option trace.Meta.isDefEq true in
set_option profiler true in
set_option trace.Meta.synthInstance true in

is my standard invocation

Matthew Ballard (Sep 12 2024 at 20:32):

The last line is just noise here though I think

Matthew Ballard (Sep 12 2024 at 20:43):

Equally fast: 

example {x y z : P} (f : P ≃ᵃ[R] P') : Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z :=
  let hf : Function.Injective f.toAffineMap := AffineEquiv.injective f
  Function.Injective.sbtw_map_iff (R := R) (V := V) (V' := V') (P := P) (P' := P') (f := f) hf

Heather Macbeth (Sep 12 2024 at 20:44):

How bizarre. I've been trying to poke around the trace with the options you sent but I don't really know how to read them -- where do I see the two relevant unification problems with their different numbers of metavariables?

Matthew Ballard (Sep 12 2024 at 20:50):

In the infoview, looking for the biggest time in [...] usually revels the culprit. For the first one, Lean ends up at the following defeq problem

[Meta.isDefEq] [5.349034] ❌️ Sbtw R (f x) (f y) (f z) ↔
      Sbtw R x y
        z =?= Sbtw ?m.9604 (?m.9619 ?m.9616) (?m.9619 ?m.9617) (?m.9619 ?m.9618) ↔ Sbtw ?m.9604 ?m.9616 ?m.9617 ?m.9618 ▶

where 

@DFunLike.coe (?m.9607 →ᵃ[?m.9604] ?m.9608) ?m.9607 (fun a => ?m.9608) (AffineMap.instFunLike ?m.9604 ?m.9607 ?m.9608)
  ?m.9619 :
?m.9607 → ?m.9608

While in the second it already knows that you should use the coercion of f instead

Heather Macbeth (Sep 12 2024 at 21:16):

Thanks, that helps me skim a bit better.

Should I be understanding this as saying that the following two things elaborate differently?

axiom Foo : Type
axiom Foo.bar : Foo → Nat

variable (x : Foo)

#check x.bar

#check Foo.bar x

Yuma Mizuno (Sep 13 2024 at 19:45):

I tackled those around AlgebraCat.forget₂_map_associator_inv.
#16776

Heather Macbeth (Sep 17 2024 at 05:36):

This conversation about finding heavy rfls went in several interesting directions, and produced Kim's lean4#5318, which searches for heavy isDefEqs in mathlib. I've now explored the list produced, and it seems to me that these are not quite what I had hoped to find: most of these heaviest isDefEqs in mathlib arise in checking a proof term (IIUC, unifying the goal with the type of the proof term).

My original motivation was to get some examples for a talk. For this, I would really like to have examples of "true" heavy rfl/change/show. To distinguish these isDefEqs from the ones which arise in checking proof terms, would it work to look for examples in which neither of the two terms being compared contains metavariables?

Mario Carneiro (Sep 17 2024 at 05:54):

I think unification should not be that slow if it's not hiding a "true" heavy rfl. Do you have an example?

Heather Macbeth (Sep 17 2024 at 13:36):

@Mario Carneiro Interesting! Here's one example.

Kim Morrison (Sep 18 2024 at 00:00):

Heather Macbeth said:

Mario Carneiro Interesting! Here's one example.

It would be great, if someone were interested, to try to produce a minimization of that example, so that we could work on improving the performance there.

Last updated: May 02 2025 at 03:31 UTC