OfScientific

Stream: mathlib4

[Heather Macbeth]

I just encountered

failed to synthesize instance
  OfScientific ℝ

while trying to refer to the real number 0.1. Do we want an OfScientific instance for (say) any characteristic-zero field? Is norm_num going to handle this? cc @Thomas Murrills @Mario Carneiro

[Thomas Murrills]

Hmm, I’m not really the one making design choices here, but I definitely think norm_num should be able to recognize scientific notation—it seems it can’t do this even in e.g. the Rat case.

I’ll open an issue/branch and see how far I get writing the extension right now.

[Thomas Murrills]

It also makes sense to me to have OfScientific defined for all charzero division rings. Rat has one already, and I don’t know if the general one should be defined in terms of casting Rat to the charzero field, or if this one should be abandoned in favor of a more general one, or what.

But imo it should exist! I wonder if it’s somewhere in mathlib3 already?

[Thomas Murrills]

Another semi-related question is whether norm_num should handle floats. (Semi-related because scientific notation defaults to Float unless you specify the type.) My guess is maybe, but I'd hope that's not needed soon? :sweat_smile:

[Heather Macbeth]

Thomas Murrills said:

scientific notation defaults to Float unless you specify the type

Is there a way to turn this off? We really don't want unsuspecting mathlib users to encounter Floats after typing 0.1. If there's a default in mathlib it should be Rat.

[Mario Carneiro]

OfScientific is basically a notation typeclass, which provides the interpretation of decimal numbers. I think it is relatively safe to have a blanket implementation for anything that would have a Rat.cast instance.

[Mario Carneiro]

It is more or less unrelated to norm_num, unless that instance leaves some ofScientific term in the expression in which case norm_num will want to unfold it to a fraction

[Mario Carneiro]

in lean 3, this instance was effectively unfolded at parse time, so if you write 0.2 you get exactly the same term as if you had written 1/5 instead

[Mario Carneiro]

Thomas Murrills said:

Another semi-related question is whether norm_num should handle floats. (Semi-related because scientific notation defaults to Float unless you specify the type.) My guess is maybe, but I'd hope that's not needed soon? :sweat_smile:

This is fundamentally impossible for lean 4 Float as currently implemented, because everything is opaque.

Heather Macbeth said:

Thomas Murrills said:

scientific notation defaults to Float unless you specify the type

Is there a way to turn this off? We really don't want unsuspecting mathlib users to encounter Floats after typing 0.1. If there's a default in mathlib it should be Rat.

I have not tried having multiple @[default_instance] instances at once, but I don't see any reason why it wouldn't work. If we provide another default instance for OfScientific pointing at Rat we can override this behavior.

[Heather Macbeth]

Is there going to be an issue having a [DivisionRing K] [CharZero K] instance for OfScientific; will it conflict in the case K = Rat with the instance for Rat?

[Heather Macbeth]

(see discussion on mathlib4#1707)

[Eric Wieser]

It shouldn't do, we already solved this problem in Lean 3

[Heather Macbeth]

How?

[Yaël Dillies]

By making it be part of the definition of DivisionRing

[Thomas Murrills]

For whatever reason it doesn’t seem to conflict as-is—if I type #synth OfScientific Rat after the DivisionRing instance I still get the Rat instance.

Not sure how Lean decides which instance to prefer or if changing the location of the instance might introduce some issues, but if it does, maybe we could tinker with the instance priorities?

[Heather Macbeth]

Yaël Dillies said:

By making it be part of the definition of DivisionRing

What do you mean? Even nonzero characteristic division rings?

[Yaël Dillies]

This is what happens what rat_cast, yes.

[Heather Macbeth]

We're talking about OfScientific, not rat casting. (Of course they're related.)

[Thomas Murrills]

Mario Carneiro said:

It is more or less unrelated to norm_num, unless that instance leaves some ofScientific term in the expression in which case norm_num will want to unfold it to a fraction

Currently we are left with an ofScientific in the expression and norm_num fails when encountering it. Is there a shortcut we’d want to use for unfolding it here, or is the standard procedure for evaluating things warranted?

