Interpreting benchmark results

Stream: mathlib4

[Daniel Weber]

In #14637 I attempted to make nonZeroDivisors.ne_zero a simp lemma, and when running a benchmark it says that Mathlib.NumberTheory.ModularForms.SlashActions got slower by 24.0%. How significant is that? Enough to make this change bad?

[Kyle Miller]

On individual modules, I'm not sure how interpretable the results are unless you go in and figure out what got slower. To me, it's somewhat significant that mathlib took 0.2% more instructions to build. That's not enough to say it's bad, but it's enough to think about whether this simp lemma is worth it.

[Kyle Miller]

I would suggest not having this simp lemma, because it means that whenever x ≠ 0 is seen, then simp will try to synthesize a MonoidWithZero M instance, a Nontrivial M instance, and a proof of x ∈ nonZeroDivisors M. How often do we expect that third condition to hold?

[Daniel Weber]

I see, not very often. Making nonZeroDivisors.coe_ne_zero simp should be fine though, right?

[Damiano Testa]

Michael Stoll posted a script to summarize the bench output. I have a branch where I would like to make it post the summary on every !bench. I have not done that yet, but this is what it would say in your case:

File	Instructions	%
Increase
build	+250.764⬝10⁹	(+0.20%)
lint	+160.357⬝10⁹	(+2.0%)
Mathlib.NumberTheory.ModularForms.SlashActions	+18.499⬝10⁹	(+24.4%)
Mathlib.Topology.ContinuousFunction.NonUnitalFunctionalCalculus	+7.876⬝10⁹	(+3.14%)
Mathlib.AlgebraicGeometry.EllipticCurve.Affine	+7.836⬝10⁹	(+3.75%)
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody	+6.697⬝10⁹	(+3.81%)
Mathlib.Algebra.Lie.Weights.Killing	+5.962⬝10⁹	(+2.63%)
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme	+3.722⬝10⁹	(+1.33%)
Mathlib.NumberTheory.ArithmeticFunction	+3.595⬝10⁹	(+4.28%)
Mathlib.NumberTheory.NumberField.Units.DirichletTheorem	+3.569⬝10⁹	(+2.15%)
Mathlib.Algebra.Polynomial.Div	+3.19⬝10⁹	(+7.68%)
Mathlib.NumberTheory.Zsqrtd.Basic	+2.746⬝10⁹	(+3.42%)
Mathlib.RingTheory.AlgebraicIndependent	+2.706⬝10⁹	(+4.98%)
Mathlib.Analysis.MeanInequalities	+2.671⬝10⁹	(+4.65%)
Mathlib.Algebra.Lie.Weights.Chain	+2.625⬝10⁹	(+3.20%)
Mathlib.LinearAlgebra.Dual	+2.617⬝10⁹	(+0.67%)
Mathlib.Algebra.MvPolynomial.Basic	+2.346⬝10⁹	(+2.63%)
Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls	+2.293⬝10⁹	(+3.59%)
Mathlib.NumberTheory.Padics.PadicIntegers	+2.286⬝10⁹	(+4.64%)
Mathlib.RingTheory.UniqueFactorizationDomain	+2.273⬝10⁹	(+2.64%)
Mathlib.RingTheory.MvPolynomial.Homogeneous	+2.261⬝10⁹	(+5.74%)
Mathlib.Analysis.SpecialFunctions.Pow.NNReal	+2.257⬝10⁹	(+5.99%)
Mathlib.Geometry.Euclidean.Angle.Oriented.Basic	+2.27⬝10⁹	(+1.58%)
Mathlib.RingTheory.PowerSeries.Order	+1.974⬝10⁹	(+9.15%)
Mathlib.Algebra.Algebra.Quasispectrum	+1.925⬝10⁹	(+2.26%)
Mathlib.RingTheory.Polynomial.Cyclotomic.Eval	+1.858⬝10⁹	(+5.92%)
Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas	+1.722⬝10⁹	(+3.90%)
Mathlib.RingTheory.PowerSeries.Inverse	+1.616⬝10⁹	(+6.7%)
Mathlib.Probability.Distributions.Gaussian	+1.600⬝10⁹	(+5.20%)
Mathlib.MeasureTheory.Function.L1Space	+1.567⬝10⁹	(+1.46%)
Mathlib.MeasureTheory.Integral.CircleIntegral	+1.558⬝10⁹	(+2.26%)
Mathlib.RingTheory.Polynomial.Basic	+1.545⬝10⁹	(+1.91%)
Mathlib.Algebra.Polynomial.RingDivision	+1.512⬝10⁹	(+3.7%)
Mathlib.Analysis.Analytic.IsolatedZeros	+1.472⬝10⁹	(+2.71%)
Mathlib.Algebra.Quaternion	+1.460⬝10⁹	(+0.69%)
Mathlib.Analysis.NormedSpace.lpSpace	+1.410⬝10⁹	(+0.57%)
Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact	+1.388⬝10⁹	(+2.84%)
Mathlib.LinearAlgebra.Dimension.Finite	+1.341⬝10⁹	(+2.2%)
Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated	+1.324⬝10⁹	(+0.96%)
Mathlib.Algebra.Lie.Weights.RootSystem	+1.315⬝10⁹	(+0.68%)
Mathlib.Topology.ContinuousFunction.FunctionalCalculus	+1.286⬝10⁹	(+1.1%)
Mathlib.Analysis.SpecialFunctions.Complex.LogBounds	+1.285⬝10⁹	(+3.76%)
Mathlib.MeasureTheory.Measure.Hausdorff	+1.251⬝10⁹	(+2.3%)
Mathlib.Analysis.Complex.UpperHalfPlane.Basic	+1.239⬝10⁹	(+1.59%)
Mathlib.Analysis.Convex.EGauge	+1.216⬝10⁹	(+6.42%)
Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol	+1.213⬝10⁹	(+4.73%)
Mathlib.LinearAlgebra.Matrix.NonsingularInverse	+1.213⬝10⁹	(+2.67%)
Mathlib.NumberTheory.SumFourSquares	+1.200⬝10⁹	(+4.40%)
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic	+1.192⬝10⁹	(+0.77%)
Mathlib.Combinatorics.Additive.AP.Three.Behrend	+1.191⬝10⁹	(+3.4%)
Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation	+1.184⬝10⁹	(+1.64%)
Mathlib.RingTheory.DedekindDomain.Ideal	+1.158⬝10⁹	(+0.66%)
Mathlib.RingTheory.Flat.EquationalCriterion	+1.148⬝10⁹	(+2.19%)
Mathlib.Analysis.Convex.Between	+1.148⬝10⁹	(+0.86%)
Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Instances	+1.143⬝10⁹	(+0.42%)
Mathlib.MeasureTheory.Integral.TorusIntegral	+1.138⬝10⁹	(+3.84%)
Mathlib.LinearAlgebra.CliffordAlgebra.Prod	+1.111⬝10⁹	(+2.9%)
Mathlib.Probability.ProbabilityMassFunction.Constructions	+1.84⬝10⁹	(+5.41%)
Mathlib.Probability.Integration	+1.81⬝10⁹	(+6.99%)
Mathlib.Topology.MetricSpace.Perfect	+1.77⬝10⁹	(+4.4%)
Mathlib.Algebra.Category.Ring.Constructions	+1.71⬝10⁹	(+3.6%)
Mathlib.Geometry.Euclidean.MongePoint	+1.56⬝10⁹	(+1.7%)
Mathlib.Analysis.Calculus.ContDiff.Basic	+1.46⬝10⁹	(+0.24%)
Mathlib.RingTheory.HahnSeries.Summable	+1.39⬝10⁹	(+2.48%)
Mathlib.Analysis.RCLike.Basic	+1.5⬝10⁹	(+1.9%)
Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts	+1.1⬝10⁹	(+2.15%)
Decrease

