Typeclass instance loops

Stream: mathlib4

[Artie Khovanov]

The predicate IsOrderedRing R is strictly weaker than IsStrictOrderedRing R (e.g. $\mathbb{Z}[\varepsilon]/\langle\varepsilon^2\rangle$). However, over a field, the two are equivalent, and the content of IsOrderedRing is the standard definition.

Since mathlib4 allows instance loops, I tried to make this into an instance in #27178, incurring a mild performance hit. However, @Eric Wieser told me that the right spelling of "ordered field" should be [Field F] [LinearOrder F] [IsStrictOrderedRing F] in order to avoid the instance loop and to make it consistent with the spelling when not over a field.

Two questions
(1) Is there anywhere else in the library that we have this pattern? That is, where the mathlib definition uses a stronger class instance than the "standard" textbook definition would suggest due to how the instances line up in a weaker context?
(2) I have a similar problem with the existing IsSemireal class and my proposed IsFormallyReal class. Over a ring, IsFormallyReal is strictly stronger (e.g. $\mathbb{Q}[X,iX]$). Over a field, they are equivalent. Again, the content of IsSemireal is the standard definition. By the same logic, I understand the should be [Field F] [IsFormallyReal F], with no instance from IsSemireal to IsFormallyReal over a Field?

[Aaron Liu]

I would like to say that we assume compact Hausdorff spaces as [CompactSpace X] [T2Space X] 97 times according to #loogle, but the equivalent spelling [CompactSpace X] [T4Space X] with stronger typeclasses gets zero results.

[Aaron Liu]

@loogle CompactSpace ?X → T2Space ?X → _

[loogle]

:search: Ultrafilter.lim_eq_iff_le_nhds, isOpen_iff_ultrafilter', and 95 more

[Aaron Liu]

@loogle CompactSpace, T4Space

[loogle]

:shrug: nothing found

[Artie Khovanov]

Interesting @Aaron Liu - is there an instance [CompactSpace X] [T2Space X] -> [T4Space X] ("compact Hausdorff spaces are normal")? The crucial property in my examples is there there's theory on the T4 / IsStrictOrderedRing / IsFormallyReal class (in the absence of CompactSpace / Field) that I'd like to be able to use automatically.

[Aaron Liu]

import Mathlib

variable {X : Type*} [TopologicalSpace X]
  [CompactSpace X] [T2Space X]

-- T4Space.of_paracompactSpace_t2Space
#synth T4Space X

[Kenny Lau]

Artie Khovanov said:

Since mathlib4 allows instance loops

is that true? i've not been informed of that?

[Artie Khovanov]

hm right thanks @Aaron Liu
seems like both design patterns are present in the library
I would strongly push to have the "right" typeclass to use in Mathlib be the one that's intuitive from the literature, where possible
even if this results in a mild performance hit due to the instance loop
eg if somebody writes [Field F] [LinearOrder F] [IsOrderedRing F] it will all look correct except now linarith, positivity etc doesn't work and it's very non obvious why

[Artie Khovanov]

Kenny Lau said:

Artie Khovanov said:

Since mathlib4 allows instance loops

is that true? i've not been informed of that?

the code snippet Aaron posted above implies they must be allowed

[Yaël Dillies]

Aaron Liu said:

I would like to say that we assume compact Hausdorff spaces as [CompactSpace X] [T2Space X] 97 times according to #loogle, but the equivalent spelling [CompactSpace X] [T4Space X] with stronger typeclasses gets zero results.

I think this is mostly because of how obscure T₄ is. I am an analyst and I can't even tell you what it means off-hand!

[Eric Wieser]

Artie Khovanov said:

Is there anywhere else in the library that we have this pattern? That is, where the mathlib definition uses a stronger class instance than the "standard" textbook definition would suggest due to how the instances line up in a weaker context?

Yes, between

• [NormedDivisionRing K] [NormedAddCommGroup V] [Module K V] [NormSMulClass K V] (what we use)
• [NormedDivisionRing K] [NormedAddCommGroup V] [Module K V] [IsBoundedSMul K V] ("weaker" assumptions, but provably equivalent via docs#NormedDivisionRing.toNormSMulClass)

[Eric Wieser]

This example came up in a refactor by @David Loeffler which introduced docs#NormSMulClass, and I think he initially built 2. but I argued for 1.

[Artie Khovanov]

@Eric Wieser This was the example you gave in the PR, right? I think that's a bit different, because surely the standard definition of a normed module is that norm is multiplicative?

[Artie Khovanov]

Like, if we always want to go with the weaker class and remove loops, then that's fine, but I'd personally prefer loops where they yield more intuitive definitions.

[David Loeffler]

Just coming late to this thread: I disagree with @Artie Khovanov about what is the "standard definition"; when you look at modules over normed rings, not fields – modules over Banach algebras, etc – it starts to seem very unnatural and inconvenient to require precise multiplicativity of the norm, and sub-multiplicativity is the much more natural concept. That was the whole point of my refactor: to make it possible to state theorems about Banach modules over Banach algebras in a natural way.

[Artie Khovanov]

hmm, fair enough - looks like it is a similar example

[Junyan Xu]

The combination [Field R] [IsOrderedRing R] is also being added at https://github.com/leanprover-community/mathlib4/pull/28179/files#diff-992879dba2aba59569a7f9927753bfac51b97ec097d9868083b355cbb93fa772R140-R145 and I personally prefer it.

[Artie Khovanov]

@Junyan Xu indeed, in that PR, the instance is added back manually within the proof
I think in either case that PR has the wrong design - either we should make .toStrictOrderedRing an instance, or (much as I dislike this) we should use the stronger instance in the hypotheses

[Jireh Loreaux]

We also use [Ring R] [IsTopologicalRing R] in hypotheses instead of IsTopologicalSemiring R, even though these are equivalent.

[Eric Wieser]

I think it's clear we should have a linter against these "weaker" spellings if we want to discourage them. Although actually, the instance not existing already works

[Artie Khovanov]

Eric Wieser said:

Although actually, the instance not existing already works

This is my point -- I don't think it does! It does in the examples where you can weaken the standard definition, but not in my example or the module over Banach algebra example. You write the obvious thing, and tactics, exact etc. just fail silently. I think a linter would be a good idea if we indeed want to avoid these sorts of threads every so often.

[Artie Khovanov]

Secondary consideration: we should formally write the preferred spelling down somewhere in the documentation.

[Eric Wieser]

I think if we have a correct linter we shouldn't do that

[Aaron Liu]

No we definitely should write the preferred spelling somewhere

[Artie Khovanov]

I would even push for library note with @Eric Wieser's rationale + common preferred spellings somewhere (else?)

[Eric Wieser]

Aaron Liu said:

No we definitely should write the preferred spelling somewhere

Sounds like a recipe for having it go out of sync with the linter

[Aaron Liu]

Things go out of sync all the time

[Aaron Liu]

Just yesterday I saw docs#ModelWithCorners.toFun' docstring saying something about how the port is still happening

Coercion of a model with corners to a function. We don't use e.toFun because it is actually e.toPartialEquiv.toFun, so simp will apply lemmas about toPartialEquiv. While we may want to switch to this behavior later, doing it mid-port will break a lot of proofs.