exposed data

Stream: mathlib4

[Matthew Ballard]

In #11331, we change

instance mulAction : MulAction S₂ (M₁ →SL[σ₁₂] M₂) where
  smul c f := ⟨c • (f : M₁ →ₛₗ[σ₁₂] M₂), (f.2.const_smul _ : Continuous fun x => c • f x)⟩
  one_smul _f := ext fun _x => one_smul _ _
  mul_smul _a _b _f := ext fun _x => mul_smul _ _ _

to

instance instSMul : SMul S₂ (M₁ →SL[σ₁₂] M₂) where
  smul c f := ⟨c • (f : M₁ →ₛₗ[σ₁₂] M₂), (f.2.const_smul _ : Continuous fun x => c • f x)⟩

instance mulAction : MulAction S₂ (M₁ →SL[σ₁₂] M₂) where
  one_smul _f := ext fun _x => one_smul _ _
  mul_smul _a _b _f := ext fun _x => mul_smul _ _ _

to prevent Lean from unfolding smul unless necessary in defeq checks.

We get

  Benchmark                                             Metric         Change
  ===========================================================================
+ ~Mathlib.Analysis.Calculus.FDeriv.Mul                 instructions    -8.9%
+ ~Mathlib.Analysis.InnerProductSpace.Adjoint           instructions   -10.4%
+ ~Mathlib.Analysis.InnerProductSpace.Basic             instructions    -4.7%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear   instructions   -13.0%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier         instructions    -5.9%
+ ~Mathlib.Geometry.Manifold.ContMDiff.NormedSpace      instructions   -12.6%

Here is the benchmarking comparison in detail.

[Matthew Ballard]

The cost is that elaboration can need some additional help but the fallout here is minor

[Matthew Ballard]

This begs the question: What do people think of a convention where you explicitly declare instances of data carrying parents? Perhaps only the small ones?

[Matthew Ballard]

For a (not very good) example of where nothing really happens see #11329. The build lint change is noise.

It is not a very good example because docs#DirectSum.mulHom is not reducible despite being used in the NonUnitalNonAssocSemiring instance currently

[Eric Wieser]

Matthew Ballard said:

The cost is that elaboration can need some additional help but the fallout here is minor

In particular, the difference is that in the old spelling, the MulAction instance could always be found by unification, but now there are presumably cases where it has to be found by TC search

[Eric Wieser]

My expectation would have been that performance worsened as a result; perhaps it is worth waiting for the next lean release that is much more willing to use unification to find instance arguments?

[Matthew Ballard]

#11332 another example with Units

[Matthew Ballard]

I am not sure if a reducible definition would behave the same