why isn't `Real.fact_zero_lt_one` an instance?

Stream: mathlib4

[David Loeffler]

Is there a reason why docs#Real.fact_zero_lt_one is not (globally) an instance?

Lots of lemmas in Fourier theory require this, because almost every lemma about AddCircle has [Fact (0 < T)] among its hypotheses. So there are something like 8 different files which make Real.fact_zero_lt_one into a local instance. Is there any reason for not doing it globally?

[Ruben Van de Velde]

My understanding is that when the type class system tries to find a Fact insurance, it needs to look at all the Fact instances, so each new global instance slows down all Fact arguments

[Kyle Miller]

Two notes from the documentation:

In particular, this class is not intended for turning the type class system
into an automated theorem prover for first order logic.

In most cases, we should not have global instances of Fact; typeclass search only reads the head
symbol and then tries any instances, which means that adding any such instance will cause slowdowns
everywhere. We instead make them as lemmata and make them local instances as required.

[Kyle Miller]

That said, you can see that there are global instances in the docgen for docs#Fact that are similar to 0 < 1 in spirit, so maybe that concrete fact is justifiable as a Fact instance.

[David Loeffler]

Kyle Miller said:

In most cases, we should not have global instances of Fact; typeclass search only reads the head
symbol and then tries any instances, which means that adding any such instance will cause slowdowns
everywhere. We instead make them as lemmata and make them local instances as required.

Just out of curiousity, where does this second quote come from? It's not familiar to me.

I'm wondering which is the lesser evil: a specific Fact that 0 < 1 in the reals, or a generic instance which will match any LinearOrderedRing. (The case of Rat is also used, e.g. in the code for injective resolutions of groups.)

[Timo Carlin-Burns]

Was this note written before typeclass synthesis used a discrimination tree? I don't think it's true in general that it only filters by the head symbol

[Kyle Miller]

Search for library_note "fact non-instances". Unfortunately this doesn't appear in the docgen yet (so it's not really in the documentation, but at least it's a docstring).

[Kyle Miller]

And yeah, it probably hasn't been updated since discrimination trees. Lean 3 only used the head symbol.

[David Loeffler]

And yeah, it probably hasn't been updated since discrimination trees. Lean 3 only used the head symbol.

So does this mean that making Real.fact_zero_lt_one a global instance will no longer cause a general slowdown? What about more generally

instance instFactZeroLTOne {𝕜 : Type*} [LinearOrderedRing 𝕜] : Fact ((0 : 𝕜) < 1) := ⟨zero_lt_one⟩

which would also avoid local-instancing the ℚ case in several places?

[Sébastien Gouëzel]

Can you make a PR and !bench it, to see if indeed it doesn't do any harm?

[David Loeffler]

I'm benchmarking the general version for LinearOrderedRings at #12115, and the real-number only version as part of #12020.

[Johan Commelin]

These are indeed legacy design decisions from the Lean 3 era. It is good and interesting to revisit them.