[Matthew Ballard]

The problem is that Lean figures out which simp theorems to try to use by looking at the expression to be simplified itself only. The leaves a blindspot when there are simp theorems with "simple" statements, like x ≠ 0, but more "complicated" proofs and hence requirements (parameters).

Since the conclusion x ≠ 0 contains no information about needing a MonoidWithZero that is Nontrivial, Lean can't take this into account before trying to apply the theorem. The result is more failed attempts to apply it. The attempts to synthesize MonoidWithZero and Nontrivial come at a cost that, while seemingly small, can snowball over the whole of the library downstream from the declaration.

Looking at the benchmark results, the 0.2% that Kyle mentioned is pretty significant for a change to overall instructions. It is comparable (but in the opposite direction) to ripping out an older less efficient API, like here.

Another data point from the benchmark that indicates that there are a lot of false positives with this as a simp theorem is the fact that linting instructions increased by 2% overall. Linting is dominated by the simpNF linter which tries to check normal forms for all simp theorems (in addition to other checks) by running simp on them. It needs to do a noticable amount more work (10s by wall clock but that tends to be more random than instructions) with nonZeroDivisors.coe_ne_zero marked as simp.

For individual level files, a 25% change is not noise and should be something that is understood before making a decision.

I think a good rule of thumb is to look at total changes in instructions for building and for linting both divided by lines of code touched.

