moving RatCast to Std

Stream: mathlib4

[Thomas Murrills]

@Mario Carneiro , how should we manage the imports here? Std.Classes.Cast needs Std.Data.Rat.Basic to know what Rat is, but Std.Data.Rat.Basic depends on Std.Classes.Cast. (Should the definition of Rat move? Or should the coercion instances move to a new file Std.Data.Rat.Cast?)

[Mario Carneiro]

Yeah, I was too quick to say it should go in that file. I would put it in Std.Classes.RatCast

[Thomas Murrills]

uh-oh: universe level errors

[Thomas Murrills]

(deleted)

[Thomas Murrills]

oops nvm

[Thomas Murrills]

do I need to worry about putting a copyright-related comment at the top of this new file? if so what should it be?

[Mario Carneiro]

copy it from mathlib

[Mario Carneiro]

minus the "this file is aligned" part if any

[Thomas Murrills]

from mathlib? not std?

[Mario Carneiro]

the code you are PR'ing is from mathlib is it not?

[Thomas Murrills]

hmmm...some of it yes

[Thomas Murrills]

some of it is derived from existing std code

[Mario Carneiro]

you can add yourself as author if you added something significant beyond the copypasta

[Thomas Murrills]

hmmm I don't know if I did. the rewritten ofScientific instance is in this file but is that really "significant"?

[Thomas Murrills]

more of a slight change

[Thomas Murrills]

I suppose I should union the sets of authors over all files I copied stuff from though

[Thomas Murrills]

though different people hold the copyright...not sure how that works

[Mario Carneiro]

the top line is the earliest contributor

[Thomas Murrills]

interesting. both you and Robert Lewis contributed stuff in 2014, but I can't pin down an exact date for when this file emerged via the github history. only seems to go back a year, even via the rename. I'll leave it as Robert Lewis for now since I already committed :sweat_smile:

[Thomas Murrills]

ok, std4#101 is up there

[Thomas Murrills]

It does seem like this will cause at least one minor breakage in mathlib4, which I'm guessing we can fix by changing

@[norm_cast]
theorem cast_id (n : ℚ) : (RatCast.ratCast n) = n := by rfl

to

@[norm_cast]
theorem cast_id (n : ℚ) : (Rat.cast n) = n := by rfl

[Thomas Murrills]

how do we deal with this, though? can we have "simultaneous PR's", or do we have PR's on mathlib4 which update the manifest and fix changes, or?

[Thomas Murrills]

Re: making overlapping OfScientific instances: how would we make the two instances defeq at .instances transparency? The following are failing for me (in a file where I can evaluate it):

attribute [-instance] instOfScientific

instance y : OfScientific Rat where ofScientific := Rat.ofScientific
instance x [DivisionRing α] : OfScientific α where ofScientific m s e := (y.ofScientific m s e : α)
instance x' [DivisionRing α] : OfScientific α where ofScientific m s e := (Rat.ofScientific m s e : α)

example : y = x := by with_reducible_and_instances rfl -- fails
example : y = x' := by with_reducible_and_instances rfl -- fails

[James Gallicchio]

I think whoever bumps Std versions will deal with all these updates -- some of the List Perm stuff will need small changes in mathlib4 too, but easier to handle it all at once I guess

[Thomas Murrills]

Ok, as discussed in today's mathlib porting meeting and as proposed by @Gabriel Ebner here, I went ahead and made Nat.cast, Int.cast, and the incoming Rat.cast reducible in std4#101.

This also means nothing related to OfScientific needs to be addressed in that PR now.

[Thomas Murrills]

Pinging std4#101 since there's been some activity on a PR which depends on it; @Gabriel Ebner I removed id from the reflexive instances as suggested (consider me gotcha'd :upside_down:)

[Gabriel Ebner]

LGTM.