data.nat.cast.defs

Stream: mathlib4

[Jireh Loreaux]

I've been avoiding this file even though it's close to the top because I know that coercions have changed in Lean 4. Has anyone else started thinking about this file yet? If so, do we have any sort of plan?

[Gabriel Ebner]

The thinking has been going on for a long time. :smile: Most of the file is already ported, just in the "wrong" places (grep for AddMonoidWithOne). I think only some of the lemmas are missing.

[Jireh Loreaux]

I kind of figured someone smarter than me had seen it coming. :smiley:

[Jireh Loreaux]

Do we have any sort of standard procedure for dealing with the coercion transition then? If so, can we write it up somewhere?

[Moritz Doll]

I think it should be done together with Algebra.GroupWithZero.Defs in mathlib4#563

[Jireh Loreaux]

I will tackle this and then incorporate it into mathlib4#563

[Jireh Loreaux]

Am I correct that has_nat_cast should just go away entirely?

[Mario Carneiro]

cc @Gabriel Ebner

[Gabriel Ebner]

Well spotted! I wrote both the Lean 3 and Lean 4 versions of add_monoid_with_one in parallel. The first version didn't have has_nat_cast, and that's the state that mathlib4 is in.

[Gabriel Ebner]

I think I've added has_nat_cast afterwards to make defining type class instances easier. (That is, you can set up the ℕ → R map without first proving that R is an additive monoid.)

[Gabriel Ebner]

So what we should do is backport (forward port?) the NatCast type class to mathlib4.

[Yaël Dillies]

Yes, from experience having has_nat_cast makes defining instances more comfortable.

[Jireh Loreaux]

Okay, so I should port has_nat_cast to a NatCasttype class. Got it.

[Jireh Loreaux]

Should it still go in data.nat.cast.defs? Or should I put it in Mathlib.Algebra.GroupWithZero.Defs?

[Gabriel Ebner]

I've also moved around the mathlib3 files long after the mathlib4 one was merged. One reason was to reduce the imports. So I think we should also have a Mathlib.Data.Nat.Cast.Defs split in mathlib4.

[Jireh Loreaux]

Currently, in mathlib3, add_monoid_with_one and has_nat_cast are both defined in data.nat.cast. In mathlib4, AddMonoidWithOne is defined in Mathlib.Algebra.GroupWithZero.Defs. Are you wanting me to move that? Sorry, I'm just not understanding the plan.

[Jireh Loreaux]

Nevermind, I think I understand now. I just read the details on #563. These things should move in mathlib4 to the places they appear in mathlib3.