[Matthew Ballard]

Is there a particular use case in mind for marking this as simp?

[Daniel Weber]

Nothing that docs#nonZeroDivisors.coe_ne_zero couldn't also prove, I just didn't expect it to have a noticeable performance impact.

[Damiano Testa]

(Just to clarify, the summary above discards changes of < 10^9 instructions in absolute value.)

[Matthew Ballard]

It is hard to predict. Interactions are complex.

[Matthew Ballard]

We probably have many existing simp theorems that are doing exactly this in master currently

[Matthew Ballard]

It's good to benchmark anything that

• modifies the import graph
• adds global simp theorems or
• adds global instances

so one doesn't need to speculate and can just see the fallout directly. It is great to see this done before things are merged!

[Daniel Weber]

I moved the @[simp] to coe_ne_zero and now the benchmark seems fine

[Kyle Miller]

nonZeroDivisors.coe_ne_zero is better as a simp lemma, since the conclusion contains the MonoidWithZero instance, which constrains it more, and also the lemma is not conditional on discharging another hypothesis. There's still a cost to needing to synthesize a Nontrivial instance, but it's likely to succeed given the conclusion.

[Matthew Ballard]

In principle, I agree but what are the keys for these two declarations?

For ne_zero, I get #[*].

For coe_ne_zero, I get #[Subtype.0, *].

[Matthew Ballard]

For reference, here is what I am using

def discrKey (e : Expr) : MetaM (Array DiscrTree.Key) := do
  let (_, _, type) ← withReducible <| forallMetaTelescopeReducing e
  let type ← whnfR type
  if let some (_, lhs, _) := type.eq? then
    DiscrTree.mkPath lhs simpDtConfig
  else if let some (lhs, _) := type.iff? then
    DiscrTree.mkPath lhs simpDtConfig
  else if let some (_, lhs, _) := type.ne? then
    DiscrTree.mkPath lhs simpDtConfig
  else if let some p := type.not? then
    match p.eq? with
    | some (_, lhs, _) =>
      DiscrTree.mkPath lhs simpDtConfig
    | _ => throwError "unexpected kind of 'simp' theorem{indentExpr type}"
  else throwError "unexpected kind of 'simp' theorem{indentExpr type}"

open Elab Term
elab "#discr_tree_key" id:ident : command => do
  Command.liftTermElabM <| do
    let info ← getConstInfo id.getId
    IO.println ((← discrKey info.type).map fun key => key.format)

[Matthew Ballard]

Is it just because we don't index lambdas?