!4#3805 (Analysis.NormedSpace.CompactOperator)

Stream: mathlib4

[David Loeffler]

I had a stab at porting Analysis.NormedSpace.CompactOperator, see !4#3805. I fixed all the failures in the auto-port except one, which I can't solve. The error message is this:

application type mismatch
  ContinuousLinearMap σ₁₂
argument
  σ₁₂
has type
  @RingHom 𝕜₁ 𝕜₂ NonAssocRing.toNonAssocSemiring NonAssocRing.toNonAssocSemiring : Type (max ?u.358606 ?u.358609)
but is expected to have type
  @RingHom 𝕜₁ 𝕜₂ Semiring.toNonAssocSemiring Semiring.toNonAssocSemiring : Type (max ?u.358606 ?u.358609)

This looks like the sort of thing that etaExperiment usually fixes, but enabling it for this theorem brings up a different error which I don't pretend to understand. Can anyone help me finish this off?

[Matthew Ballard]

attribute [-instance] Ring.toNonAssocRing

might fix this

[David Loeffler]

It doesn't see

Matthew Ballard said:

attribute [-instance] Ring.toNonAssocRing

might fix this

It doesn't, sadly (either with or without etaExperiment as well) -- it just gives a different error message. But Kevin has pointed out on the PR that !4#3809 might solve the problem (edit: typo)

[Kevin Buzzard]

(deleted)

[Eric Wieser]

What's the "different error"?

[David Loeffler]

Eric Wieser said:

What's the "different error"?

failed to synthesize instance TopologicalSpace (M₁ →SL[σ₁₂] M₂)

[Eric Wieser]

That sounds like the thing to try to fix

[Eric Wieser]

See if you can synthesize it manually with #synth

[David Loeffler]

(The declaration that causes the error is

theorem compactOperator_topologicalClosure {𝕜₁ 𝕜₂ : Type _} [NontriviallyNormedField 𝕜₁]
    [NormedField 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {M₁ M₂ : Type _} [SeminormedAddCommGroup M₁]
    [AddCommGroup M₂] [NormedSpace 𝕜₁ M₁] [Module 𝕜₂ M₂] [UniformSpace M₂] [UniformAddGroup M₂]
    [ContinuousConstSMul 𝕜₂ M₂] [T2Space M₂] [CompleteSpace M₂]
    [ContinuousSMul 𝕜₂ (M₁ →SL[σ₁₂] M₂)] :
    (compactOperator σ₁₂ M₁ M₂).topologicalClosure = compactOperator σ₁₂ M₁ M₂ :=
  SetLike.ext' isClosed_setOf_isCompactOperator.closure_eq

)

[Kevin Buzzard]

Setting etaExperiment true gives the error

stuck at solving universe constraint
  max ?u.371016 ?u.371017 =?= max u_3 u_4
...

which can perhaps be fixed with the new TypeMax hack

[Eric Wieser]

I would guess setting explicit universes solves the problem

[Eric Wieser]

That is, using {A : Type u} {B : Type v} instead of {A B : Type _}

[Sebastien Gouezel]

I've made some experiments to see if one could solve some needs for eta in linear algebra by tweaking priorities. The outcome is is !4#3809, and it seems pretty good.

[Sebastien Gouezel]

Here is what I did there. In linear algebra, you have modules (the definition of modules depends on a Semiring R) and semilinear maps, based on some map of kind ->+* (where the definition of these maps depends on a NonAssocSemiring R). The main issue comes from the fact that, when you have Ring R, then the path found by instance search to NonAssocSemiRing R goes currently through NonAssocRing R instead of going through Semiring R (and the diamond does not seem to be defeq without eta, for reasons I don't really understand). What I've done in the PR is tweak the priorities so that the path found by instance search now goes through Semiring R. And apparently this solves a lot of issues with linear algebra (including the !4#3805 one).

[Sebastien Gouezel]

Of course, it doesn't "solve" everything (because it's impossible to solve everything without eta or flat structures). But even if we eventually make eta perform better, my guess is that it would still be a good move to do, to make sure that most of the time Lean follows the same path in instances and so everything becomes trivially defeq.

[Sebastien Gouezel]

(And I have to use a roundabout trick to change the priorities, because right now one can not change these priorities because of lean4#2115 -- instead, I changed the order of declarations, as the last declared one is tried first).

[David Loeffler]

And apparently this solves a lot of issues with linear algebra (including the !4#3805 one).

Indeed. Not only does this fix the one problem I couldn't solve in !4#3805, it also allows me to remove the 17 instances of etaExperiment I needed to add to get the rest of the file to compile.

[Eric Wieser]

You shouldn't feel particularly guilty about adding those

[David Loeffler]

I wasn't losing sleep over it, but it is nice to remove them since it gives a noticeable speedup

[Eric Wieser]

Sebastien Gouezel said:

(And I have to use a roundabout trick to change the priorities, because right now one can not change these priorities because of lean4#2115 -- instead, I changed the order of declarations, as the last declared one is tried first).

Let's make sure to add a porting note about that

[Eric Wieser]

Though we could even try backporting and see if it helps lean3

[Anatole Dedecker]

Thanks a lot Sebastien! I had a try at doing something similar but I couln't make it work. This should help to unstuck !4#3708 too.

[Sebastien Gouezel]

I should mention I started from the minimized file you provided some days ago: without it, I would never have understood what was going on.

[Eric Wieser]

Is that aimed at Anatole or me?

[Sebastien Gouezel]

It was aimed at @Anatole Dedecker . I was thinking of https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Some.20observations.20on.20eta.20experiment/near/354981202