[Eric Wieser]

docs4#OfScientific for reference

[Eric Wieser]

Heather Macbeth said:

We're talking about OfScientific, not rat casting. (Of course they're related.)

The implementation for a division ring K is presumably going to be ratCast (OfScientific ...). The implementation of ratCast for Rat is just id.

[Yaël Dillies]

Well, rat_cast is enough to define of_scientific, so it should be included in at least all the structures where rat_cast is.

[Eric Wieser]

As Yael alludes to, if we introduce some other division ring which has a more efficient implementation of ofScientific that going through Rat, then we're in trouble unless we make ofScientific a field of docs4#DivisionRing

[Heather Macbeth]

This seems to fail in Lean 4:

import Mathlib.Data.Rat.Basic

example : (1:ℚ) / 10 = 0.1 := rfl -- fails

So I guess we really do need a norm_num extension.

[Eric Wieser]

That's weird; I guess division doesn't reduce any more?

[Mario Carneiro]

Thomas Murrills said:

Mario Carneiro said:

It is more or less unrelated to norm_num, unless that instance leaves some ofScientific term in the expression in which case norm_num will want to unfold it to a fraction

Currently we are left with an ofScientific in the expression and norm_num fails when encountering it. Is there a shortcut we’d want to use for unfolding it here, or is the standard procedure for evaluating things warranted?

I was kind of hoping that lean would automatically unfold the instance like it does for coes, that would make things simpler. If there is a ofScientific then we need to do the usual thing in norm_num: have a norm_num extension that matches on ofScientific and unfolds it to a division or what have you. (If this comes up a few more times we might consider having a meta-norm_num tactic/macro which generates such extensions on demand, similar to the delaborator and formatter that you get for free using syntax.)

[Heather Macbeth]

Note that Thomas already made a first stab at a norm_num extension for OfScientific: mathlib4#1707

[Mario Carneiro]

that last example does seem weird. What does it actually unfold to?

[Mario Carneiro]

oh fun:

