perf(Tactic/FieldSimp): exclude simp lemmas that don't apply for fields.

[JovanGerb]

This PR excludes simp lemmas like div_self' from being used in the field_simp tactic. These lemmas have discrimination tree keys that commonly find a match when running field_simp, and if they do match then unification needs to fail, because the field is in fact not a Group/CommGroup/LeftCancelMonoid/RightCancelMonoid.

---

[JovanGerb]

!bench

[github-actions]

PR summary 84caac5752

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ fieldSimpExcluded

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[leanprover-bot]

Here are the benchmark results for commit 84caac5.
There were significant changes against commit 213a36c:

  Benchmark                                                        Metric         Change
  ======================================================================================
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Affine                  instructions    -8.7%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian                instructions    -4.9%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Projective              instructions    -4.0%
+ ~Mathlib.Analysis.Convex.Slope                                   instructions   -19.3%
+ ~Mathlib.Analysis.Convex.Visible                                 instructions   -18.5%
+ ~Mathlib.Analysis.SpecialFunctions.Gamma.Deligne                 instructions   -29.6%
+ ~Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd   instructions   -31.1%

[github-actions]

File	Instructions	%
build	-410.161⬝10⁹	(-0.26%)

40 files, Instructions -2.0⬝10⁹

File	Instructions	%
Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic	-1.1⬝10⁹	(-3.32%)
Mathlib.Analysis.Calculus.Rademacher	-1.29⬝10⁹	(-1.57%)
Mathlib.Analysis.Convex.Side	-1.38⬝10⁹	(-1.23%)
Mathlib.Topology.Sheaves.Stalks	-1.64⬝10⁹	(-0.77%)
Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs	-1.126⬝10⁹	(-7.33%)
Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics	-1.137⬝10⁹	(-5.24%)
Mathlib.RingTheory.Valuation.ValuationSubring	-1.141⬝10⁹	(-0.96%)
Mathlib.Analysis.Analytic.Meromorphic	-1.151⬝10⁹	(-2.41%)
Mathlib.Analysis.Convex.Strict	-1.197⬝10⁹	(-3.79%)
Mathlib.Analysis.Fourier.AddCircle	-1.209⬝10⁹	(-1.58%)
Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating	-1.221⬝10⁹	(-3.60%)
Mathlib.NumberTheory.LSeries.MellinEqDirichlet	-1.230⬝10⁹	(-4.53%)
Mathlib.Analysis.Asymptotics.AsymptoticEquivalent	-1.247⬝10⁹	(-4.83%)
Mathlib.Data.Array.Lemmas	-1.248⬝10⁹	(-26.28%)
Mathlib.Analysis.InnerProductSpace.Rayleigh	-1.263⬝10⁹	(-2.69%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic	-1.280⬝10⁹	(-1.30%)
Mathlib.MeasureTheory.Integral.MeanInequalities	-1.332⬝10⁹	(-2.64%)
Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv	-1.333⬝10⁹	(-7.18%)
Mathlib.Analysis.SpecialFunctions.Log.Deriv	-1.342⬝10⁹	(-3.02%)
Mathlib.Analysis.Convex.Continuous	-1.376⬝10⁹	(-3.57%)
Mathlib.Analysis.SpecialFunctions.Complex.Circle	-1.395⬝10⁹	(-9.82%)
Mathlib.Geometry.Euclidean.Inversion.Basic	-1.429⬝10⁹	(-7.26%)
Mathlib.Combinatorics.Derangements.Exponential	-1.469⬝10⁹	(-17.64%)
Mathlib.Data.Complex.Trigonometric	-1.502⬝10⁹	(-1.85%)
Mathlib.Data.Complex.Exponential	-1.506⬝10⁹	(-2.21%)
Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension	-1.557⬝10⁹	(-2.29%)
Mathlib.Analysis.Convex.Between	-1.558⬝10⁹	(-1.77%)
Mathlib.Analysis.InnerProductSpace.Defs	-1.599⬝10⁹	(-3.61%)
Mathlib.Analysis.SpecialFunctions.Exp	-1.642⬝10⁹	(-5.45%)
Mathlib.Analysis.Convex.Join	-1.685⬝10⁹	(-5.17%)
Mathlib.Analysis.Complex.UpperHalfPlane.Metric	-1.687⬝10⁹	(-1.42%)
Mathlib.Analysis.SpecialFunctions.Gamma.Basic	-1.697⬝10⁹	(-4.55%)
Mathlib.Analysis.SpecialFunctions.Gamma.Beta	-1.710⬝10⁹	(-3.74%)
Mathlib.Analysis.Complex.LocallyUniformLimit	-1.798⬝10⁹	(-8.34%)
Mathlib.MeasureTheory.Measure.Tilted	-1.834⬝10⁹	(-5.71%)
Mathlib.NumberTheory.Harmonic.ZetaAsymp	-1.867⬝10⁹	(-4.06%)
Mathlib.GroupTheory.CommutingProbability	-1.876⬝10⁹	(-8.01%)
Mathlib.Analysis.Complex.Arg	-1.908⬝10⁹	(-20.26%)
Mathlib.Analysis.SpecialFunctions.Complex.LogBounds	-1.911⬝10⁹	(-4.73%)
Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric	-1.975⬝10⁹	(-4.95%)

16 files, Instructions -3.0⬝10⁹

File	Instructions	%
Mathlib.Analysis.Polynomial.CauchyBound	-2.51⬝10⁹	(-10.79%)
Mathlib.Algebra.Polynomial.HasseDeriv	-2.54⬝10⁹	(-9.40%)
Mathlib.Algebra.QuadraticDiscriminant	-2.70⬝10⁹	(-8.61%)
Mathlib.Combinatorics.SetFamily.AhlswedeZhang	-2.88⬝10⁹	(-5.40%)
Mathlib.Analysis.Convex.Jensen	-2.201⬝10⁹	(-4.71%)
Mathlib.Geometry.Euclidean.Sphere.Ptolemy	-2.264⬝10⁹	(-23.99%)
Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn	-2.270⬝10⁹	(-4.55%)
Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls	-2.468⬝10⁹	(-3.60%)
Mathlib.Analysis.Complex.Angle	-2.487⬝10⁹	(-13.62%)
Mathlib.Analysis.CStarAlgebra.ApproximateUnit	-2.529⬝10⁹	(-1.68%)
Mathlib.Data.Real.GoldenRatio	-2.623⬝10⁹	(-11.21%)
Mathlib.NumberTheory.Modular	-2.678⬝10⁹	(-3.12%)
Mathlib.Probability.Distributions.Gaussian	-2.732⬝10⁹	(-6.55%)
Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace	-2.742⬝10⁹	(-5.11%)
Mathlib.Geometry.Manifold.Instances.Sphere	-2.799⬝10⁹	(-1.94%)
Mathlib.Analysis.Calculus.FDeriv.Measurable	-2.888⬝10⁹	(-2.70%)

7 files, Instructions -4.0⬝10⁹

File	Instructions	%
Mathlib.Analysis.Analytic.Composition	-3.80⬝10⁹	(-2.12%)
Mathlib.NumberTheory.LSeries.AbstractFuncEq	-3.187⬝10⁹	(-5.70%)
Mathlib.FieldTheory.Differential.Basic	-3.361⬝10⁹	(-8.39%)
Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable	-3.404⬝10⁹	(-3.80%)
Mathlib.Combinatorics.Additive.PluenneckeRuzsa	-3.674⬝10⁹	(-9.21%)
Mathlib.Analysis.Calculus.Deriv.Inv	-3.760⬝10⁹	(-9.61%)
Mathlib.NumberTheory.DiophantineApproximation.Basic	-3.924⬝10⁹	(-8.33%)

9 files, Instructions -5.0⬝10⁹

File	Instructions	%
Mathlib.NumberTheory.Bernoulli	-4.208⬝10⁹	(-6.82%)
Mathlib.RingTheory.Valuation.ValuationRing	-4.209⬝10⁹	(-9.23%)
Mathlib.Analysis.Analytic.Basic	-4.321⬝10⁹	(-1.68%)
Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms	-4.582⬝10⁹	(-8.43%)
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic	-4.595⬝10⁹	(-2.03%)
Mathlib.Analysis.FunctionalSpaces.SobolevInequality	-4.737⬝10⁹	(-3.86%)
Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform	-4.771⬝10⁹	(-5.65%)
Mathlib.Combinatorics.Enumerative.Catalan	-4.834⬝10⁹	(-18.13%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex	-4.863⬝10⁹	(-17.68%)

5 files, Instructions -6.0⬝10⁹

File	Instructions	%
Mathlib.Analysis.Calculus.LogDeriv	-5.65⬝10⁹	(-20.71%)
Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral	-5.138⬝10⁹	(-10.53%)
Mathlib.Analysis.SpecificLimits.FloorPow	-5.655⬝10⁹	(-10.85%)
Mathlib.RingTheory.RootsOfUnity.Complex	-5.679⬝10⁹	(-27.01%)
Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ	-5.758⬝10⁹	(-10.47%)

4 files, Instructions -7.0⬝10⁹

File	Instructions	%
Mathlib.NumberTheory.PythagoreanTriples	-6.332⬝10⁹	(-10.99%)
Mathlib.Analysis.Calculus.Taylor	-6.570⬝10⁹	(-14.39%)
Mathlib.Analysis.SpecialFunctions.Stirling	-6.576⬝10⁹	(-14.17%)
Mathlib.RingTheory.WittVector.FrobeniusFractionField	-6.875⬝10⁹	(-12.99%)

3 files, Instructions -8.0⬝10⁹

File	Instructions	%
Mathlib.Analysis.Complex.UpperHalfPlane.Basic	-7.143⬝10⁹	(-10.29%)
Mathlib.NumberTheory.ZetaValues	-7.658⬝10⁹	(-13.85%)
Mathlib.Analysis.SpecialFunctions.Integrals	-7.698⬝10⁹	(-8.75%)

File	Instructions	%
Mathlib.Analysis.InnerProductSpace.Basic	-8.525⬝10⁹	(-7.73%)
Mathlib.NumberTheory.NumberField.Discriminant.Basic	-9.191⬝10⁹	(-6.22%)

2 files, Instructions -14.0⬝10⁹

File	Instructions	%
Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian	-13.298⬝10⁹	(-4.90%)
Mathlib.Analysis.SpecialFunctions.Gamma.Deligne	-13.732⬝10⁹	(-29.62%)

2 files, Instructions -16.0⬝10⁹

File	Instructions	%
Mathlib.AlgebraicGeometry.EllipticCurve.Projective	-15.593⬝10⁹	(-4.02%)
Mathlib.AlgebraicGeometry.EllipticCurve.Affine	-15.910⬝10⁹	(-8.70%)

File	Instructions	%
Mathlib.Analysis.Convex.Visible	-18.762⬝10⁹	(-18.54%)
Mathlib.Analysis.Convex.Slope	-20.508⬝10⁹	(-19.30%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd	-22.817⬝10⁹	(-31.07%)
CI run

[grunweg]

These are impressive gains, thanks a lot! I can take a more detailed look at the list of lemmas later; in the meantime, I was wondering about the followoing:

• Is your list of excluded lemmas exhaustive? (Do you think there are further gains to be had by restricting the list more?)
• Is this the best approach? In the future, when new simp lemmas are added, it's easy for field_simp to regress again. Would it make more sense to have field_simps operate on a manually curated list of lemmas instead? How many lemmas do field_simp calls in mathlib use, overall? (This is a bit hard to determine, as there is no field_simp?. I'd try to replace it with the supposedly equivalent simp (disch := ...) call, and see which lemmas are used.
• Finally, it's well-known that field_simp is in need of a major rewrite. So far, nobody actually had/took the time to do so. (I might in the future, but at this point that is not certain.) So I wouldn't want to spend too much time on a temporary solution. At the same time, this PR is a strict improvement, does not pose a maintenance burden (the worst case is it regressing... which is still better than the status quo), so I don't think this PR should wait on such a hypothetical future.

I had some PRs un-expanding field_simp calls; I'll test on top of this PR.

[JovanGerb]

For the list of lemmas, I particularly picked all lemmas involving *, / and =. I skipped the ones with ⁻¹ since ⁻¹ shouldn't appear in field_simp. I looked through all the lemmas in Mathlib.Algebra.Group.Basic, but there might be other lemmas somewhere else that can be excluded too.

Yes, it would be more robust against regression if field_simp only used its own curated set of lemmas, but I don't know which lemmas those are and/or if people expect field_simp to also use normal simp lemmas.