Slowdown on pospart

Stream: mathlib4

[Kenny Lau]

import Mathlib

set_option trace.profiler true
variable {N : ℕ} (u : EuclideanSpace ℝ (Fin N) → ℝ)

#check (u⁺ : EuclideanSpace ℝ (Fin N) → ℝ)
-- [Elab.command] [0.542016] #check (u⁺ : EuclideanSpace ℝ (Fin N) → ℝ)

[Kevin Buzzard]

docs#IsScalarTower.complexToReal is a horrible instance. It says "to check that the reals is doing something nice in a certain situation, it suffices to check that the complexes are doing the same nice thing" which is far less likely to be true and conversely can send typeclass inference on a wild goose chase. The instance is sandwiched between two other instances both of which are prio 900 but for some reason this one isn't.

import Mathlib

set_option trace.profiler true
variable {N : ℕ} (u : EuclideanSpace ℝ (Fin N) → ℝ)

#check (u⁺ : EuclideanSpace ℝ (Fin N) → ℝ) -- 0.34

attribute [instance 900] IsScalarTower.complexToReal

#check (u⁺ : EuclideanSpace ℝ (Fin N) → ℝ) -- 0.18

[Eric Wieser]

It's a bit weirder that that because this is about the Real-module structure that is deduced from the complex module structure

[Eric Wieser]

If you're going to derive the real smul operator from the complex one then you don't really have any choice but to also derive all the compatibility properties in the same way

[Jireh Loreaux]

1. Is the trace looking for a NonUnitalContinuousFunctionalCalculus class somewhere?
2. If so, that may be the real culprit here. We could scope the instances to the CStarAlgebra namespace in case they aren't already.
3. Kevin, I really want that instance so I don't have to always assume my complex C*-algebras are also real algebras. But it's fine to lower the priority I think.

[Kevin Buzzard]

Yeah we need that instance! It's just that it can be costly when it fails, e.g. #synth SMul ℂ ℝ[X][X] takes 0.2 seconds to fail on a fast machine.

Continuous functional calculus: yes, it's about 30-40% of the slowdown:

      [] [0.291078] expected type: EuclideanSpace ℝ (Fin N) → ℝ, term
          PosPart.posPart✝ u ▼
        [Meta.synthInstance] [0.290175] ✅️ PosPart (EuclideanSpace ℝ (Fin N) → ℝ) ▼
          [] [0.012785] ❌️ apply @IsScalarTower.complexToReal to IsScalarTower ℝ ℝ ℝ ▶
          [] [0.124495] ❌️ apply @IsScalarTower.complexToReal to IsScalarTower ℝ (EuclideanSpace ℝ (Fin N) → ℝ)
                (EuclideanSpace ℝ (Fin N) → ℝ) ▶
          [] [0.051119] ❌️ apply @IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus to NonUnitalContinuousFunctionalCalculus ℝ
                (EuclideanSpace ℝ (Fin N) → ℝ) IsSelfAdjoint ▶
          [] [0.013341] ❌️ apply @NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus to NonUnitalContinuousFunctionalCalculus
                ℝ (EuclideanSpace ℝ (Fin N) → ℝ) IsSelfAdjoint ▶
          [] [0.020293] ✅️ apply @ContinuousFunctionalCalculus.toNonUnital to NonUnitalContinuousFunctionalCalculus ℝ
                (EuclideanSpace ℝ (Fin N) → ℝ) IsSelfAdjoint ▶
          [] [0.025813] ❌️ apply @IsSelfAdjoint.instContinuousFunctionalCalculus to ContinuousFunctionalCalculus ℝ
                (EuclideanSpace ℝ (Fin N) → ℝ) IsSelfAdjoint ▶

[Eric Wieser]

If docs#CStarAlgebra is the main concern, we could have it have a [toRealNormedAlgebra : NormedAlgebra Real A] field

[Jireh Loreaux]

I'm taking about scoping this instance: docs#CStarAlgebra.instPosPart, which should instantly solve a large chunk of the slowdown.