#whnf (0.1 : ℚ)
-- Decidable.rec
--   (fun h =>
--     (fun hg => Rat.mk' (Int.div ↑1 ↑(Nat.gcd (Int.natAbs ↑1) (10 ^ 1))) (10 ^ 1 / Nat.gcd (Int.natAbs ↑1) (10 ^ 1))) h)
--   (fun h => (fun hg => Rat.mk' (↑1) (10 ^ 1)) h) (instDecidableEqNat (Nat.gcd (Int.natAbs ↑1) (10 ^ 1)) 1)

[Mario Carneiro]

it looks like it got stuck evaluating Nat.gcd

[Eric Wieser]

Does nat.gcd reduce in Lean 3?

[Thomas Murrills]

Heather Macbeth said:

Note that Thomas already made a first stab at a norm_num extension for OfScientific: mathlib4#1707

I’ve only got it half done—I’m actually encountering some really weird monad errors in the main extension! I’ll bring them up later when I continue working on it.

[Mario Carneiro]

no it does not @Eric Wieser

[Mario Carneiro]

the difference in this case is that the reduction of 0.1 to 1/10 is done by meta code in lean 3, so the theorem 0.1 = 1/10 in lean 3 is a syntactic tautology

[Thomas Murrills]

(Moving from the GitHub discussion) Where is Rat.cast? I can’t seem to find it—only Rat.castRec, RatCast, and Rat.castCoe

[Gabriel Ebner]

I think it's called RatCast.ratCast.

[Thomas Murrills]

My understanding (via Mario’s comments) is that that’s not the lawful version, though, and Rat.cast is meant to be lawful somehow

[Thomas Murrills]

It seems to me like the laws for the rat cast are fields of DivisionRing directly, though. Does Rat.cast as a stand-alone typeclass actually exist yet?

[Gabriel Ebner]

Nat.cast isn't lawful either.

[Gabriel Ebner]

The lawful version of Nat.cast is the AddMonoidWithOne type class. And the lawful version of Int.cast is the AddGroupWithOne type class.

[Gabriel Ebner]

Requiring a DivisionRing instance to prove things about RatCast.ratCast is the right (or at least consistent) thing to do here.

[Kevin Buzzard]

Hot take: AddMonoidWithOne should be the to_additiveised version of MonoidWithE, with E=2.718....

[Reid Barton]

Do we have exponential periods yet?

[Johan Commelin]

Depending on which definition you want, they are either 5 lightyears away, or < 2 days of hacking.

[Thomas Murrills]

Gabriel Ebner said:

Requiring a DivisionRing instance to prove things about RatCast.ratCast is the right (or at least consistent) thing to do here.

Makes sense! So, if we added it as a field to DivisionRing would we also want a field that made ofScientific lawful (i.e. said it was extensionally equal to the cast of Rat.ofScientific)?

This would make it easy to prove things about it (e.g. in norm_num), but I don’t know if any division rings somehow have completely different scientific notations.

[Kevin Buzzard]

The division rings which show up in my research are just full of things called d and x.

[Thomas Murrills]

It shouldn’t be much overhead (computationally or cognitively) in almost all cases, I think, as the default values should take care of it like they do for ratCast: the default value of ofScientific will be the cast of Rat.ofScientific, and so the default proof that it’s lawful will be reflexivity, and you won’t even know it’s there. But if you need 0.1, you’ll have it. :)

[Mario Carneiro]

I still think we should not make this a field and should just have an OfScientific instance for any division ring defined in terms of Rat.ofScientific

[Mario Carneiro]

There are lots of definitions that are not fields, and structure fields have a significant cost on the overall typeclass system, so I would really rather not have silly things like this being something everyone has to deal with when making fields

[Heather Macbeth]

Mario Carneiro said:

I still think we should not make this a field and should just have an OfScientific instance for any division ring defined in terms of Rat.ofScientific

Mario, there's a point about this suggestion which I don't understand -- won't it mean that Rat gets two separate OfScientific instances? Even though their data is the same, I would think that would cause problems.

[Mario Carneiro]

they should be defeq

[Heather Macbeth]

OK, maybe I hadn't appreciated that: it's ok to have multiple instances if they're defeq.

[Mario Carneiro]

because the RatCast Rat instance should be the identity

[Heather Macbeth]

Do they need to be "quickly" defeq?

[Mario Carneiro]

they should be defeq at instance reducibility

[Mario Carneiro]

which I think is the case here

[Thomas Murrills]

Hmm…if someone wants to implement a new definition of ofScientific for their division ring (which happens in one spot I think—something about Cauchy sequences), would that cause problems? Would we give the general one a lower priority or something?

[Mario Carneiro]

They should not do that

[Thomas Murrills]

They already do :grimacing:

[Mario Carneiro]

in lean 3 this was simply not a possibility and I think that was a good thing

[Mario Carneiro]

this is one more knob that people can use to write the same thing in multiple ways

[Thomas Murrills]

(Maybe we can get rid of the bespoke definition? I haven’t checked…)

[Mario Carneiro]

I'm sure the definition was written because the general one didn't exist yet

[Heather Macbeth]

I don't see that one? it's not listed at
https://leanprover-community.github.io/mathlib4_docs/Init/Data/OfScientific.html#OfScientific

[Thomas Murrills]

Wow, if I’m looking at the right thing, it’s disappeared since this thread started! That’s convenient!

[Thomas Murrills]

Oh, perhaps I’m mixing things up. I might have been thinking about things with custom RatCast implementations. docs4#RatCast

Will that also make things potentially break though? When the instance of ofScientific for all division rings searches for a way to cast rationals, will it find the custom cast, or the canonical cast? (Should we just force the canonical cast somehow in this instance?)

[Mario Carneiro]

It doesn't search for a way to cast rationals, the cast is baked into the definition and it is the canonical one

[Thomas Murrills]

Hmmm. So writing (3/4 : ℚ) : R will use the canonical cast instead of whatever the division ring R has defined?

[Thomas Murrills]

(Because that’s all this new instance we’re defining does atm)

[Gabriel Ebner]

I can only think of one case where the blanket instance is problematic: floating point numbers. There the (naive) rat cast version has less precision than the current implementation which directly produces the mantissa.

[Gabriel Ebner]

We could declare the blanket instance only for division rings, where the cast is unique.

[Thomas Murrills]

Is the cast definitionally unique for division rings or just propositionally unique? (Or is the latter enough for all purposes?) Does the ratCast field of division rings ever come into play here?

[Gabriel Ebner]

Just proposition ally.

[Gabriel Ebner]

The ratCast field is used for coercions from rational numbers as the name implies.

[Thomas Murrills]

So when we write this instance for division rings for ofScientific, I’m guessing we should use the value in that field instead of the (potentially not defeq) canonical cast to cast the value of Rat.ofScientific, right? I’m just trying to figure out if that will ever cause any problems…

[Gabriel Ebner]

Oh yeah, I think we should define of scientific in terms of rat cast.

[Mario Carneiro]

Gabriel Ebner said:

I can only think of one case where the blanket instance is problematic: floating point numbers. There the (naive) rat cast version has less precision than the current implementation which directly produces the mantissa.

In that case we don't really care that it's the wrong instance since we aren't proving anything about those floats anyway

[Mario Carneiro]

It should be possible to implement that in such a way that there is no loss however, where the Rat -> Float function builds the nearest float to the rational number according to the rounding mode

[Eric Wieser]

Floating point numbers aren't a division ring so I don't see a conflict here?

[Eric Wieser]

That is, DivisionRing.toOfScientific should be safe

[Gabriel Ebner]

Mario Carneiro said:

Gabriel Ebner said:

I can only think of one case where the blanket instance is problematic: floating point numbers. There the (naive) rat cast version has less precision than the current implementation which directly produces the mantissa.

In that case we don't really care that it's the wrong instance since we aren't proving anything about those floats anyway

On the contrary, we care much more for floating-point numbers than for division rings because the two operations are not equivalent. It's not just that we can't prove they're equal, we can actually observe that one of them is much worse! For division rings, it doesn't really matter whether we define scientific literals as ratCast ... or intCast .. / natCast ... or something else, because we provably get the same result every time. But for floating-point numbers e.g. going via intCast .. / natCast .. would have unacceptable numerical precision.

[Mario Carneiro]

was intCast .. / natCast .. ever on the table?

[Mario Carneiro]

that is a terrible implementation

[Gabriel Ebner]

Mario Carneiro said:

It should be possible to implement that in such a way that there is no loss however, where the Rat -> Float function builds the nearest float to the rational number according to the rounding mode

It is a good idea to define ratCast that way (or at least close enough to that spec). Which still leaves the issue that 0.1 might be a different floating-point number depending on which instance is used. I'd like to avoid that potential nightmare.

[Mario Carneiro]

Like Eric said, there is no diamond here

[Gabriel Ebner]

?

[Mario Carneiro]

Float is not a division ring

[Gabriel Ebner]

Core has an OfScientific instance for Float.

[Mario Carneiro]

no one is suggesting an instance for [RatCast R] : OfScientific R

[Gabriel Ebner]

Oh yeah, my objections doesn't apply to the [DivisionrRing R] : OfScientific R instance.

[Mario Carneiro]

I don't think Float has a RatCast instance either, for that matter

[Mario Carneiro]

although it probably should

[Gabriel Ebner]

Mario Carneiro said:

no one is suggesting an instance for [RatCast R] : OfScientific R

I was going by Thomas's comment on the norm_num PR:

Though, @digama0, you suggested a blanket implementation for anything that has an instance of RatCast.

[Mario Carneiro]

yes, he misunderstood what I meant by "the instances required to get Rat.cast"

[Thomas Murrills]

Ok, ofScientific in norm_num now works (mathlib4#1707) :)

[Thomas Murrills]

I relocated things best I could, and I’m sure there are cleanups or improvements to be made, but given the teaching deadline, I wanted to put it out for review asap!